Ja, herzlich willkommen. Ich arbeite mal mit Mikro, damit es vielleicht zumindest Audio gibt.

Das hat ja letztes Mal auch ohne Kamera geklappt. Also ich sehe gerade vom Rechenzentrum niemanden.

Also das es vorletztes Mal keine Aufnahme gab, lag an plötzlicher Krankheit. Das es letztes

Mal keine Aufnahme gab, lag daran, dass Herr Hausmann das nicht so gerne hat. Heute hätte

es eigentlich eine geben können. Gut, können wir nichts machen. Es sei denn jemand möchte...

Es ist sogar an. Ich habe doch eben gerade gefragt, ob jemand da ist. Ach so, dann brauche ich hier

gar nicht mühsam irgendwie. Man sieht sie so schlecht. Alles bestens. Ja, dann ist ja gut.

Okay. Bestens. Ja, sind Sie mit Herrn Hausmann denn ansonsten klar gekommen?

Gibt es noch Rückfragen dazu? Wir haben heute eine relativ entspannte Sitzung. Also ich kann

mich gerne mit Fragen beschäftigen. Alles gut. Okay. Es gab einen Punkt in der Notation,

den wir eigentlich dieses Jahr ändern wollten und weil das im Skript noch nicht geändert war,

hat das Herr Hausmann noch nicht so dargestellt. Also Substitution. Herr Hausmann hatte Ihnen,

glaube ich, Substitution noch in dieser Notation hier dargestellt, wo also die Variablen links stehen,

die Terme rechts und dazwischen ein Backslash maps to. Und dafür wollen wir vor allem folgende

eigentlich weiter verbreitete Notation ab jetzt nehmen. Term links, Variable rechts und dazwischen

ein Slash. Und davon wie gehabt eventuell Listen von solchen Paaren. Das hat den Vorteil,

dass man weniger notationelle Clashes bekommt, wenn man diese Schreibweise nimmt. Sie ist etwas

weniger suggestiv, gebe ich zu. Man liest sie sich vor, so in der Reihenfolge, wie sie da steht. Also

E1 wird eingesetzt für X1 und so weiter bis EN wird eingesetzt für XN. So, wir sind,

wie Sie vielleicht gesehen haben, dadurch, dass ich vorletztes Mal unerwartet viel geschafft habe

und das, obwohl wir zwischendurch ja fünf Minuten Pause gemacht haben, mehr oder weniger, so ungefähr

eine Sitzung vorm Plan. Ja, also gerne Zwischenfragen stellen, wir haben Zeit.

Ja, Thema des heutigen Tages, natürliches Schließen in Prädikatenlogik. Herr Hausmann hat

Ihnen ja letzte Woche die Syntax der Prädikatenlogik nahegebracht. Wir hatten vorher behandelt

Aussagenlogik und wir haben von der Aussagenlogik ungefähr in dieser Reihenfolge Syntax, Semantik

und Deduktionssystem abgehandelt und das Deduktionssystem war auch ein System natürlichen

Schliessens. Wir machen das jetzt für die Prädikatenlogik andersrum, also gut, ohne Syntax

geht es natürlich nicht. Also wir haben die Syntax letztes Mal kennengelernt und wenden uns jetzt

aber zuerst dem Deduktionssystem zu, in erster Linie aus didaktischen Gründen. Das Deduktionssystem

ist im Falle der Prädikatenlogik doch, sagen wir mal, deutlich einfacher zu verstehen, vielleicht

ist zu viel gesagt, einfacher zu präsentieren zumindest als die Semantik. Die Semantik von

Prädikatenlogik, die ist dann doch ein etwas komplizierteres Konstrukt, auch wenn sie im Grunde

natürliche Sache ist, hat sie also viel notationelles Gepäck dabei, was also einiges vielleicht etwas

schwierig zu verdauen macht. Dagegen ist also das natürliche Schließen in Prädikatenlogik eine

vergleichsweise naheliegende Sache, die sich auch nur durch hinzufügen von ein paar Dingen

von ihrem Aussagen logischen Gegenpart unterscheidet. Also mit anderen Worten, das System natürlichen

Schließens für Prädikatenlogik ist schlicht und einfach eine Erweiterung des Systems für die

Aussagenlogik. Also alles, was wir an aussagenlogischen Zutaten dabei haben, Negation,

Konjunktion und dann die abgeleiteten konnektive Implikation und Disjunktion, das wird genauso

behandelt wie halt in der Aussagenlogik auch schon, da ändert sich nichts. Das Einzige,

was wir also machen müssen, ist für unsere neuen syntaktischen Einheiten passende Regeln

hinzuzufügen und zwar eben gerade, wie wir das gewohnt sind, Einführungs- und Eliminationsregeln.

Wir fangen mal an mit den Regeln für Gleichheit. Das ist ja eins von den Dingen, die jetzt

dazugekommen sind. Ich wollte keine Panik erzeugen, ich hatte nur niemanden gesehen, deswegen dachte

ich, es wäre niemand da, aber es offenbar nur eine hohe Ballustrate. So, da gibt es also einmal

eine Einführungsregel für Gleichheit. Wir wollen also jetzt eine Regel einführen,

wo wir anschließend in der Konklusion eine Aussage über Gleichheit kriegen. Die Regel

ist erstaunlich einfach, sie hat keine Prämisse, sie ist also in Wirklichkeit ein Axiom.

Und sie beinhaltet schlicht und einfach Reflexivität der Gleichheit. Sie sagt uns also,

ein Term ist gleich sich selber. Gut. Und da gibt es eine Eliminationsregel für Gleichheit,