Как бы вы продолжали доказывать закон исключенного третьего с помощью кванторов?

Намекать

Нам понадобится ЛЭМ : ∀zP(z) ∨ ¬∀zP(z)

Доказательство по случаям (или ∨ -elim):

1) ∀zP(z) --- предполагается [a]

2) P(x) --- по ∀ -elim

3) ¬P(y) ∨ P(x) --- по ∨ -intro

4) ∃y∀x (¬P(y) ∨ P(x)) --- с помощью ∀ -intro, за которым следует ∃ -intro

5) ¬∀zP(z) --- предполагается [б]

6) ∃z¬P(z) --- эквивалентно

7) ¬P(y) --- предполагается [c] для ∃ -elim

8) ¬P(y) ∨ P(x) --- по ∨ -intro

9) ∃y∀x (¬P(y) ∨ P(x)) --- теперь мы можем разрядить [c] по ∃ -elim из 6)

Из 4) и 9) заключаем:

∃y∀x (¬P(y) ∨ P(x))

на ∨ -elim с LEM .

---

Мы можем «проверить» его с помощью некоторых эквивалентностей. Рассмотреть возможность :

∀x (A ∨ P(x)) ↔ (A ∨ ∀x P(x)) ;

с ним мы можем переписать исходную формулу: ∃x ∀y (¬P (y) ∨ P (x)) как:

∃x (∀y ¬P (y) ∨ P (x)) .

Тогда нам нужна эквивалентность:

∃x (A ∨ P (x)) ↔ (A ∨ ∃x P(x))

и мы перепишем последнюю формулу как:

∀y ¬P (y) ∨ ∃x P (x))

что, в свою очередь, эквивалентно:

¬ ∃y P (y) ∨ ∃x P (x) --- ЛЭМ .