Wie würden Sie weiter das Gesetz der ausgeschlossenen Mitte mit Quantoren beweisen?

Hinweis

Wir brauchen LEM : ∀zP(z) ∨ ¬∀zP(z)

Beweis durch Fälle (oder ∨ -elim) :

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

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

3) ¬P(y) ∨ P(x) --- von ∨ -intro

4) ∃y∀x (¬P(y) ∨ P(x)) --- durch ∀ -Intro gefolgt von ∃ -Intro

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

6) ∃z¬P(z) --- Äquivalent

7) ¬P(y) --- angenommen [c] für ∃ -elim

8) ¬P(y) ∨ P(x) --- von ∨ -intro

9) ∃y∀x (¬P(y) ∨ P(x)) --- jetzt können wir [c] um ∃ -elim aus 6) entladen

Von 4) und 9) schließen wir mit:

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

durch ∨ -elim mit LEM .

---

Wir können es durch einige Äquivalenzen "verifizieren". Erwägen :

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

damit können wir die ursprüngliche Formel : ∃x ∀y (¬P (y) ∨ P (x)) umschreiben als :

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

Dann brauchen wir die Äquivalenz:

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

und wir schreiben die letzte Formel um als:

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

was wiederum äquivalent ist zu:

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