Доказательство естественной дедукции в помощь!

Более ранняя версия вопроса состояла из пяти частей:

1. ∀x(Px ∨ Q) ⊢ (∀xPx ∨ Q)
2. ∀xPx → Q ⊢ ∃x(Px → Q)
3. ∀x∀y(Rxy → ¬x = y) ⊢ ¬∃xRxx
4. ∀x(∃yPxy → ∀yPyx) ⊢ ∃x∃yPxy → ∀x∀yPxy
5. ∃x∃y∀z(x = z ∨ y = z) ⊢ ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))

В вопросе остается только часть 5.

---

Слишком много ...

Подсказка для 1) :

1) ∀x(Px ∨ Q) --- посылка

2) Px ∨ Q --- форма 1) по ∀-elim

3) ¬Q --- предполагается [а]

4) ∃x¬Px --- предполагается [б]

5) Q --- предполагается [c] из 2) для ∨-elim

6) ⊥ --- противоречие, из 3) и 5)

7) ¬¬Q --- из 3) и 6) по ¬-intro, разрядив [а]

8) Q --- из 7) по ¬¬-elim

9) ∀xPx ∨ Q --- из 8) by ∨-intro

10) Px --- предполагается [d] из 2) для ∨-elim

11) ¬Px --- предполагается [e] из 4) для ∃-elim

12) ⊥ --- противоречие, из 10) и 11) и разрядка [e] по ∃-elim

13) ¬∃x¬Px --- из 4) и 12) по ¬-intro, разрядка [b]

14) ∀Px --- из 13) с помощью подвывода ¬∃x¬ ⊢∀x : предположим ¬Px, а затем ∃x¬Px по ∃-введению. С противоречием и двойным отрицанием выведите Px, отбросив предположение, и заключите с ∀xPx с помощью ∀-введения.

15) ∀Px ∨ Q --- из 14) by ∨-intro

16) ∀Px ∨ Q --- из 2) и 5)-9) и 10)-15) через ∨-elim, разряжая [c] и [d].

---

---

Подсказка для 2):

1) ∀xPx → Q --- посылка

2) Рх --- предполагается [а]

3) ∃x¬Px --- предполагается [б]

4) ¬Px --- предполагается [c] из 3) для ∃-elim

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

6) ⊥ --- из 3), 4) и 5) по ∃-elim, разгружая [c]

7) ¬∃x¬Px --- из 3) и 6) по ¬¬-элим, разрядка [б]

8) ∀Px --- из 7) с помощью подвывода ¬∃x¬ ⊢∀x

9) Q --- из 1) и 8) по →-elim

10) Px → Q$ --- из 2) и 9) по →-вступлению, разрядив [а]

11) ∃x(Px → Q) --- из 10) по ∃-введению.

---

---

Подсказка для 3) :

1) ∀x∀y(Rxy → ¬x = y) --- посылка

2) Rxx --- предполагается [а]

3) Rxx → ¬ x = x --- из 1 на ∀-elim

4) ¬ x = x --- из 2) и 3) по →-elim

5) х = х --- аксиома равенства

6) ¬Rxx --- от 2) и противоречие, по ¬-вступлению, разрядив [а]

7) ∀x¬Rxx --- из 6) by ∀-intro

Теперь нам нужно добавить подвывод: ∀x¬ ⊢ ¬∃x.

---

---

Последнее долго и нудно, но довольно просто.

Подсказка для 5):

1) ∃x∃y∀z(x = z ∨ y = z) --- посылка

2) ¬∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) --- предполагаем отрицание вывода и ищем противоречие: если найдено, результат будет ¬¬ -элим

3) ∀z(a = z ∨ b = z) --- предполагается из 1) для ∃-elim дважды

4) ∃x∃y ¬(¬x = y → ∀z(x = z ∨ y = z)) --- из 2), снова играя с эквивалентностью кванторов

5) ¬(¬c = d → ∀z(c = z ∨ d = z)) --- предполагается из 4) для ∃-elim дважды

6) ¬c = d ∧ ¬∀z(c = z ∨ d = z) --- из 6) по тавтологической эквивалентности

7) ¬c = d --- из 6) на ∧-elim

8) ¬∀z(c = z ∨ d = z) --- из 6) на ∧-elim

9) ∃z ¬(c = z ∨ d = z) --- из 9) снова по кванторной эквивалентности

10) ¬(c = e ∨ d = e) --- предполагается из 9) для ∃-elim

11) ¬c = e ∧ ¬d = e --- из 10) по тавтологической эквивалентности

12) ¬c = e --- из 11) на ∧-elim

13) ¬d = e --- из 11) на ∧-elim

Теперь нам нужно создать экземпляр 3) ∀z(a = z ∨ b = z) трижды с c, d, e соответственно, чтобы получить:

14) а = с ∨ б = с

15) а = d ∨ б = d

16) а = е ∨ б = е

и тонко получить желаемое противоречие с 7), 12) и 13) (простое, но скучное применение ∨-elim).

Что мы получаем:

20) ⊥

который закрывает все вышеперечисленные ∃-элимы, снимая соответствующие предположения.

21) ∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) --- из 2) и 20) по ¬¬-выд.

Более ранняя версия вопроса состояла из пяти частей:

1. ∀x(Px ∨ Q) ⊢ (∀xPx ∨ Q)
2. ∀xPx → Q ⊢ ∃x(Px → Q)
3. ∀x∀y(Rxy → ¬x = y) ⊢ ¬∃xRxx
4. ∀x(∃yPxy → ∀yPyx) ⊢ ∃x∃yPxy → ∀x∀yPxy
5. ∃x∃y∀z(x = z ∨ y = z) ⊢ ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))

В вопросе остается только часть 5.

---

Специфика вашего доказательства будет зависеть от того, как именно система доказательств, с которой вы работаете, определила правила.

Вот доказательства для 1), 2), 3) и 4) с использованием системы доказательств Fitch, как определено в Language, Proof, and Logic (это книга и программный пакет):

Для 5) вам явно нужно сделать ∃ Elim в предпосылке и ∀ Intro для заключения. Для этой задачи на самом деле не имеет значения, в каком порядке вы их выполняете. То есть вы можете настроить это так:

или вот так:

Хорошо, давайте просто работать с последним. Теперь, поскольку мы ищем еще одну ∀, мы сделаем еще одну ∀. Вступление:

Теперь, чтобы получить эту дизъюнктию, мы проведем доказательство с помощью противоречия. Почему? Потому что, если вы подумаете об этой проблеме концептуально: мы знаем, что каждый объект равен либо a, либо b (или обоим, поскольку a и b могут быть одним и тем же объектом). Итак, мы знаем, что в домене не более двух объектов. Поэтому вывод имеет смысл: если есть два различных объекта c и d, то все должно равняться либо тому, либо другому. Хорошо, но как это доказать? Ну, возьмем любой предмет e. Мы знаем, что e равно a или b или тому и другому. Теперь, как правило, когда вы переходите от дизъюнкции P v Q к дизъюнкции R v S, вы можете проследить одну из дизъюнктов, которые вы хотите (R), до одной из дизъюнкций, которые у вас есть (скажем, Q), в то время как другая дизъюнкция вас желание (S) происходит от другого, которое у вас есть (P). Итак, вы можете сделать Доказательство по падежам (v Elim), чтобы сделать это. Но здесь эта стратегия не сработает: если e = a, можем ли мы сказать, что e = c? Нет. И не то, что e = d. Да, это определенно должно быть одно или другое, но мы просто не можем сказать, какое именно. Итак, прямое доказательство по случаям не сработает. Что ж, в этом случае используйте другую распространенную стратегию для доказательства дизъюнкции: Доказательство противоречием:

Хорошо, и теперь это должно быть довольно просто. Мы знаем, что c, d и e — это a или b, и теперь нужно просто пройти через все эти дизъюнкции, каждый раз доказывая противоречие. Вот базовая настройка:

А вот и половина проработана:

Утомительно, но довольно просто. Удачи!

Предпосылка гласит, что в домене ∃x∃y∀z(x = z ∨ y = z)существует не более двух различных значений.

Вывод ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))гласит, что для любых двух различных значений в области не существует третьего.

Ясно, что нам нужно использовать экзистенциальное устранение и универсальное введение.

∃-elim здесь будет сложно.

«Хитрость» заключается в использовании пяти предполагаемых терминов. Два термина в качестве свидетелей для экзистенциальных исключений ( a, b) и три произвольных термина для введений ( c, d, e).

Чтобы доказать вывод из посылки: возьмем свидетеля для посылки (предположим aи bгде ∀z(a = z ∨ b = z), возьмем произвольные значения ( c, d, и e) и (используя универсальное исключение для каждого) покажем, что когда b, и cсчитаются различными, следует, что eдолжно быть тот или иной из них с помощью некоторых вложенных исключений дизъюнкции (и исключений равенства).

Короче говоря: Так как (a = c ∨ b = c), (a = d ∨ b = d), и (a = e ∨ b = e)через универсальное исключение, поэтому(c = e ∨ d = e)

---

Вкратце: это утомительно и повторяется, но...

    |_ ∃x∃y∀z(x = z ∨ y = z)                P
    |  |_ [a,b] ∀z(a = z ∨ b = z)           H
    |  |  |_ [c,d]                          H
    |  |  |  a = c ∨ b = c                 ∀E
    |  |  |  a = d ∨ b = d                 ∀E
    |  |  |  |_ ¬c = d                      H
    |  |  |  |  |_ [e]                      H
    |  |  |  |  |  a = e ∨ b = e           ∀E
    |  |  |  |  |  |_ a = e                 H
    |  |  |  |  |  |  |_ a = c              H
    |  |  |  |  |  |  |  c = e             =E
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨I
    |  |  |  |  |  |  +
    |  |  |  |  |  |  |_ b = c              H
    |  |  |  |  |  |  |  |_ a = d           H
    |  |  |  |  |  |  |  |  d = e          =E
    |  |  |  |  |  |  |  |  c = e ∨ d = e  ∨I
    |  |  |  |  |  |  |  +
    |  |  |  |  |  |  |  |_ b = d           H
    |  |  |  |  |  |  |  |  c = d          =E
    |  |  |  |  |  |  |  |  #              ¬E
    |  |  |  |  |  |  |  |  c = e ∨ d = e   X
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨E
    |  |  |  |  |  |  c = e ∨ d = e        ∨E
    |  |  |  |  |  +
    |  |  |  |  |  |_ b = e                 H
    |  |  |  |  |  |  |_ a = c              H
    |  |  |  |  |  |  |  |_ a = d           H
    |  |  |  |  |  |  |  |  c = d          =E
    |  |  |  |  |  |  |  |  #              ¬E
    |  |  |  |  |  |  |  |  c = e ∨ d = e   X
    |  |  |  |  |  |  |  +
    |  |  |  |  |  |  |  |_ b = d           H
    |  |  |  |  |  |  |  |  d = e          =E
    |  |  |  |  |  |  |  |  c = e ∨ d = e  ∨I
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨E
    |  |  |  |  |  |  +
    |  |  |  |  |  |  |_ b = c              H
    |  |  |  |  |  |  |  c = e             =E
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨I
    |  |  |  |  |  |  c = e ∨ d = e        ∨E
    |  |  |  |  |  c = e ∨ d = e           ∨E
    |  |  |  |  ∀z (c = z ∨ d = z)         ∀I
    |  |  |  ¬c = d → ∀z (c = z ∨ d = z)   →I
    |  |  ∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) ∀I 
    |  ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))    ∃E