Irgendeine Lösung, um (∀x)(∃y)(Fx & Gy) ⊢ (∃y)(∀x)(Fx & Gy) mit natürlichem Abzug zu beweisen?

Schauen wir uns zunächst an, in welchen Fällen die erste Formel zutrifft. Da die Konjunktion erfordert, dass beide Operanden wahr sind, wissen wir (durch Vereinfachung):

(∀x)(Fx)

Das heisst

Fx ⇔ 1

Nun, da Fx immer wahr ist, erhalten wir

(Fx & Gy) ⇔ (1 & Gy) ⇔ (Gy)

und

(∀x)(∃y)(Fx & Gy) ⇔ (∃y)(Gy)

ebenso gut wie

(∃y)(∀x)(Fx & Gy) ⇔ (∃y)(Gy)

Deshalb

(∀x)(∃y)(Fx & Gy) ⇔ (∃y)(∀x)(Fx & Gy)

Die Ableitbarkeit folgt aus der Äquivalenz (aber nicht unbedingt das Gegenteil):

(∀x)(∃y)(Fx & Gy) ⊢ (∃y)(∀x)(Fx & Gy)

Dies ist eine Illustration der Tatsache, dass, wenn alle Prädikate nur ein Argument haben (dh F(x), G(y) ), dies auf ein Problem in der Satzlogik reduziert werden kann .

Wenn Sie es Schritt für Schritt tun möchten, brauchen Sie nur die „Irrelevanz“-Regeln – der Gültigkeitsbereich eines Quantifizierers muss keine Konjunktionen enthalten, die die Variable nicht verwenden.

(∀x)(∃y)(Fx & Gy) ⊢ Irrelevanter Quantor

(∀x)(Fx & (∃y) Gy) ⊢ Irrelevanter Quantor

(∀x) Fx & (∃y) Gy ⊢ Irrelevanter Quantor (beachten Sie, dass dies wirklich ein Satzausdruck ist )

(∃y)((∀x) Fx & Gy) ⊢ Irrelevanter Quantor

(∃y)(∀x)(Fx & Gy)

Hier ist eine Möglichkeit, das Ergebnis zu beweisen:

Ich versuche einen indirekten Beweis (IP), indem ich in Zeile 2 negiere, was ich zeigen möchte. In Zeile 23 erreiche ich schließlich einen Widerspruch (⊥). Um dorthin zu gelangen, verwende ich die Konvertierungsregel der Quantoren (CQ), die De-Morgan-Regel (DeM) und den disjunktiven Syllogismus (DS) zusammen mit Einführungs- und Eliminationsregeln.

Weitere Informationen zu diesen Regeln im Zusammenhang mit dem Proof Checker, den ich verwendet habe, finden Sie unter forall x: Calgary Remix .

Bezug

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/

Sie können Einführungs- und Eliminierungsregeln verwenden, um die „Quantifizierer-Irrelevanz“ in nicht leeren Universen zu beweisen.

|_ Ɐx Ǝy (Fx & Gy)
|  |_ [a]
|  |  Ǝy (Fa & Gy)
|  |  |_ [b] Fa & Gb
|  |  |  Fa
|  |  Fa
|  Ɐx Fx
|  |_ [a]
|  |  Ǝy (Fa & Gy)
|  |  |_ [b] Fa & Gb
|  |  |  Gb
|  |  |  |_ [c]
|  |  |  |  Fc
|  |  |  |  Fc & Gb
|  |  |  Ɐx (Fx & Gb)
|  |  Ǝy Ɐx (Fx & Gy)
|  Ǝy Ɐx (Fx & Gy)

Und analog für die Umkehrung.