Как в Fitch можно доказать «P» из посылки «(¬P ∨ Q)→P»?

Как в Fitch можно доказать «P» из посылки «(¬P ∨ Q)→P»?

Один предполагает не-P и использует доказательство сведения к абсурду.

|_ (~P v Q) -> P   Premise
|  |_ ~P           Assumption
|  |  :            :
|  |  :            :
|  |  :            :
|  ~~P             Negation Introduction
|  P               Double Negation Elimination

Вот способ доказать это, используя правила проверки Клемента в стиле Fitch. Правила описаны в forallx . Оба доступны по ссылкам ниже и станут хорошим дополнительным материалом к ​​любому тексту, который вы используете.

Это доказательство использует закон исключенного третьего (LEM). Чтобы использовать это, я беру простое утверждение и его отрицание и пытаюсь вывести из обоих один и тот же результат. Если я получу тот же результат, то смогу применить закон исключенного третьего. Здесь я выбрал «P» и «¬P», потому что одно из них, «P», является самой целью.

Для «P» мне ничего не нужно делать, кроме как добавить поддоказательство с предположением «P». Для «¬P» я использую введение дизъюнкции, чтобы получить строку 4, а затем условное исключение в строке 5 (modus ponens), чтобы получить «P». Я достиг цели «P» в обоих случаях, поэтому я могу выполнить два предположения в строках 2 и 3 и дойти до конца доказательства.

Ссылка

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

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