Herzlich willkommen!

Ja, heute haben wir mal was, das macht Spaß. Vollständigkeit der Aussagenlogik.

So, ja, was soll das heißen?

Ich erinnere nochmal an eine Äußerung aus der letzten Sitzung.

Und zwar zu Korrektheit.

Das ist eine Aussage gewesen über unser formales Beweissystem, das System des natürlichen Schließens, das wir letztes Mal eingeführt haben.

Und zwar sagt sie aus, wenn ich in diesem System eine Aussage psi aus Annahmen in Großphi herleiten kann, dann ist psi auch eine Konsequenz von Großphi.

Und der Beweis, das waren so anderthalb Absätze ganz am Ende der Vorlesung, die im Wesentlichen besagten, naja, jede Regel ist halt korrekt.

Mit anderen Worten, das ist also eine Induktion über die Struktur dieser Beweise. Das Einzige, was daran so ein bisschen schwieriger war, ist, dass eben diese Beweise so als Datenobjekte so ein bisschen komplizierte Tiere sind.

Wenn Sie versuchen, das in Heskel oder C so als Datentyp zu realisieren, werden Sie das merken, dadurch, dass die eben diese hierarchische Struktur haben und in Beweisen wiederum Unterbeweise sind, also dass das gewissermaßen Bäume sind, in denen sich wiederum Unterbäume aufhalten.

Nicht dadurch allein wird der Beweis so ein bisschen kompliziert hinzuschreiben, aber das Grundprinzip ist eben sehr einfach. Alle Aktionen sind korrekt und die Regeln sind alle korrekt. Fertig.

So, heute beweisen wir die sogenannte Vollständigkeit, gut sagen wir das einmal vollständig,

die Vollständigkeit der Aussagenlogik. Das ist jetzt sehr schnell hinzuschreiben, das ist einfach die umgekehrte Implikation.

Das heißt, wann immer eine Formel psi eine logische Folgerung aus Annahmen in Groß Phi ist, womöglich unendlich vielen Annahmen,

dann kann ich psi auch aus diesen Annahmen in Groß Phi in unserem formalen System herleiten.

Das ist jetzt als Aussage eben ein ganz anderes Kaliber, weil ich nicht etwa einen Beweis schon in Händen habe,

den ich nur durch Induktionen, also gewissermaßen durch ein Auseinandernehmen einer Datenstruktur auf Korrektheit untersuchen muss,

sondern im Gegenteil, ich habe so ein rein semantisches Faktum, das also hier großallquantifiziert ist über alle Wahrheitsbelegungen,

also wenn es der Fall ist, dass alle Wahrheitsbelegungen, die Phi wahrmachen, auch psi wahrmachen,

dann muss ich mir irgendwie einen Beweis aus den Fingern saugen, mittels dessen, psi eben aus Groß Phi herleitbar ist. Das ist ein ganz anderer Schnack.

So, der Beweis ist nicht fürchterlich kompliziert, wir werden ihn auch heute schaffen und hoffentlich nicht die ganze Sitzung dafür brauchen,

aber er verlangt also so ein bisschen Abstraktionsvermögen. Wir geben erstmal so einen Überblick über den Beweis, das heißt, wir zerlegen ihn in mehrere Schritte.

Das heißt, wir geben also gewissermaßen vorab einen Überblick über die Beweisstrategie, wenn wir es mal so hochtraben, so nennen wollen.

Nein, das geht mir noch nicht, weil wir noch Begriffe definieren müssen, die in der Beweisstrategie vorkommen.

Wir brauchen folgende Definition, und zwar definieren wir Eigenschaften von Formelmengen, also wir geben uns vor eine Formelmenge Groß Phi,

definieren jetzt zwei Eigenschaften davon. So, ich definiere zunächst einmal, was es heißt, dass eine Formelmenge inkonsistent ist.

Irgendwer hat wieder die Kreide versaut. So, eine Formelmenge ist inkonsistent, genau dann, wenn ich einen Widerspruch aus ihr herleiten kann.

Nicht zu verwechseln mit Unerfüllbarkeit, das haben wir schon gesehen, eine Formelmenge ist unerfüllbar, wenn ich keine Wahrheitsbedingungen finde, die alle Formeln in der Formelmenge wahr macht.

Hier reden wir also von formaler Inkonsistenz in unserem formalen System. Also das hier heißt, wir können in unserem formalen System, in unserem System natürlichen Schließens einen Beweis hinschreiben, mit dem wir also Phaesum herleiten aus unseren Annahmen.

Und sonst natürlich ist Phi konsistent. Wohlgemerkt ist also damit dieser positiv ausklingende Ausdruck Konsistenz eigentlich eine negative Eigenschaft.

Also Konsistenz heißt, ich kann eine bestimmte Formel nicht herleiten. Interessanterweise ist das übrigens äquivalent dazu, dass es überhaupt eine Formel gibt, die ich aus Phi nicht herleiten kann.

Also eine Phi ist dann konsistent, wenn es eine Formel gibt, die ich nicht aus Phi herleiten kann.

Denn sobald ich Phaesum herleiten kann, kann ich auch alle anderen herleiten mittels Phaesum-Elimination, ex Phaesum-Quadrivet. So, das ist die eine Eigenschaft.

Und für die zweite, ja, erinnere ich jetzt nochmal an das, was in diesem Primer zu mathematischen Grundbegriffen steht, weil erfahrungsgemäß die meisten den dann doch nicht gelesen haben.

Und insofern an dieser Stelle man Missverständnissen vorbeugen muss. Also, und zwar erinnere ich an Begriffe aus der Ordnungstheorie.

Wir nennen uns also vor eine geordnete Menge x, kleiner gleich. Das heißt, kleiner gleich ist eine Relation auf x binär, die ist transitiv, reflexiv und antisymmetrisch.

An die drei Begriffe erinnere ich jetzt nicht nochmal. So, das ist eine Ordnung. Insbesondere sieht das typische Bild einer Ordnung in etwa so aus.

So eine Ordnung kann nach oben verzweigen, mal wieder vielleicht zusammenlaufen, mal auch nicht. Keineswegs ist das hier die richtige Vorstellung von einer geordneten Menge, also einfach so eine lineare Anordnung von Dingen.

Das ist man gewohnt so zu denken, weil man dieses Symbol so kennt von den natürlichen und reellen Zahlen und die sind natürlich so angeordnet, wie dieses Bild hier rechts sogar riert.

Aber wenn nicht ausdrücklich gesagt wird, dass eine Menge linear oder total geordnet ist, so heißt das dann, dann stellt man sie sich besser so vor als so.

So, und dann gibt es zwei Begriffe, die es auseinander zu halten gilt. Das eine ist der Begriff eines größten Elements einer geordneten Menge.

Und das besagt, x, also x ist dann ein größtes Element, genau dann, wenn für alle anderen Elemente y aus x, also alle Elemente, nicht nur die anderen, sondern auch x selbst, gilt, dass y kleiner als x ist.

Diese Menge beispielsweise hat kein größtes Element. Ja gut, ich muss natürlich irgendwie oben suchen, also hier und hier finde ich gute Kandidaten, aber die sind keine größten Elemente, da sie untereinander unvergleichbar sind.

Also dieses hier ist nicht größer gleich dem da und umgekehrt auch nicht. Also ist keins von beiden ein größtes Element.

So, und dann gibt es einen sehr ähnlich klingenden Begriff, der meinetwegen auch ein bisschen unglücklich gewählt ist, aber das ist nicht meine Schuld.

Wir sagen ein Element x sei maximal, wenn etwas subtil anderes gilt.

So, es klingt jetzt erstmal gleich. Wir sagen x ist ein größtes Element, wenn es größer als alle anderen ist. Und wir sagen x ist maximal, wenn kein anderes Element größer ist als x.

So, ich fahre mir das einmal aus. So, ich kann natürlich nicht sagen, es gäbe kein y, das größer gleich x ist, denn x selber ist ja zum Beispiel größer gleich x.

Aber ich will sagen, es gibt auch kein anderes. Das heißt, wenn y größer gleich x ist, dann ist y schon gleich x.

Naja, und wenn man dann ein bisschen sparsam sein will, das merkt man, wenn man so etwas versucht in einem Theorenbeweiser zu implementieren oder so was, dann merkt man, dass man hier natürlich statt gleich kleiner gleich schreiben kann, denn größer gleich wissen wir ja schon.