В fitch S → (R ∨ P), P → (¬R → Q) ∴ S → (Q ∨ R)

Другой подход состоит в том, чтобы предположить, что ~(Q ∨ R), как я сделал в строке 9 ниже. Это приводит к противоречию в строке 17, так что вы можете завершить другую половину дизъюнкции.

1 | (S→(R ∨ P)) Посылка
2 |_ (P→(~R→Q)) Посылка
3 | |_ S Предположение
4 | | (R ∨ P) 1,3 → E
5 | | |_ R Предположение
6 | | | (Q ∨ R) 5 ∨ I
7 | | |_ P Предположение
8 | | | (~R→Q) 2,7 →E
9 | | | |_ ~(Q ∨ R) Предположение
10 | | | | |_ ~R Предположение
11 | | | | | Q 8,10 →Э
12 | | | | | (Q ∨ R) 11 ∨ I
13 | | | | | ⊥ 9,12 ⊥I
14 | | | | ~~Р 10-13 ~Я
15 | | | | Р 14 ~Е
16 | | | | (Q ∨ R) 15 ∨ I
17 | | | | ⊥ 9,16 ⊥I
18 | | | ~~(Q ∨ R) 9-17 ~I
19 | | | (Q ∨ R) 18 ~E
20 | | (Q ∨ R) 4,5-6,7-19 ∨E
21 | (S → (Q ∨ R)) 3-20 → I

Намекать

Предположим S и выведите R ∨ P из 1-й посылки.

Теперь два поддоказательства для ∨ -elim:

1) Предположим , что R и вывести Q ∨ R с помощью ∨ -intro, и это сделано.

2) Предположим , что P и вывести ¬R → Q из 2-й посылки.

Теперь используйте R ∨ ¬R (исключенное среднее) для нового ∨ -elim:

2.1) Предположим, что R и вывести Q ∨ R .

2.2) Предположим , что ¬R и вывести Q из ¬R → Q, а затем вывести Q ∨ R .

Получив Q ∨ R в каждом случае, мы можем заключить:

S → (Q ∨ R)

по → -вступление.

Как и Pe, я сделал доказательство от противного... и сделав допущение ~(Q v R) ранее в доказательстве (и воспользовавшись упрощенным методом Fitch, позволяющим использовать ~ Intro, избавляясь от отрицания допущения), Я смог сбрить несколько строк:

Что мне действительно интересно в этом доказательстве, так это то, что поддоказательство, начинающееся с R, используется дважды: как доказательство от противного для вывода ~R, а также как доказательство по случаям для получения противоречия. Такое не часто увидишь.

Вот доказательство с использованием средства проверки доказательств в стиле Fitch .

Первые две строки содержат помещения.

Поскольку цель является условной, я предположил антецедент S в поддоказательстве, начинающемся в строке 3. Моя цель состояла в том, чтобы получить консеквент Q v R , что я и сделал в строке 13. Это позволило мне отбросить предположение и закрыть поддоказательство, введя условие для завершения доказательства.

Чтобы добраться до строки 13, я предположил отрицание того следствия, которое хотел доказать, начав новое поддоказательство. Я стремился найти противоречие, что и сделал в строке 12. Использование дизъюнктивного силлогизма (DS) в строке 8 позволило мне сократить проверку двух случаев дизъюнкции в строке 6.

---

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

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

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