Дизъюнктивный силлогизм в системе стилей Fitch

Я пытаюсь доказать аргумент формы:

  1. Б
  2. ~ (С и Б)

Поэтому: ~С.

Я могу расширить ~(C & B) до ~C ИЛИ ~B, и с предпосылкой B ясно, что имеет место ~C.

Однако у меня возникли проблемы с доказательством этого с использованием системы стиля Fitch. Я пробовал дизъюнктивное исключение, но я не вижу, как добраться до ~ C из предположения ~ B, поэтому мне интересно, правильный ли это путь.

Если кто-нибудь знает, как показать эквивалент дизъюнктивного силлогизма в Fitch или, по крайней мере, где-то узнать, как это сделать, буду очень признателен за указание.

Предположим C. Соедините C и B, чтобы получить (C & B), что противоречит предпосылке 2. Заключите ~C. [здесь используются только следующие правила: &-Intro, Bottom/Absurd-Intro, ~-Elim].
Действительно, спасибо. Я только что понял это. Я сделал это намного сложнее, чем это было, сосредоточившись на дизъюнктивном исключении.
Вот пример с Де Морганом и в-Элимом: вставьте отрицание в посылку (2), чтобы получить (~C v ~B). Предположим ~С. Повторите, чтобы получить ~C. Предположим ~B, чтобы получить противоречие с посылкой (1) и заключить ~C. Так как ~C следует из обоих случаев, то по v-Elim следует, что ~C.
+1 Показывает исследовательские усилия, понятно и даже может быть полезно другим. Что не менее важно, он имеет соответствующие теги.

Ответы (3)

Вот несколько вариантов:

  • Если у вас есть правило двойного отрицания, вы можете превратить B в ~~B. Затем вы можете использовать правило дизъюнктивного силлогизма вместе с (~C v ~B), чтобы получить ~C.

  • Вы можете попробовать косвенное доказательство, где вы предполагаете C, а затем соединяете его с B, чтобы получить (C & B), что дает противоречие со строкой 2, влекущее за собой ~C.

Эй, спасибо за ответ! Проблема, с которой я сталкиваюсь, связана с отсутствием правила дизъюнктивного силлогизма. Единственный способ выполнить исключение v в Fitch — использовать Proof by Cases (где случаи являются дополнительными доказательствами). Если я использую косвенное доказательство и получаю (C & B), то все, что я могу сделать в рамках Fitch, — это ввести противоречие, из которого я могу вывести ~(C & D), но тогда я снова вернусь к тому, с чего начал. Обзор системы, в которой я работаю .
И.... Не обращайте на это внимания :). Я действительно решил это с помощью косвенного доказательства, не совсем уверенного, как я упустил из виду эту возможность. Я был настолько сосредоточен на использовании законов ДеМоргана в своем доказательстве, что заставил себя думать, что единственным способом продолжения является дизъюнктивное исключение. Спасибо!

Вот подход, который использует дизъюнктивное исключение. Учитывая следующее, я предполагаю, что правила ДеМоргана доступны:

Я могу расширить ~(C & B) до ~C ИЛИ ~B

введите описание изображения здесь

В строке 3 я использовал правила ДеМоргана (DeM), чтобы получить дизъюнктуру, которую затем мне нужно будет устранить, чтобы достичь цели.

Чтобы устранить дизъюнктуру, я должен рассмотреть обе дизъюнкции, «¬C» и «¬B».

Первый дизъюнкт самый простой, но он может сбивать с толку, потому что он очень простой. Предположение «¬C» для этого поддоказательства — это именно то, что я хочу показать. Делать больше нечего (по крайней мере, для этого средства проверки доказательств).

Второй дизъюнкт использует взрыв, основанный на наблюдении, что строки 1 и 5 противоречат друг другу. Это средство проверки доказательств позволяет мне сформулировать противоречие (⊥) в строке 6 и использовать взрыв (X) в строке 7, чтобы прийти к выводу, что я хочу "¬C". Тот, который вы используете, может потребовать чего-то другого.

Поскольку у меня один и тот же вывод для каждой дизъюнкции, я могу опровергнуть два предположения в строках 4 и 5, сославшись на правило устранения дизъюнкции (∨E). В этом средстве проверки доказательств я должен сослаться на саму дизъюнктуру (3), первое дополнительное доказательство (это всего лишь строка 4, но записанная как диапазон 4–4) и второе дополнительное доказательство (5–7).

использованная литература

Редактор и средство проверки естественной дедукции Кевина Клемента на JavaScript/PHP в стиле Fitch http://proofs.openlogicproject.org/

PD Магнус, Тим Баттон с дополнениями Дж. Роберта Лофтиса, ремикшированный и отредактированный Аароном Томасом-Болдуком, Ричардом Заком, forallx Calgary Remix: An Introduction to Formal Logic, зима 2018 г. http://forallx.openlogicproject.org/

Вам обещали B и ~(C ^ B). Если вы предполагаете C, вы можете вывести C ^ B из первой посылки, противоречащей второй посылке, что позволит вам снять допущение с помощью введения отрицания и, таким образом, вывести ~C по мере необходимости. Вот и все.

|  B           Premise
|_ ~(C ^ B)    Premise
|  |_ C        Assumption
|  |  C ^ B    Conjunction Introduction
|  |  #        Negation Elimination
|  ~C          Negation Introduction

Что ж, версия правила введения отрицания, которую использует ваша система, может различаться, но в основном это все.

|  B           Premise
|_ ~(C ^ B)    Premise
|  |_ C        Assumption
|  |  C ^ B    Conjunction Introduction
|  C->(C ^ B)  Conditional Introduction
|  |_ C        Assumption
|  |  ~(C ^ B) Reiteration
|  C->~(C ^ B) Conditional Introduction
|  ~C          Negation Introduction
Дизъюнктивный силлогизм в системе стилей Fitch
СпросиСетьПолитика конфиденциальности1y, 0v