Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Ja, herzlich willkommen zur letzten Sitzung des Semesters.

Wir haben relativ entspanntes Material vor uns.

Und zwar den Vollständigkeitssatz jetzt natürlich für Logik erster Stufe.

Gesehen haben wir schon Vollständigkeitssatz für Aussagenlogik.

Er bezieht sich auf das System natürlichen Schließens, was wir eingeführt haben.

Insbesondere ist er ein Vollständigkeitssatz für die ganze Logik.

Also nicht nur für die Logik mit nur Alkvantoren in der pränexen Normalform.

Also für nur das Golem-Formeln.

Also gewissermaßen das universelle Fragment der Logik, wie wir es letztes Mal,

vorletztes Mal für den Resolutionskalkül gesehen haben, sondern eben hier für die gesamte Logik mit Existenzquantor.

In der Tat werden wir nachher den Existenzquantor vorrangig behandeln

und also im Gegenteil den Alquantor durch den Existenzquantor kodieren irgendwann kurz zwischendurch.

Zur Erinnerung, was hieß gleich noch Vollständigkeit.

Wir haben ja immer unser Problem mit den verschieden vielen Querstrichen an diesen Turnstiles.

Was ich erinnere daran, es gab den doppelten Turnstyle und den einfachen Turnstyle.

Der doppelte Turnstyle kommt aus der Semantik.

Der doppelte Turnstyle sagt, Psi, also die rechte Formel, ist logische Folgerung aus den Annahmen in Groß Phi.

Dieses Groß Phi hier ist eine Menge von Formeln.

Das heißt, jedes Modell, das die linke Seite erfüllt, erfüllt auch die rechte.

Dagegen, das hier rechts ist Syntax bzw.

bisschen wissenschaftlicher ausgedrückt, das ist Beweistheorie.

Das heißt, hier rechts der einfache Turnstyle sagt, Psi ist aus diesen Annahmen hier herleitbar.

Das heißt, in unserem System natürlichen Schließens gibt es einen Beweis,

der irgendwelche Annahmen sich aus Phi rausgreift und auf Psi endet.

Also hier nochmal die Bezeichnung dafür.

Hier links reden wir also über logische Folgerung.

Folgerung war bei uns eben ein semantischer Begriff und hier rechts über Herleitbarkeit.

Wir hatten schon gesehen, den Correctheitssatz, der besagt, die Implikation gilt von rechts nach links.

Alles, was herleitbar ist, ist auch tatsächlich eine logische Folgerung.

Das ist so eine Mindestanforderung an ein Beweissystem,

ein Beweissystem, das mir irgendwelchen Blödsinn herleitet, der nicht in Wirklichkeit eine logische Folgerung ist.

Das würde ich in genau dem Moment, wo ich das sehe, wieder wegwerfen.

Dagegen, wie gesagt, bei der Umkehrung, da müssen wir schon mal damit rechnen, dass das auch mal nicht stimmt.

Siehe eben zum Beispiel der berühmte Gödelche Unvollständigkeitssatz, der etwas vereinfacht sagt,

also zum Beispiel in logik höherer Stufe gilt das nicht.

Aber hier in logik erster Stufe gilt es eben doch.

Auch dieser Satz von Gödel, das ist eben der gödelche Vollständigkeitssatz.

Gödel ist in erster Linie berühmt für einen Vollständigkeitssatz und zwei Unvollständigkeitssätze.

Wie wir uns schon im Fall der Aussagenloge klargemacht haben,

der Weg von links nach rechts ist eben auch viel schwieriger und kompliziert als der von rechts nach links.

Von rechts nach links dieser Korrektheitssatz, da muss ich mir bei so einem einfachen System wie diesem hier im Wesentlichen

nur Regel für Regel überlegen, dass die Regeln vernünftig sind, dass die also tatsächlich zum Beispiel

gültige Formeln in gültige Formeln überführen oder im komplizierten Fall, wo sie eben Unterbeweise als Prämissen haben,

dass sie aus gültigen Formeln und korrekten Unterbeweisen wieder korrekt eine Formel folgern.

Ich habe also dieses einfache Induktionsprinzip über die Herleitung letztlich,

wogegen hier links ich erstmal überhaupt nichts in der Hand habe.

Ich habe nur diese Implikation in der Hand, die logische Folgerbarkeit, also jedes Modell, das die linke Seite erfüllt,

erfüllt auch die rechte Seite.

Daraus jetzt einen Beweis zu konstruieren, dass das erst einmal kein Selbstläufer ist.