P <=> (Q v R), P, -Q⊢R Вопрос пропозициональной логики

<=> — биусловный, «-» — отрицание, «v» — дизъюнкция.

Я не могу понять, где взять это из строки 4. Отрицательное Q бросает меня в петлю.

P <=> (Q v R), P, -Q ⊢ R

  1. P <=> (Q v R) P
  2. ПП
  3. -QP/R
  4. QvR 1,2<=>E (правило двухусловного исключения, удаляющее P)
Не уверен, почему вы отредактировали его обратно. Все, что я сделал, это отформатировал его.
Точка обозначает его в другой контекстуальной основе, но он исчезает, если его нет, что странно.
Не уверен, что вы подразумеваете под «другой контекстной основой» как таковой, но синтаксис уценки SE довольно придирчив. Если вы действительно хотите избежать . в списке, вы можете использовать предварительно отформатированный синтаксис.

Ответы (3)

Учитывая 3 и 4, нормальным ходом является дизъюнктивный силлогизм, который позволяет:

  1. А против Б
  2. ~ А
  3. Поэтому Б

Это даст:

  1. Р ДС 3,4

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

У меня пока нет доступа к дизъюнктивным силлогизмам, это наш следующий модуль.
у вас есть доступ к условным доказательствам или доведению до абсурда?
У нас есть доступ только к введению и устранению конъюнкции, условному введению и устранению, повторению, введению и устранению отрицания, введению и устранению дизъюнкции и двуусловному введению и устранению.
условное введение является синонимом условного доказательства ( факультет.вашингтон.эду/смкоэн /120/Chapter8.pdf )
Насколько я понимаю, в этом курсе мы используем широкий спектр синонимов, потому что вещи называются немного по-разному, когда я их исследую. Но да.
Кроме того, это Кьеркегор на твоей аватарке?
да - это действительно большая и раздражающая особенность логики. И да. Я исследователь современной философии. Попытка придумать, как это сделать, используя только список того, что у вас есть.
Я очень ценю, что вы нашли время, чтобы помочь мне с этим. Подумал, что это ниже твоего статуса.
Интернет - невероятное место для траты времени :). Если у вас есть противоречие с введением и устранением, у Reddit есть способ ( reddit.com/r/logic/comments/1sukq6/… )
Единственная проблема заключается в том, что мы еще не узнали о введении и устранении противоречия.

Обычно при наличии дизъюнкции приходится использовать правило устранения дизъюнкции. Поэтому, когда вы видите это, вы должны подумать, как это правило может привести вас к заключению.

В этом случае нам понадобится следующее:

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.

Предполагая, что ему разрешено делать шаг 7, но это не совсем ясно.

Я согласен с ответом Вирмайора , использующим дизъюнктивный силлогизм (ДС). Вот как программа проверки доказательств Кевина Клемента форматирует доказательство, используя дизъюнктивный силлогизм:

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

Дизъюнктивный силлогизм получен из исключения дизъюнкции (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/