Wie kann ich ⊢(∀x)(Fx V ~Fx) mit natürlichem Abzug beweisen?

Es hängt von den Regeln ab, die Sie verwenden dürfen ...

Hier ist ein Beweis mit der Eliminierung der doppelten Negation:

1) ¬ (Fx ∨ ¬Fx) --- angenommen [a]

2) Fx --- angenommen [b]

3) Fx ∨ ¬Fx --- aus 2) von ∨-Intro

4) ⊥ --- aus 1) und 3)

5) ¬Fx --- aus 2) und 4) per ¬-Intro, Entladung [b]

6) Fx ∨ ¬Fx --- aus 5) von ∨-Intro

7) ⊥ --- aus 1) und 6)

8) Fx ∨ ¬Fx --- aus 1) und 7) durch ¬¬-elim, Entladung [a]

9) ∀x (Fx ∨ ¬Fx) --- aus 8) durch ∀-Intro

Hier ist ein formaler Beweis in Fitch:

Die Frage ist: ⊢(∀x)(Fx V ~Fx) Wie kann ich das mit natürlichem Schluss beweisen?

Ich werde zwei Beweise liefern, einen indirekten und einen direkten.

Der indirekte Beweis verwendet Konversion von Quantoren (CQ), die De-Morgan-Regel (DeM), doppelte Negationseliminierung (DNE), indirekten Beweis (IP) sowie Einführungs- und Eliminationsregeln.

Der nächste Beweis verwendet das Gesetz des ausgeschlossenen Dritten (LEM). Es mag den Anschein haben, als wollten wir das zeigen, aber die Frage scheint eher zu sein, ob wir angesichts des Gesetzes der ausgeschlossenen Mitte die universelle Einführungsregel anwenden können.

Weitere Informationen und Beispiele zur Verwendung dieser Regeln finden Sie unter forall x: Calgary Remix .

Verweise

Kevin Klements JavaScript/PHP-Beweiseditor und -prüfer im Fitch-Stil für natürliche Deduktion http://proofs.openlogicproject.org/

PD Magnus, Tim Button mit Ergänzungen von J. Robert Loftis, remixt und überarbeitet von Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/