Sprachbeweis und Logik Kapitel 13 Frage 49 Hilfe

Das Ende sollte nicht matschig sein. Das Ende ist dort, wo Sie beginnen, dann arbeiten Sie sich hinein.

Schauen Sie sich an, wo Sie anfangen und wohin Sie wollen.

|  Ex P(x)                         Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)    Premise
|   :
|   :
|  Ex (P(x) ^ Ay (P(y) -> y=x)     ...

Natürlich müssen Sie dieses Existenzielle einführen, und der beste Kandidat ist, die existenzielle Prämisse zu eliminieren.

|  Ex P(x)                         Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)    Premise
|  |_ [a] P(a)                     Assumption
|  |   :
|  |   :
|  |  P(a) ^ Ay (P(y) -> y=a)      ...
|  |  Ex (P(x) ^ Ay (P(y) -> y=x)) Existential Introduction
|  Ex (P(x) ^ Ay (P(y) -> y=x))    Existential Elimination

Jetzt müssen Sie ein Universal (zweimal) eliminieren und eins einführen; und auch eine Konjunktion.

|  Ex P(x)                            Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)       Premise
|  |_ [a] P(a)                        Assumption
|  |  |_ [b]                          Assumption
|  |  |  |_ P(b)                      Assumption
|  |  |  |  Ay ((P(a) ^ P(y)) -> a=y) Universal Elimination
|  |  |  |  (P(a) ^ P(b)) -> a=b      Universal Elimination
|  |  |  |   :
|  |  |  |   :
|  |  |  |  b=a                       ...
|  |  |  P(b) -> b=a                  Conditional Introduction
|  |  Ay (P(y) -> y=a)                Universal Introduction
|  |  P(a) ^ Ay (P(y) -> y=a)         Conjunction Introduction
|  |  Ex (P(x) ^ Ay (P(y) -> y=x))    Existential Introduction
|  Ex (P(x) ^ Ay (P(y) -> y=x))       Existential Elimination

Ich bin sicher, Sie können abschließen. Ich füge einen Hinweis hinzu: Gleichstellungseinführung sagt b=b.

Der folgende Beweis ähnelt dem von Graham Kemp vorgeschlagenen. Was anders ist, ist, dass ich die ersten acht Zeilen des Beweises des OP verwende, die Verwendung eines anderen Beweisprüfers zeigen und eine Möglichkeit bieten, die Identitätsregeln zu verstehen.

In diesem Beweis beachten Sie, dass a = b in Zeile 8 zu b = a in Zeile 10 wird. Um dieses Ergebnis zu erreichen, muss ich in Zeile 9 eine Identität einführen, a = a . Ich muss keine Zeile referenzieren, um diese Identität einzuführen. Wenn ich diese Zeile habe, habe ich eine Zeile, in der ich eine Ersetzung vornehmen kann, wenn ich die Identitätsbeseitigung verwende.

Die Identitätsbeseitigung ist so einfach, dass man leicht übersehen kann, was vor sich geht. So beschreibt es Frederic Fitch (14.3, Seite 81):

Nehmen wir an, dass ( ...a...) irgendein Satz ist, der a erwähnt , und dass (...b...) das Ergebnis der Ersetzung von a durch b an einer oder mehreren Stellen in (...a... ) ist. ) . Nach dieser Regel [der Identitätseliminierung] können wir dann aus (...a...) und [a = b] auf (...b...) schließen .

Im obigen Beweis steht die Identität, die für diese Regel benötigt wird, in Zeile 8, a = b , und die Aussage, die a erwähnt, in der wir a durch b ersetzen , ist Zeile 9, a = a , genau die, die wir eingeführt haben eine Identität. Zeile 9 wird jetzt nicht als Identität angesehen, sondern als Proposition, die ein enthält . Wir ersetzen nur das erste a in Zeile 9 und lassen das andere übrig. Daraus können wir Zeile 10 ableiten: b = a .

---

Referenz

Fitch, FB, Symbolische Logik: Eine Einführung, 1952.

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