Доказательство отрицания универсальной квантификации

Вы допустили ошибку на шаге 6. Nr. 3 - это не универсальная квантификация, это отрицание (¬ находится вне ∀). Следовательно, вы не можете устранить ∀.

Вместо этого вам нужно устранить ¬. Если вы хотите исключить ¬из ¬p , вы предполагаете p , а затем работаете над противоречием. Итак, вы получаете:

6. Предположим, что ∀x(¬S(x))

Теперь вы можете исключить ∀ на x0:

7. ¬S(x0)

Это в сочетании с 5 дает нам

8. Р(х0)

Но это противоречит 4. Следовательно, предположение в 6 было неверным, и, следовательно, должно выполняться ¬∀x(¬S(x)).

Рассмотрим следующий аргумент

∀x(R(x) ∨ S(x)), ∃x(¬R(x)) ⊦ ¬∀x(¬S(x))

Моя стратегия состоит в том, чтобы попытаться доказать, что ∀x(¬S(x)) является противоречием и, следовательно, ¬∀x(¬S(x)) должно быть истинным.

Хорошая стратегия! Доказательство отрицанием.

Мое решение до сих пор

1. | ∀x(R(x) ∨ S(x)) Посылка

2. |_ ∃x(¬R(x)) Посылка

3. | |_ ¬∀x(¬S(x)) Предположение

Что случилось с вашей стратегией предположения ∀x(¬S(x)) ? Вот где вы должны сделать это. Также здесь вы поднимаете первое предположение. (Первые два являются предпосылками.)

3. | |_ ∀x(¬S(x)) Предположение

4. | | |_ x0 ¬R(x0) ∃e 2
5. | | | R(x0) ∨ S(x0) ∀e 1
6. | | | ¬¬S(x0) ∀e 3

Нет, вы не можете исключить универсальный квантор в ¬∀x(¬S(x)) и получить ¬¬S(x0). Отрицание имеет приоритет. Кроме того, поскольку в любом случае вы должны были принять ∀x(¬S(x)) в строке , мы просто исправим строку 6, и это действительно должно было быть предположением в блоке: это свидетельство универсальности, которую мы ищем. отрицать.

4. | | |_ [x0] ¬S(x0) ∀e 3
5. | | | ¬R(x0) ∃ e 2
6. | | | R(x0) ∨ S(x0) ∀e 1

7. | | | |_ R(x0) Предположение
8. | | | | ⊥ ¬e 5, 7
9. | | | | ¬S(x) ⊥e 8

Хорошо. Вы настраиваете вещи на устранение дизъюнкции. Просто оставьте его на восьмой строке.

7. | | | |_ R(x0) Предположение
8. | | | | ⊥ :¬e 5, 7
9. | | | R(x0) → ⊥ :→i 7-8
10. | | | |_ S(x0): предположение
11. | | | | ⊥ :¬e 4, 10
12. | | | S(x0) → ⊥ : →i 10-11
13. | | | ⊥ :∨e 6, 9, 12
14. | | ⊥ :[]е 4-13
15. | ¬∀x (¬S(x)) :¬i 3-14

Возникает вопрос: «Как можно работать с отрицанием кванторов в сценариях, подобных описанному выше?»

Я приведу два доказательства, которые могут помочь ответить на вопрос. Первым будет косвенное доказательство, аналогичное попытке в ОП. Второй будет более прямым.

Вот первое доказательство:

Помещения находятся на первых двух линиях. В третьей строке я допускаю отрицание того, что хочу показать, чтобы получить противоречие. Я достиг желаемого противоречия в строке 9, что приводит к завершению доказательства в строке 10.

В строке 4 я использую вторую предпосылку. В строке 5 я использую первую предпосылку. Они быстро порождают противоречие.

Второе доказательство более прямое.

Первые две строчки являются предпосылкой. В строке 3 я запускаю процесс для завершения экзистенциального исключения. Чтобы сделать это, я должен сделать допущение, которое будет выполнено в строке 15, допуская экзистенциальное исключение.

Используя первую посылку, я рассматриваю два случая «Ра» и «Са». Я хочу, чтобы оба случая дали мне (1) один и тот же результат и (2) результат, который я могу использовать. Результат, который я хочу, это "¬¬Sa". Наличие этих двойных отрицаний позволяет мне ввести квантор существования, а затем с помощью преобразования кванторов переместить одно из этих отрицаний за пределы универсального квантора.

Для получения дополнительной информации о том, как работают эти правила, связанные с используемой мной проверкой проверки, см. forall x: Calgary Remix .

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

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

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