¿Cómo seguirías demostrando la Ley del Medio Excluido con Cuantificadores?

Insinuación

Necesitamos LEM : ∀zP(z) ∨ ¬∀zP(z)

Prueba por casos (o ∨ -elim) :

1) ∀zP(z) --- asumido [a]

2) P(x) --- por ∀ -elim

3) ¬P(y) ∨ P(x) --- por ∨ -introducción

4) ∃y∀x (¬P(y) ∨ P(x)) --- por ∀ -introducción seguida de ∃ -introducción

5) ¬∀zP(z) --- asumido [b]

6) ∃z¬P(z) --- equivalente

7) ¬P(y) --- asumido [c] para ∃ -elim

8) ¬P(y) ∨ P(x) --- por ∨ -introducción

9) ∃y∀x (¬P(y) ∨ P(x)) --- ahora podemos descargar [c] por ∃ -elim de 6)

De 4) y 9) concluimos con :

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

por ∨ -elim con LEM .

---

Podemos "verificarlo" a través de algunas equivalencias. Considerar :

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

con él, podemos reescribir la fórmula original: ∃x ∀y (¬P (y) ∨ P (x)) como:

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

Entonces necesitamos la equivalencia:

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

y reescribimos la última fórmula como:

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

que a su vez es equivalente a:

¬ ∃y P (y) ∨ ∃x P (x) --- LEM .