Ja, herzlich willkommen.

Ja, wir hatten letztes Mal begonnen mit dem Thema natürliche Deduktion.

Wir hatten für die einzelnen Konnektivenaussagen Logik, Einführungsregeln und Eliminationsregeln

kennengelernt.

Dazu hatten wir zunächst uns die beiden Grundkonnektive Negation und Konjunktion vorgenommen mit entsprechenden

Regeln.

Und wir haben dann für die abgeleiteten Konnektive, insbesondere eben für Disjunktion und Implikation,

eigene Einführungs- und Eliminationsregeln angegeben, da wir aus den, da wir die Disjunktion

und Implikation durch Konjunktion und Negation kodiert sind, aus den Regeln für Konjunktion

und Negation herleiten konnten.

Genauer gesagt, wir haben sie hergeleitet für Implikation und die Regeln für Disjunktion,

die stehen auf dem heute veröffentlichten aktuellen Übungsblatt.

Ja, gut, diese Regeln, die habe ich eben so ein bisschen vom Himmel fallen lassen und

die sollen eben in vernünftiger Beziehung stehen zu der Semantik, die wir schon kennengelernt

haben.

Nicht insbesondere gab es eben diese beiden sehr ähnlichen Schreibweisen.

Aber einmal hier mit dem einfachen Querstrich.

Hier dieses mit dem einfachen Querstrich bedeutet also Herleitbarkeit.

Dies hier liest sich, psi ist, das mittlere klammer ich mal ein, das ist nur der Verklarung,

das mittlere, also diesmal mit dem einfachen Querstrich liest sich, psi ist aus phi herleitbar,

das heißt, ich kann einen Beweis konstruieren, an dessen Ende psi steht und der eingangs

irgendwelche Annahmen stehen hat, die ich mir aus Groß phi raus greife.

Groß phi ist eine Menge von Formeln, im Zweifelsfalle unendlich.

Natürlich kommen in so einem Beweis dann nur endlich viele von diesen Annahmen vor.

Ich schreibe irgendwie aus meiner unendlichen Menge von Annahmen 25 einmal eingangs in

meinem Beweis hin und leite dann irgendwelches Zeugs her und am Ende steht psi.

Das bedeutet diese Notation hier.

Während das mit dem Doppelstrich etwas ganz anderes ist, was wir früher eingeführt haben,

nämlich, psi ist logische Folgerung aus Groß phi, das heißt,

das heißt, für jede Wahrheitsbelegung kappa gilt, wenn sie Groß phi erfüllt, das heißt,

alle Formeln in Groß phi erfüllt, dann erfüllt sie auch die Formel klein psi.

Das ist also von der Definition her etwas völlig anderes als das mit dem einfachen

Querstrich, da kommen doch nicht mal dieselben Begriffe drin vor.

So, und zwischen diesen Begriffen hätte man aber natürlich gerne Beziehungen.

Also das hier, das ist so unser Gold Standard gewissermaßen.

Das hier ist unsere Definition von logischer Folgerung, das hier ist nur irgendwelche Spielerei

mit Symbolen auf Papier.

Sage ich jetzt mal so, Sie werden Leute treffen, die sagen das genau umgekehrt.

Aber wir gehen jetzt mal davon aus, dass also unser Begriff von Wahrheitsbelegung, und

da füllt halt eine Formel durch eine Wahrheitsbelegung, dass das etwas Natürliches und Gegebenes

sei und wir fragen uns also, ob jetzt hier unser Beweissystem, was uns die Herdartbarkeit

definiert, ob das in vernünftiger Weise entworfen ist, also ob es uns genau diese Relation hier

unten einfängt.

Das zerfällt in zwei Implikationen.

Einmal wollen wir gerne, dass wenn wir etwas in unserem Beweissystem herleiten, es dann

auch tatsächlich eine logische Folgerung ist.

Das ist so eine Minimalanforderung an unser System.

Wenn es das nicht erfüllt, schmeißen wir es anschließend wieder weg.

Das nennt sich Korrektheit.

Und ein System, das eben nicht korrekt ist, also ein Beweissystem, das nicht korrekt