Vollständigkeit / Korrektheit der Logik zweiter Ordnung

Skizze des Beweises

1) Wir definieren die Syntax für SOL und den entsprechenden deduktiven Apparat, indem wir Axiome und Regeln für die Verwaltung der Quantifizierung zweiter Ordnung hinzufügen (siehe z. B. van Dalen, Logik und Struktur (2013), Kap . 5 ).

2) Wir definieren die "Standard"-Semantik für die Sprache.

3) Wir definieren den Begriff der normgültigen Erweiterung des FOL-Konzepts auf natürliche Weise.

Dann beweisen wir:

Korrektheitssatz : Jeder Satz des Prädikatenkalküls zweiter Ordnung ist standardmäßig gültig.

4) Wir betrachten die FOL-Version der Peano-Axiome plus das Induktionsaxiom ; Es ist wichtig zu beachten, dass Induktion in der SOL-Version eine Formel und kein Axiomschema ist .

5) Sei AR2 die Konjunktion der Axiome erster Ordnung der formalen Arithmetik plus des Axioms zweiter Ordnung der mathematischen Induktion.

Das beweisen wir:

Alle zwei Standardinterpretationen M und M' , die Modelle von AR2 sind, sind isomorph .

6) Sei L2A die Sprache zweiter Ordnung für Arithmetik (mit den nichtlogischen Konstanten der formalen Arithmetik: Null, Nachfolger, Addition, Multiplikation).

Sei N die Standardinterpretation von L2A mit der Menge der natürlichen Zahlen als Definitionsbereich und den üblichen Interpretationen der nichtlogischen Konstanten.

Wir beweisen (mit 5) dass:

Sei B eine beliebige Formel der arithmetischen Sprache. Dann ist B in N genau dann wahr , wenn AR2 ⇒ B standardgültig ist .

7) Wir beweisen:

Die Menge SV normgültiger Formeln von L2A ist nicht effektiv aufzählbar.

Nehmen Sie an, dass SV effektiv aufzählbar ist. Dann könnten wir mit 6 die Menge TR aller wahren Formeln der Arithmetik erster Ordnung effektiv aufzählen, indem wir SV durchlaufen , alle Formeln der Form AR2 ⇒ B finden, wobei B eine Formel der Arithmetik erster Ordnung ist, und diese auflisten Formeln B. _ Dann wäre die Theorie TR entscheidbar (was nicht der Fall ist), da wir für jede geschlossene Formel C effektiv TR aufzählen könnten, bis entweder C oder seine Negation erscheint.

8) Aus 7 folgt, dass die Menge aller allgemeingültigen Formeln nicht effektiv aufzählbar ist.

Eine Aufzählung aller standardmäßig gültigen Formeln würde eine Aufzählung aller standardmäßig gültigen Formeln von L2A ergeben , da die Formelmenge von L2A entscheidbar ist.

9) Es gibt kein effektives formales System, dessen Theoreme die standardmäßig gültigen Formeln von L2A sind .

Wenn es ein solches Axiomensystem gäbe, könnten wir die allgemeingültigen Formeln von L2A aufzählen , die 7 widersprechen.

10) Unvollständigkeit der Standard-Semantik : Es gibt kein effektives formales System, dessen Theoreme alle standardmäßig gültige Formeln sind.

Wenn es ein solches Axiomensystem gäbe, könnten wir die Menge aller standardmäßig gültigen Formeln aufzählen, die 8 widersprechen.

Die letzte Tatsache unterscheidet die Logik zweiter Ordnung klar von der Logik erster Ordnung, da Gödels Vollständigkeitssatz uns sagt, dass es ein effektives formales System gibt, dessen Sätze alle logisch gültige Formeln erster Ordnung sind.

Es ist ein komplizierter Beweis.

Angenommen, wir haben Prädikatenkalkül erster Ordnung und Grundrechenarten. Wir können logische Aussagen numerisch codieren. (Dieser gesamte Eintrag wird zum Beispiel durch eine Reihe von Bits dargestellt, wenn ihn jemand liest.) Angenommen, wir haben ein starres logisches System mit Axiomen und Ableitungsregeln, können wir einige Aussagen beweisen, und wir können einige beweisen kann nicht bewiesen werden. Zum Beispiel kann bei gegebenen vernünftigen Axiomen und Ableitungsregeln „3 ist eine Primzahl“ bewiesen werden, aber „3 ist zusammengesetzt“ kann nicht bewiesen werden. Wir haben drei Klassen von Aussagen: solche, die wir als wahr beweisen können, solche, die wir als falsch beweisen können, und solche, die wir noch nicht beweisen können.

Wenn Sie sich nun eine Montage von Tafeln und Reden von jemandem vorstellen, der in formaler Logik besser ist als ich ...

Beweisbarkeit ist eine numerische Relation. Es ist möglich, numerisch auszudrücken, ob ein Satz bewiesen werden kann. Beweisbarkeit ist also eine numerische Beziehung, und wir können diese Beziehung in einem Satz ausdrücken, den wir in eine unvorstellbar große Zahl verwandeln können, die wir genauso gut N nennen können. Wir können auch eine Zahl U bilden, die das Komplement der Beweisbarkeit darstellt.

Ausgehend von U können wir eine Zahl P konstruieren. (Stellen Sie sich vor, wir hätten sie während einer Toilettenpause, da ich mich nicht an die Details erinnere.) Wenn wir P entschlüsseln, lesen wir, dass die Aussage P nicht beweisbar ist.

Nun gibt es zwei Möglichkeiten. P könnte wahr sein, in diesem Fall haben wir eine wahre Aussage, die nicht bewiesen werden kann, also ist das logische System unvollständig. Es könnte falsch sein, in diesem Fall ist es beweisbar, und wir können eine falsche Aussage beweisen, also ist das logische System inkonsistent.

Jetzt können wir Regeln hinzufügen, um dies auszubessern, sodass P entweder beweisbar wahr oder beweisbar falsch ist. An diesem Punkt haben wir geändert, was Beweisbarkeit ist, also kommen wir auf eine viel größere, unvorstellbar große Zahl N1, und so erhalten wir U1 und kommen auf eine neue P1, die besagt: „Proposition P1 ist selbst mit unseren neuen Regeln nicht beweisbar.“ , und wir sind wieder da, wo wir angefangen haben.