Как доказать '∃xP(x)' из '¬∀x(P(x)→Q(x))'

Как бы выглядело официальное доказательство Fitch для этого?

Мне дано ¬∀x(P(x)→Q(x)), и мне нужно вывести из него ∃xP(x).

Я начал с этого, но я не знаю, правильно ли я поступаю, и куда идти дальше:

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

РЕДАКТИРОВАТЬ: сделал это (см. ответ)

Пока нет ответов, написанных на английском языке. Разве суть дела не в том, что если бы не было $x$ такого, что $P(x)$, то $P(x)$ было бы ложным для всех $x$ и, таким образом, подразумевало бы абсолютно все что угодно?

Ответы (4)

Решено! Я понял, что никуда не двигался, предполагая противоположное тому, что мне дали в качестве предпосылки... Я, очевидно, должен был предположить противоположное тому, что пытался доказать:

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

На самом деле. У вас есть правильное решение. Теперь вы можете принять свой собственный ответ, чтобы закрыть этот вопрос.

1) ¬∀x(P(x) → Q(x)) --- посылка

2) ¬∃xP(x) --- предполагается [a]

3) P(x) --- предполагается [b]

4) ∃xP(x) --- из 3) по ∃ -intro

5) ⊥ --- противоречие : из 2) и 4)

6) Q(x) --- из 5) на ⊥ -elim

7) P(x) → Q(x) --- из 3) и 6) по → -intro, разрядка [b]

8) ∀x(P(x) → Q(x)) --- из 7) с помощью ∀ -intro

9) ⊥ --- противоречие : из 1) и 8)

10) ∃xP(x) --- из 2) Двойным Отрицанием (или ¬ -elim ), сбрасывая [a].

Следующее доказательство такое же, как и доказательство Мауро АЛЛЕГРАНЦА, но в нем используется средство проверки доказательств Клемента в стиле Fitch. Описания правил есть в forallx . Оба доступны в Интернете и перечислены ниже. Они могут помочь в качестве дополнительного материала к тому, что вы сейчас используете.

В программе проверки доказательств вам может потребоваться представить противоречия как конъюнкцию противоречивых утверждений. Эта проверка проверки требует только отметить противоречие как «⊥» и перечислить противоречивые строки, как я сделал в строках 5 и 9.

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

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

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

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

Мне удалось это сделать, но мой результат немного отличается от вашего. Я попробовал ваш из любопытства, и он не работает в моей программе Fitch. Меня озадачивает тот факт, что ваша программа проверки доказательств позволила вам экспортировать временное предположение «а» за пределы его поддоказательства!
@ 35308 Вы можете посмотреть на это дополнительное доказательство (строки 3-6) как на то же самое, что и условное утверждение в строке 7 «Pa > Qa». Учитывая предположение Pa, я могу вывести Qa из того, что доступно (а именно из строки 2). Поддоказательство просто показало, как это было сделано, и средство проверки доказательств потребовало, чтобы я показал это, прежде чем использовать строку 7.
Проблема в том, что вам действительно не должно быть разрешено вводить новый свободный термин «а», не поднимая новый контекст, чтобы изолировать его.

Пр. ~∀x(P(x)->Q(x))

2. ∃x~(P(x)->Q(x)) ~ Universal out Pr.

3. ~(P(a)->Q(a)) Экзистенциальный out(x/a)2

4. P(a)&~Q(a) ~ условный выход 3

5. P(a) Соединение вых 4

6. ∃xP(x) Экзистенциальный In 5

Как доказать '∃xP(x)' из '¬∀x(P(x)→Q(x))'
СпросиСетьПолитика конфиденциальности1y, 0v