Справка Fitch «Доказательство от противоречия»

Правила вывода названы так, как они есть, не просто так.

Когда вы почувствуете необходимость поднять контекст, чтобы вывести цель, определите, какое правило введения вам понадобится, чтобы вывести цель. Это подскажет вам, какое допущение вам, возможно, потребуется сделать, и какой вывод вам нужно будет сделать .

• Когда цель является условной, например, Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b)), используйте условное введение . Примите антецедент и выведите консеквент .

• Когда целью является отрицание, например ~(StrongPref(b,a) v StrongPref(a,b)), используйте введение отрицания . Предположим положительное и получим противоречие.

Достигнув цели, не полученной с помощью правила введения, обратите внимание на допущения (и предпосылки) правил исключения , чтобы заполнить выводы.

• Когда вы предполагаете дизъюнктуру, например StrongPref(b,a) v StrongPref(a,b), используйте устранение дизъюнкции . Предположим, что каждый случай по порядку, и вывести одно и то же следствие.

Я оставлю вывод противоречия вам (но ладно, посылки 3 и 4 наиболее полезны).

|  Ɐx Ɐy StrongPref(x,y) ↔ ~WeakPref(y,x) 
|  Ɐx Ɐy Indiff(x,y) → WeakPref(y,x) ^ WeakPref(x,y)
|  |_ [a]
|  |  |_ [b]
|  |  |  |_ Indiff(a,b)
|  |  |  |  :
|  |  |  |  |_ StrongPref(b,a) v StrongPref(a,b)
|  |  |  |  |  |_ StrongPref(b,a)
|  |  |  |  |  |  :
|  |  |  |  |  |  #
|  |  |  |  |  +
|  |  |  |  |  |_ StrongPref(a,b)
|  |  |  |  |  |  :
|  |  |  |  |  |  #
|  |  |  |  |  #
|  |  |  |  ~(StrongPref(b,a) v StrongPref(a,b))
|  |  |  Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b))
|  |  :

Изменить: завершенное доказательство

:
|  Ɐx Ɐy StrongPref(x,y) ↔ ~WeakPref(y,x) 
|_ Ɐx Ɐy Indiff(x,y) → WeakPref(y,x) ^ WeakPref(x,y)
|  |_ [a]                                                   Arbitrary Term
|  |  |_ [b]                                                Arbitrary Term
|  |  |  |_ Indiff(a,b)                                     Assumption
|  |  |  |  Ɐy Indiff(a,y) → WeakPref(y,a) ^ WeakPref(a,y)  Universal Elimination
|  |  |  |  Indiff(a,b) → WeakPref(b,a) ^ WeakPref(a,b)     Universal Elimination
|  |  |  |  WeakPref(b,a) ^ WeakPref(a,b)                   Conditional Elimination
|  |  |  |  WeakPref(b,a)                                   Conjunction Elimination 
|  |  |  |  WeakPref(a,b)                                   Conjunction Elimination
|  |  |  |  |_ StrongPref(b,a) v StrongPref(a,b)            Assumption
|  |  |  |  |  |_ StrongPref(b,a)                           Assumption
|  |  |  |  |  |  Ɐy StrongPref(b,y) ↔ ~WeakPref(y,b)       Universal Elimination
|  |  |  |  |  |  StrongPref(b,a) ↔ ~WeakPref(a,b)          Universal Elimination
|  |  |  |  |  |  ~WeakPref(a,b)                            Biconditional Elimination
|  |  |  |  |  |  #                                         Negation Elimination
|  |  |  |  |  +
|  |  |  |  |  |_ StrongPref(a,b)
|  |  |  |  |  |  Ɐy StrongPref(a,y) ↔ ~WeakPref(y,a)       Universal Elimination
|  |  |  |  |  |  StrongPref(a,b) ↔ ~WeakPref(b,a)          Universal Elimination
|  |  |  |  |  |  ~WeakPref(b,a)                            Biconditional Elimination
|  |  |  |  |  |  #                                         Negation Elimination
|  |  |  |  |  #                                            Disjunction Elimination
|  |  |  |  ~(StrongPref(b,a) v StrongPref(a,b))            Negation Introduction
|  |  |  Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b)) Conditional Introduction
|  |  Ɐy Indiff(a,y) → ~(StrongPref(y,a) v StrongPref(a,y)) Universal Introduction
|  Ɐx Ɐy Indiff(x,y) → ~(StrongPref(y,x) v StrongPref(x,y)) Universal Introduction

Вот доказательство с использованием другого средства проверки доказательств. Я также сделал некоторые замены.

• Для Indiff я использовал I .
• Для StrongPref я использовал S .
• Для WeakPref я использовал W .

Из четырех помещений я использовал только третье и четвертое.

Вот опасения:

Теперь я зашел так далеко в доказательстве, но я не уверен, что то, что я делаю, неправильно, поскольку я больше не могу использовать универсальные экземпляры. Точно так же я не могу найти противоречие, требуемое для ~(StrongPref(b,a) v StrongPref(a,b)).

Я столкнулся с проблемой также и с универсальными экземплярами или введениями, но у меня было две отдельные предпосылки, на которых я использовал универсальное исключение. Я не связывал переменные в универсальных утверждениях с одинаковыми именами в этих двух предпосылках. Другими словами, то, что я связал «х» с «а» в четвертой посылке, не означает, что я не могу связать «х» с «б» в третьей посылке. Аналогично для «у». «x» и «y» являются переменными и могут обозначать любые имена, поскольку это универсальные количественные переменные. Можно использовать любое имя.

В частности, чтобы исключить квантор всеобщности «x» в посылке 4, я заменил переменную «x» на имя «a» в строке 5. Затем я устранил квантор всеобщности «y» в строке 5, заменив переменную «у» с именем «б». Получилась строка 6.

Однако в строке 9 я использовал универсальное исключение по предпосылке 3, заменив «x» на «b» (а не «a»). В строке 10 я использовал универсальное исключение в строке 9 и заменил «y» на «a» (не «b»).

Чтобы ввести отрицание в 15, я предположил, что «Sba» в строке 11, убрал биусловие в строке 12, исключил союз в строке 13 и получил противоречие в строке 14. Это противоречие позволило мне вывести «¬Sba» в строке. 15.

Рекомендации

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

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