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

Ja, herzlich willkommen.

Ja, wir befassen uns also weiter mit dem letztes Mal angeschnittenen Thema mit Erbrauchemodellen.

Wenn irgendjemand mal eben Wikipedia offen hört, ich glaube, der Herr ist Franzose.

Ja, ich erinnere an die zuletzt dargewesenen Definitionen.

Die zwei zentralen Begriffe hier sind also das Erbrauuniversum und die Erbraumbasis.

Das Erbrauniversum, später der Träger der Modelle, um die es gehen wird, ist eine Menge von Termen,

und zwar die Menge derjenigen Termen, die ich ohne Zuhilfenahme von Variablen bauen kann,

mit anderen Worten, die ich alleine aus Konstanten und Funktionssymbolen zusammengebaut bekomme.

Das heißt, hier ist E ein Term über Sigma. Die ganze Geschichte hängt ab von einer Signatur Sigma,

also einem Vorrat von Prädikaten und Funktionssymbolen. Hierfür relevant nur die Funktionssymbole.

Und die freien Variablen von E, die dürfen nicht existieren.

Das heißt, die Menge der freien Variablen von E soll leer sein.

Also das hier ist das Erbrauuniversum.

Und die Erbraumbasis ist also die Menge aller elementaren Fakten über die Individuen in diesem Universum.

Das sind eben alle Dinge, von denen ich sicher sein kann, dass sie existieren.

Nicht jede Konstante muss im Modell vorhanden sein und ich muss alle Funktionssymbole anwenden können.

Die Elementarfakten über diese Individuen sind Formeln, von denen ich folgendes verlange.

Erstens, die Formeln sollen atomar sein.

Natürlich leben sie wiederum über der gegebenen Signatur Sigma.

Das also diesmal bestimmt, dass wir zum einen aus den Funktionssymbolen bestimmen,

welche Terme hier vorkommen und zum anderen aus den vorkommenden Prädikatensymbolen,

welche Prädikate halt in atomaren Formeln vorkommen.

Und wiederum verlangen wir, dass die Formeln abgeschlossen sind, das heißt keine freien Variablen haben.

Und das können wir nochmal übersetzen. Was für atomare Formeln kann ich denn bilden?

Wir haben am Anfang ja die Gleichheit aus der Sprache ausgeschlossen für Zwecke der logischen Programmierung.

Ich komme ja auch im Prolog nicht vor.

Das heißt, eine atomare Formel ist in jedem Fall eine Anwendung eines Prädikatensymbols auf irgendwelche Terme,

also von der Form P von E1 bis EN.

Dabei muss die Stelligkeit stimmen, das heißt P muss ein endstelliges Symbol in Sigma sein.

Und weil ich verlange, dass die Formel abgeschlossen ist, müssen eben die hier vorkommenden Terme auch alle abgeschlossen sein.

Mit anderen Worten, sie müssen Elemente des Erbrauchuniversums sein.

Das heißt also E1 bis EN sind Elemente von U Sigma.

Gut.

Ja, ein Erbrauchmodell ist nun schlicht und einfach ein Modell, das über diesem Erbrauchuniversum lebt

und sich hinsichtlich des Verhaltens von Funktionssymbolen so verhält, wie man das nun von so einer Termmenge erwartet.

Das heißt folgendes, Definition.

Ein Erbrauch-Sigma-Modell ist ein bestimmtes Sigma-Modell, wie der Name schon sagt, ist ein Sigma-Modell mit

ja, erstens seine Sigma-Modell M hatte ich hier vergessen, also hier Deutsch M mit.

Erstens, die Trägermenge des Modells ist gerade das Erbrauch-Universum, das heißt das Modell besteht aus allen abgeschlossenen Termen.

Und zweitens, die Funktionssymbole werden so interpretiert, wie man es erwartet.

Na, wie erwartet man das denn?

Also ich habe einen Haufen Terme, ein Stück, auf die ich ein endstelliges Funktionssymbol anwenden möchte.

Das erste, was mir einfällt, ist schlicht und einfach diese Endterme in die Funktion einzusetzen und einen neuen Term zu bekommen.

Und genau das ist das, was ich hier verlange.

Das heißt also für ein Funktionssymbol Stelligkeit N in Sigma gilt, ja, das haben wir, wir haben die Interpretation des Funktionssymbols in M.

Das ist eine Funktion auf dem Grundbereich, der Grundbereich ist das Erbrauch-Universum.

Das heißt ich muss sagen, was tut diese Funktion, wenn ich sie anwende auf N Elemente des Grundbereichs, also N geschlossene Terme E1 bis EN.

Naja, der geschlossene Term, den ich dann rausbekommen will, ist einfach der, den ich kriege, indem ich hier die Termbildungsregel anwende.

Ich kann F anwenden auf die Terme E1 bis EN und bekomme einen geschlossenen Term.