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

So ich sage noch einmal abschließend das was ich am ende der letzten Sitzung gesagt habe,

das sage ich jetzt nur für die Kamera, damit die Leute, die sich das online angucken,

noch alle Informationen haben. Also der Haker im Korrektheitsbeweis des Unif... quatsch,

des doch des Unifikationsalgorithmus, der war keiner. Also ich hatte nach der

der Extemporale noch erklärt, warum die Argumente, die an der Tafel standen, korrekt waren.

So, for the record gewissermaßen.

Wir fahren fort mit der Definition der Semantik und Syntax von Logik erster Stufe.

Das hatten wir letztes Mal schon im Wesentlichen fertig, was die grundlegenden Definitionen anging.

Ich erinnere nochmal an die Kerndinge.

Formeln sind also folgender Form. Phi ist entweder eine Gleichung oder eine Prädikatenanwendung auf eine Reihe von Termen.

Oder ein paar Dinge, die wir aus der Aussagenlogik schon kennen.

Oder eine allquantifizierte Formel für alle x.phi.

Das war die Syntax. Die Semantik hatten wir dann erklärt über Strukturen für eine gegebene Signatur.

Eine Signatur ist ein Vorrat von Symbolen, Prädikaten und Funktionssymbolen.

Eine Struktur bestand aus einer Trägermenge, dem sogenannten Grundbereich.

Und Interpretationen der Symbole in der Signatur, also Interpretationen der Funktionssymbole als Funktionen auf dem Grundbereich der richtigen Stelligkeit.

Und Interpretationen der Prädikatensymbole als Prädikate auf dem Grundbereich der jeweils richtigen Stelligkeit.

Und wir hatten dann erklärt, die Erfülltheit von Formeln über einem Modell zusätzlich ausgerüstet mit einer sogenannten Umgebung,

etat, die uns die Werte der Variablen als Elemente des Grundbereichs festlegt.

Und Erfülltheit schreibt sich hier mit dem doppelten Turnstyle. Die Definition dieser Erfülltheitsrelation war letztlich rekursiv.

Mit offensichtlichen Klauseln für die Buhlchenformeln und immer noch relativ offensichtlichen Klauseln hier für diese Atomanformeln E gleich D oder P von E1 bis EN.

Wobei letztere dann abhängen auf einer ebenfalls rekursiv definierten Denotation eines Terms E im Modell M und unter Umgebung etat als ein Element des Grundbereichs M.

Und die entscheidende semantische Klausel für den Alquantor war dann diese hier M und etat erfüllen für alle x Punkt Phi.

Genau dann wenn jetzt kommt ein Meta Alquantor und das Spiel sind wir jetzt mittlerweile gewöhnt für alle Elemente des Grundbereichs, also für alle M, Klein M aus Groß M, gilt M und etat mit einer Abänderung,

nämlich der Abänderung das jetzt x auf M zeigt erfüllt Phi. Ja, so weit waren wir letztes Mal gekommen und das schließt auch im Prinzip die Definition der Semantik ab.

Das gehört jetzt eine Bemerkung hinterher, denn wir hatten ja den Existenzquantor definiert durch den Alquantor. Ich erinnere, Recall existiert x Punkt Phi war einfach definiert als nicht für alle x nicht Phi.

In klassischer Logik geht das, in intuitionistischer natürlich nicht mehr. Und wenn wir das so deklarieren, dann können wir jetzt die semantischen Klauseln für einmal nicht einmal Alquantor und einmal nicht zusammensetzen.

Wenn wir das durch xen, stellen wir fest, dass damit folgendes gilt M und etat erfüllt es existiert x Phi. Genau dann wenn Meta Alquantor es existiert ein Klein M aus dem Grundbereich Groß M,

so das gilt ja dasselbe wie hier M und etat mit x abgeändert auf M erfüllen Phi. Gut.

Ja, damit ist also die Definition der Semantik tatsächlich abgeschlossen. Wir kümmern uns jetzt ein bisschen um ein paar syntaktische Sachen, zum Beispiel um den Begriff der freien Variablen.

Ja, es ist immer wichtig zu wissen, welche Variablen einer Formel überhaupt vorkommen. Unter anderem, das werden wir gleich in einem folgenden Lämmer festhalten, um zu wissen,

welche Variablen für die Semantik einer Formel relevant sind. Und es ist aber zunächst mal nicht so offensichtlich, welche Variablen in einer Formel denn nun vorkommen, in Anführungsstrichen,

weil ja einige Variablen gewissermaßen im Laufe der Auswertung der Formel wieder überschrieben werden. Deswegen unterscheidet man also in sogenannte freie und gebundene Variablen,

wobei man nur die freien Variablen definiert, die gebunden sind dann eben die anderen. Also freie Variablen einer Formel Phi definiert man wie folgt.

Erst mal intuitiv, sag ich doch mal das Gegenteil. Das Gegenteil ist sowas hier. Also wenn ich schrage, für alle x gilt irgendwas, dann ist das für alle,

diese Variable x, die ist gebunden durch das für alle. Das heißt, die ist hier in dem Bereich bis zum Ende des Phi eben nicht mehr frei.

Also man sagt, dieses Ding hier bindet x. Ja, und nach dieser Intuition funktioniert auch die formale Definition. Also die freien Variablen von einem Ausdruck,

das sind tatsächlich die in ihm vorkommenden Variablen, die wir schon mal informell als vars von e definiert hatten. Also einfach syntaktisch die Variablen, die in dem Term halt drin stehen.

Das ist deswegen hier so einfach, weil es also unter den Termen keine gibt, die Variablen binden. Also jedes Vorkommnis einer Variablen in einem Term ist tatsächlich frei.

Ja, dann geht es erstmal relativ einfach weiter. Die freien Variablen einer Gleichung sind die auf beiden Seiten vorkommenden Variablen, also vars e plus vars b.

Die freien Variablen in so einer Prädikatenanwendung e1 bis en. Das ist die Vereinigung, die große Vereinigung von i gleich 1 bis n der freien Variablen der vorkommenden Terme ei.

Dann die freien Variablen einer Negation sind die freien Variablen der ursprünglichen Formel, genauso einfach für den Fall der Konjunktion.

Die freien Variablen von Phi und Pi sind die freien Variablen von Phi, vereinigt mit den freien Variablen von Pi.

So, und jetzt kommt endlich mal eine Klausel, wo tatsächlich was passiert. Die freien Variablen einer allquantifizierten Formel für alle x Punkt Phi,

das sind eben die in Phi freien Variablen, also fv von Phi, aber eben nicht die quantifizierte Variable x, das heißt die wird wieder weggenommen.

Ja, also zum Beispiel sind die freien Variablen in, so was nehmen wir jetzt, x gleich y und für alle z, z gleich z oder sowas,

das sind x Komma y, die eine Variable z, die nun da in dem allquanto vorkommt, oder nehmen wir hier nochmal w, z gleich w, das sind dann also x, y und w,

das w hier ist frei, das z ist gebunden, das ist natürlich eine blödsinnige Formel, aber es geht ja nur um Syntax.

Und man passe aber auf, wenn ich jetzt hier anfange Variablen umzubenennen, also sowas wie x gleich y und für alle y, y gleich w,