Sprachlogische Beweisfrage: ¬∃x∀y[E(x,y) ↔ ¬E(y,y)]

Hier ist ein Beweis mit einem natürlichen Abzugsprüfer im Fitch-Stil.

Um wohlgeformte Sätze zu bilden, musste ich einige der im Beispiel des OP verwendeten Namen umschreiben. Anstelle von "E" habe ich "P" verwendet, da "E" in diesem Proof-Checker ein Symbol für den Existenzquantor ist. Auch die Notation in diesem Proof-Checker ist kompakter. Beispielsweise wurde „E(x,y)“ zu „Pxy“.

Anstatt mit einer Negation des Schlusses zu beginnen, habe ich das Negationszeichen aus dem Schluss entfernt, um die Negation am Ende einzufügen, was ich in Zeile 12 getan habe.

Von Zeile 2 bis Zeile 10 habe ich einen Unterbeweis verwendet, um den Versuch zu starten, den Existenzquantor (∃E in Zeile 11) zu eliminieren, indem ich den Namen "a" für die Variable "x" nahm. Ich habe den gleichen Namen verwendet, um den universellen Quantor (∀E) in Zeile 3 zu eliminieren. Dies erlaubte mir, das Gesetz der ausgeschlossenen Mitte (LEM) zu verwenden, um einen Widerspruch in Zeile 10 zu erreichen, der die in den Zeilen 4 und 7 getroffenen Annahmen durch Schließen entlädt die Unterbeweise.

Zeile 10 erlaubte mir, den existenziellen Quantor in Zeile 11 zu eliminieren, wodurch die Annahme in Zeile 2 entkräftet wurde. Der Widerspruch in Zeile 10 erlaubte mir, eine Negation in Zeile 12 einzuführen und den Beweis zu vervollständigen.

---

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

Ich habe LPL selbst nicht verwendet/unterrichtet, daher kenne ich das Format oder die Standards für die Fertigstellung eines RAA-Proofs nicht. Die eingerückten Zeilen 1-4 sind richtig; Für die nicht eingerückte Zeile 2 ist sie entweder fehlerhaft (Eaa, wenn und nur wenn E?) Oder ich verstehe nicht, wie ich sie analysieren soll.

In meinen Logikkursen würde ich wahrscheinlich 4 als ausreichend akzeptieren, um zu zeigen, dass 1 zu einem Widerspruch führt, QED.

Um ~P zu beweisen, beginne mit der Annahme von P mit dem Ziel, einen Widerspruch zu demonstrieren. Verwenden Sie daher "Negationseinführung". (Anmerkung: Gehen Sie nicht von einer doppelten Verneinung aus, wenn Sie sie vermeiden können – insbesondere, wenn Ihr erster Schritt darin besteht, sie zu eliminieren.)

Um einen Widerspruch von ƎxⱯy Qxy zu erhalten, verwenden Sie die Instantiierungsregeln für Quantoren und zeigen Sie, dass Qba ein Widerspruch für Zeuge b und beliebiges a (das möglicherweise auch b sein kann) ist.

Um einen Widerspruch von Eba <-> ~Eaa zu erhalten, für Zeuge b und willkürliches a, beachten Sie, dass Sie einen Widerspruch haben, wenn a gleich b ist. Ihre universelle Eliminierung wird also zum Zeugen des Existenziellen.

Zusammenfassend: Wir sollten ƎxⱯy (Exy <-> ~Eyy) annehmen, dann einen Zeugen [b] für das Existentielle annehmen, also Ɐy (Eby <-> ~Eyy), damit wir das Universelle zum Zeugen eliminieren können, so Ebbe <-> ~Ebbe, und demonstrieren, dass dies ein Widerspruch ist, wodurch wir die Annahmen aufheben und mit der Negationseinführung abschließen können.

Um zu zeigen, dass Ebb <-> ~Ebb ein Widerspruch ist, geht es einfach darum, Negationseliminationen und bikonditionale Eliminierungen zu verwenden. Angenommen, Ebb leitet einen Widerspruch aus der Bibedingung ab und führt so eine Negation ein. ~Ebb leitet ebenfalls den benötigten Widerspruch aus dem Biconditional ab.

 |_
 |  |_ Ǝx Ɐy (Exy <-> ~Eyy)
 |  |  |_ [b] Ɐy (Eby <-> ~Eyy)
 |  |  |  Ebb <-> ~Ebb
 |  |  |  |_ Ebb
 |  |  |  |  ~Ebb
 |  |  |  |  ┴
 |  |  |  ~Ebb
 |  |  |  Ebb
 |  |  |  ┴
 |  |  ┴
 |  ~Ǝx Ɐy (Exy <-> ~Eyy)

Die Aussage ¬∃x∀y[E(x,y)⟷¬E(y,y)] ist äquivalent, mit den Eigenschaften der Negation zu

∀x∃y{[E(x,y)∧¬¬E(y,y)]∨[¬E(y,y)∧¬E(x,y)]} .

Der Satz in geschweiften Klammern gilt immer für y=x mit ¬¬E→E, und dies beweist die Aussage. Dieser Beweis hat den Vorteil, dass er die Verwendung der reductio ad absurdum und damit des Gesetzes des ausgeschlossenen Dritten vermeidet; es nutzt jedoch die Tatsache, dass ¬¬E→E. Daher wäre dieser Beweis in der intuitionistischen Logik nicht akzeptabel . Die Aussage von OP ist ein Theorem in der klassischen Logik, aber nicht in der schwächeren intuitionistischen Logik.