Любое решение для доказательства (∀x)(∃y)(Fx & Gy) ⊢ (∃y)(∀x)(Fx & Gy) с естественной дедукцией?

Сначала посмотрим, в каких случаях верна первая формула. Поскольку конъюнкция требует, чтобы оба операнда были истинными, мы знаем (путем упрощения):

(∀x)(Fx)

Это означает

Fx ⇔ 1

Теперь, поскольку Fx всегда истинно, мы получаем

(Fx и Гр) ⇔ (1 и Гр) ⇔ (Гр)

и

(∀x)(∃y)(Fx & Gy) ⇔ (∃y)(Gy)

а также

(∃y)(∀x)(Fx & Gy) ⇔ (∃y)(Gy)

Следовательно

(∀x)(∃y)(Fx и Gy) ⇔ (∃y)(∀x)(Fx и Gy)

Выводимость следует из эквивалентности (но не обязательно наоборот):

(∀x)(∃y)(Fx и Gy) ⊢ (∃y)(∀x)(Fx и Gy)

Это иллюстрация того факта, что если все предикаты принимают только один аргумент (т.е. F(x), G(y)), это может быть сведено к проблеме сентенциальной логики.

Если вы хотите сделать это шаг за шагом, вам нужны только правила «нерелевантности» — область действия квантификатора не обязательно должна включать какие-либо конъюнкты, которые не используют переменную.

(∀x)(∃y)(Fx & Gy) ⊢ Нерелевантный квантор

(∀x)(Fx & (∃y) Gy) ⊢ Нерелевантный квантор

(∀x) Fx & (∃y) Gy ⊢ Нерелевантный квантификатор (обратите внимание, что это действительно сентенциальное выражение)

(∃y)((∀x) Fx & Gy) ⊢ Нерелевантный квантор

(∃y)(∀x)(Fx и Gy)

Вот один из способов доказать результат:

Я пытаюсь косвенно доказать (IP), отрицая то, что хочу показать в строке 2. В строке 23 я наконец прихожу к противоречию (⊥). В процессе этого я использую правило преобразования кванторов (CQ), правило Де Моргана (DeM) и дизъюнктивный силлогизм (DS), а также правила введения и исключения.

Для получения дополнительной информации об этих правилах, связанных с проверкой проверки, которую я использовал, см. 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/

Вы можете использовать правила введения и исключения, чтобы доказать «нерелевантность квантификатора» в непустых вселенных.

|_ Ɐx Ǝy (Fx & Gy)
|  |_ [a]
|  |  Ǝy (Fa & Gy)
|  |  |_ [b] Fa & Gb
|  |  |  Fa
|  |  Fa
|  Ɐx Fx
|  |_ [a]
|  |  Ǝy (Fa & Gy)
|  |  |_ [b] Fa & Gb
|  |  |  Gb
|  |  |  |_ [c]
|  |  |  |  Fc
|  |  |  |  Fc & Gb
|  |  |  Ɐx (Fx & Gb)
|  |  Ǝy Ɐx (Fx & Gy)
|  Ǝy Ɐx (Fx & Gy)

И аналогично для обратного.