<=> — биусловный, «-» — отрицание, «v» — дизъюнкция.
Я не могу понять, где взять это из строки 4. Отрицательное Q бросает меня в петлю.
P <=> (Q v R), P, -Q ⊢ R
Учитывая 3 и 4, нормальным ходом является дизъюнктивный силлогизм, который позволяет:
Это даст:
Если у вас нет доступа к дизъюнктивному силлогизму, сделать это будет намного сложнее.
Обычно при наличии дизъюнкции приходится использовать правило устранения дизъюнкции. Поэтому, когда вы видите это, вы должны подумать, как это правило может привести вас к заключению.
В этом случае нам понадобится следующее:
1. Q v R
2. Q → R
3. R → R
Используя устранение дизъюнкции, вы получите R
. У вас уже есть 1, а 3 тривиально. Итак, нам нужно выяснить, как получить 2. Это можно сделать следующим хитрым способом:
1. ~Q
2. | Q
3. | | ~R
4. | | ~Q
5. | | Q
6. | | Q & ~Q
7. | ~~R
8. | R
9. Q → R
Теперь у вас есть все 3 утверждения, необходимые для правила устранения дизъюнкции, которое приведет вас к R
.
Я согласен с ответом Вирмайора , использующим дизъюнктивный силлогизм (ДС). Вот как программа проверки доказательств Кевина Клемента форматирует доказательство, используя дизъюнктивный силлогизм:
Дизъюнктивный силлогизм получен из исключения дизъюнкции (vE). Вот доказательство с использованием исключения дизъюнкции, иллюстрирующее вывод дизъюнктивного силлогизма из исключения дизъюнкции, данное в forall x: Calgary Remix (стр. 137):
Обратите внимание, как это использует введение соединения «R» с самим собой в строке 9, а затем удаление соединения в строке 10, чтобы снова получить «R». Правила этого средства проверки доказательств устраняют необходимость в этих шагах.
Вот третья версия доказательства:
В ОП те же первые четыре строки и говорится: «Я не могу понять, где взять это из строки 4». Выше показано три способа действий, и их может быть больше в зависимости от используемой программы проверки доказательств.
использованная литература
Редактор и средство проверки естественной дедукции Кевина Клемента на JavaScript/PHP в стиле Fitch http://proofs.openlogicproject.org/
PD Магнус, Тим Баттон с дополнениями Дж. Роберта Лофтиса, ремикшированный и отредактированный Аароном Томасом-Болдуком, Ричардом Заком, forallx Calgary Remix: An Introduction to Formal Logic, зима 2018 г. http://forallx.openlogicproject.org/
вирмайор
Майкл Фоллетт
вирмайор