3.5 Interpretationen und Modelle von Formeln der PL1S

Die Semantik für die PL1S ist wesentlich komplizierter als die Semantik für die Aussagenlogik. Znächst muss sie festlegen, für welche Objekte die Konstanten und andere Terme stehen können. Die Menge aller betrachteten Objekte wird im sogenannten Universum (oder Diskursuniversum) zusammengefasst. Darauf aufbauend ist zu definieren, wie der Wahrheitswertvon atomaren Formeln zustande kommt. Ferner muss die Deutung der Quantoren festgelegt werden. Das einzige, was einfach aus der Semantik der Aussagenlogik übernommen werden kann, ist die Deutung der Junktoren. Trotzdem ist die Semantik der PL1S nur eine Erweiterung der Semantik für die Aussagenlogik. Die folgenden beiden Sätze sind nützliche Hilfsmittel für die erforderlichen Definitionen und können ähnlich bewiesen werden wie Satz 3.3.2.

Satz 3.5.1 (Definitionsprinzip der strukturellen Rekursion für Terme der PL1S).

Sei eine Sprache der Prädikatenlogik erster Stufe. Um eine Funktion Φ:τ→B von der Menge der -Terme in einen Wertebereich B eindeutig zu definieren, genügen folgende Angaben für Φ:

Basisfälle:
1.1 Der Wert von Φ auf jeder Variablen wird explizit angegeben.
1.2 Der Wert von Φ auf jeder Konstanten wird explizit angegeben.
Rekursionsfälle:
Der Wert von Φ auf zusammengesetzten Termen der Gestalt f(t₁,...,t_n)
wird für jedes n-stellige (n≥1) Funktionssymbol f in Abhängigkeit von den
Werten von Φ auf den Termen t₁ und ... und t_n definiert.

Satz 3.5.2 (Definitionsprinzip der strukturellen Rekursion für Formeln der PL1S).

Sei eine Sprache der Prädikatenlogik erster Stufe. Um eine Funktion Φ:F->B von der Menge der -Formeln in einen Wertebereich B eindeutig zu definieren, genügen folgende Angaben für Φ:

Basisfälle:
1.1 Die Werte von Φ auf $\bot$ und $\ensuremath{{\cal L}}$ werden explizit angegeben.
1.2 Der Wert von Φ auf jeder atomaren -Formel wird explizit angegeben.
Rekursionsfälle:
2.1 Der Wert von Φ auf zusammengesetzten Formeln der Gestalt ¬F wird in Abhängigkeit von dem Wert von Φ auf der Teilformel F definiert.
2.2 Der Wert von Φ auf zusammengesetzten Formeln der Gestalt (FθG) wird für jeden zweistelligen Junktor θ in Anghängigkeit von den Werten von Φ auf den Teilformeln F und G definiert.
2.3 Der Wert von Φ auf zusammengesetzten Formeln der Gestalt QxG wird für jeden Quantor Q in Anghängigkeit von dem Wert von Φ auf der Teilformel F definiert.

Eine Interpretation für eine Sprache der Prädikatenlogik erster Stufe muss in erster Linie die Symbole der Signatur von interpretieren. Die Grundidee ist, dass sie den Funktionssymbolen Funktionen zuordnet und den Relationssymbolen Relationen. Zusätzlich müssen aber auch die Variablen berücksichtigt werden. Dies geschieht durch eine sogenannte Umgebung.

Definition 3.5.4 (Interpretation einer Sprache der PL1S).

Sei eine Sprache der Prädikatenlogik erster Stufe. Eine -Interpretation M ist ein Tripel (D,Ab,U) mit:

D ist eine nichtleere Menge, genannt das Universum von M (auch: Diskursuniversum, Diskursbereich, Domäne).
Ab ist eine auf der Signatur von definierte Abbildung mit:
1. Ab bildet jedes n-stellige (n≥1) Funktionssymbol f von ab auf eine Funktion Ab(f): D x ... x D -> D
  Für n=0 ist Ab(f) ∈ D.
2. Ab bildet jedes n-stellige (n≥1) Relationssymbol p von ab auf eine Relation Ab(p) ⊆ D x ... x D
  Für n=0 ist Ab(p) ∈ {w,f}
U ist eine D-Umgebung.
Ist M=(D,Ab,U) eine -Interpretation, so bezeichnet
U_niv := D das Universum von M
f^M := Ab(f) die Funktion zum Funktionssymbol f
p^M := Ab(p) die Relation zum Relationssymbol p

Das Universum einer Interpretation darf nicht leer sein, damit U und Ab überhaupt definierbar sind. Außerdem würde sonst der (uninteressante) Sonderfall auftreten, dass jede Existenzaussage von vornherein falsch wäre.

Definition 3.5.5 (Wert eines Terms unter einer Interpretation).

Der Wert t^M eines -Terms t unter einer -Interpretation M=(D,Ab,U) ist rekursiv über den Aufbau von t definiert:
x^M := U(x) (Variable)
c^M := Ab(x) (Konstante)
f(t₁,...,t_n)^M := Ab(f)(t₁^M,...,t_n^M) (zusammengesetzter Term)

Diese Definition ist eine Anwendung des Definitionsprinzips der strukturellen Rekursion für Terme. Der Wert eines Terms unter einer Interpretation ist immer ein Objekt aus dem Universum der Interpretation.

Notation 3.5.6. Ist D eine nichtleere Menge, U eine D-Umgebung, ferner d ∈ D und x eine Variable, so bezeichnet U[d/x] die folgende D-Umgebung:

U[d/x](y) :=	U(y)	falls y ≠ x
	d	falls y = x

Ist M=(D,Ab,U) eine

-Interpretation und d ∈ D, so bezeichnet M[d/x] die

-Interpretation (D,Ab,U[d/x]).

Definition 3.5.7 (Modellbeziehung).

Sei eine Sprache der Prädikatenlogik erster Stufe. Für eine -Interpretation M=(D,Ab,U) und eine -Formel F ist die Modellbeziehung MF rekursiv über den Aufbau von F definiert:

M $\bot$		gilt
M $\ensuremath{{\cal L}}$		gilt nicht
M p	gdw.	p^M = w (p nullstellig)
M p(t₁,...,t_n)	gdw.	(t₁^M,...,t_n^M)∈p^M (p n-stellig, n≥1)
M ¬G	gdw.	M G nicht gilt
M G₁∧G₂	gdw.	M G₁ und M G₂
M G₁∨G₂	gdw.	M G₁ oder M G₂
M G₁⇒G₂	gdw.	wenn M G₁, so M G₂
M G₁⇔G₂	gdw.	entweder M G₁ und M G₂ oder weder M G₁ noch M G₂
M ∀xG	gdw.	für alle d∈D gilt M[d/x] G
M ∃xG	gdw.	es gibt ein d∈D mit M[d/x] G

Die Schreibweise M(F) = w anstelle von M F ist für die Prädikatenlogik erster Stufe weniger gebräuchlich und wurde deshalb in der obigen Definition nicht eingeführt. Die Möglichkeit dieser alternativen Schreibweise macht aber klar, dass eine -Interpretation im Prinzip als eine Funktion betrachtet werden kann, die jeder -Formel einen Wahrheitswert zuordnet. Wie wir vorher schon bemerkt haben, ist eine -Interpretation außerdem auch eine Funktion, die jedem -Term ein Objekt aus ihrem Universum zuordnet.

Die Definitionsprinzipien der strukturellen Rekursion für Terme und Formeln der PL1S stellen sicher, dass diese Werte für alle Terme und Formeln eindeutig bestimmst sind.

Die übrigen semantischen Begriffe werden jetzt ganz genau wie für die Aussagenlogik definiert.

Definition 3.5.8 (Modellbeziehung, Folgerungsbeziehung, logische Äquivalenz).

M bezeichne eine -Interpretation, F und G bezeichne -Formeln, S bezeichne eine Menge von -Formeln.

M erfüllt F (oder M ist ein Modell von F) gdw. M F. Andernsfalls: M falsifiziert F, notiert M ? F. M erfüllt S (oder M ist ein Modell von S), notiert M S, gdw. M F für jedes F ∈ S. Andernfalls: M falsifiziert S, notiert M ? S.
Eine -Formel (oder Menge von -Formeln) heißt
- allgemeingültig gdw. sie von jeder -Interpretation erfüllt wird
- erfüllbar gdw. sie von einer -Interpretation erfüllt wird
- falsifiziert gdw. sie von einer -Interpretation falsifiziert wird
- unerfüllbar gdw. sie von jeder -Interpretation falsifiziert wird
Eine allgemeingültige Formel nennt man auch Tautologie, eine unerfüllbare Formel(menge) auch widersprüchlich, eine erfüllbare Formel(menge) auch widerspruchsfrei.
Aus F folgt G, notiert F G, gdw. für jede -Interpretation M gilt: wenn M F dann M G (jedes Modell von F erfüllt auch G). F, G sind logisch äquivalent, notiert F G, gdw. F G und G F (F und G haben dieselben Modelle).
Die Folgerungsbeziehung F G und die logische Äquivalenz F G sind genauso diefiniert, wenn F oder G oder sowohl F als auch G eine Formelmenge ist.

Die Bemerkungen, dass das Zeichen überladen ist und dass eine Menge S nur im endlichen Fall durch die Konjunktion ihrer Elemente ersetzt werden kann, geleten hier ganz genauso wie die aussagenlogische Definition 3.3.4. Ferner gilt wie für die Aussagenlogik der Satz:

Satz 3.5.9

Sei eine Sprache der Prädikatenlogik erster Stufe, seien F und G -Formeln.

Ist F allgemeingültig, so ist ¬F unerfüllbar.
Ist F unerfüllbar, so ist ¬F allgemeingültig.
Ist F erfüllbar und falsifizierbar, so ist ¬F erfüllbar und falsifizierbar.
F G gdw. ¬G ¬F
gdw. (F G) allgemeingültig ist
gdw. (F∧¬ G) unerfüllbar ist.
F G gdw. ¬F ¬G
gdw. (FG) allgemeingültig ist.

Die folgenden Sätze haben dagegen keine Entsprechung in der Aussagenlogik, da sie sich auf die Struktur von Termen beziehen.

Satz 3.5.10 (Koinzidenzsatz).

Seien M₁=(D,Ab,U₁) und M₂=(D,Ab,U₂) -Interpretationen mit demselben Universum D und derselben Funktion Ab. Sei t ein -Term und F eine -Formel

Gilt U₁(x)=U₂(x) für alle x ∈ var(t) so ist t^M₁=t^M₂.
Gilt U₁(x)=U₂(x) für alle x ∈ fvar(t) so gilt M₁ F gdw. M₂ F.

Beweis: Strukturelle Induktion über den Term- bzw. Formelaufbau.

Basisfall Variable x: nach Voraussetzung x^M₁=U₁(x)=U₂(x)=x^M₂.
Basisfall Konstante c: nach Definition c^M₁=Ab(c)=c^M₂.
Induktionsfall f(t₁,...,t_n): Es gelte t₁^M₁=t₁^M₂,...,t_n^M₁=t_n^M₂, dann gilt
f(t₁,...,t_n)^M₁ = Ab(f)(t₁^M₁,...,t_n^M₁) nach Definition
= Ab(f)(t₁^M₂,...,t_n^M₂) nach Induktionsannahme
= f(t₁,...,t_n)^M₂ nach Definition
Ähnlich wie 1.

Geschlossene Formeln enthalten nach Definition keine freien Variablen. Dafür bedeutet der Koinzidenzsatz: Ist eine -Interpretation M=(D,Ab,U) ein Modell einer geschlossenen Formel F, so ist für jede beliebige D-Umgebung U' die -Interpretation M=(D,Ab,U') ebenfalls ein Modell von F.
Die Umgebung dient also nur dazu, nichtgeschlossene Formeln zu interpretieren, wie etwa die nichtgeschlossene Teilformel G von ∀xG und ∃xG in Definition 3.5.7. Für geschlossene Formeln ist die Umgebung irrelevant.

Notation 3.5.11 (Elementare Substitution). Seien s und t

-Terme, F eine

-Formel und x eine Variable.

t[s/x] sei der Term, der entsteht, wenn man alle Vorkommen von x in t durch s ersetzt.
F[s/x] sei die Formel, die entsteht, wenn man alle freien Vorkommen von x in F durch s ersetzt.

Dabei heißt [s/x] eine elementare Substitution.

Bemerkung: Im Ersetzungssatz 3.3.6 wurde die Notation F <G₂/V_G₁> für die Ersetzung eines Vorkommens der Formel G₁ in F durch G₂ benutzt. Im Gegensatz dazu bezeichnet die Notation F[s/x] die Ersetzung aller freien Vorkommen der Variablen x in F durch s. Die unterschiedlichen Notationen <...> und [...] sollen diesen Unterschied hervorheben.

Die Notation F[s/x] erinnert an die Schreibweise M[d/x] (Notation 3.5.6) für eine Interpretation und ihre Umgebung. Aber s ist ein Term, also etwas syntaktisches, und d ein Objekt des Universums von M, also etwas semantisches. Der folgende Satz stellt einen wichtigen Zusammenhang her.

Der Substitutionssatz erlaubt eine Art Übersetzung zwischen Syntax und Semantik: der syntaktische Term s entspricht semantisch einem Objekt s^M des Universums. Es ist egal, ob man einer Variablen dieses Objekt semantisch über die Umgebung zuordnet (mittels M[s^M/x]) oder die Variable syntaktisch durch den Term ersetzt (mittels t[s/x] bzw. F[s/x]).

Satz 3.5.13.

Der Ersetzungssatz 3.3.6 gilt auch für -Formeln.
Die Regeln von Satz 3.3.7 gelten auch für -Formeln.
Regeln der überflüssigen Quantoren: falls x ∉ fvar(F), gilt
∀xF F und ∃xF F.
Variablenumbenennungsregeln: falls x' ∉ fvar(F), gilt
∀xF ∀x'F[x'/x] und ∃xF ∃x'F[x'/x] .
Quantorenvertauschungsregeln:
∀x∀yF ∀y∀xF und ∃x∃yF ∃y∃xF
Achtung: im Allgemeinen aber ∀x∃yF nicht ∃y∀xF
Regeln der negierten Quantoren:
¬∀xF ∃x¬F ¬∃xF ∀x¬F
Quantor/Junktor-Verträglichkeitsregeln:
∀x(F∧G) ((∀xF)∧(∀xG)) und ∃x(F∨G) ((∃xF)∨(∃xG))
Variablenverschmelzungsregeln:
∀x∀yF ∀xF[x/y] und ∃x∃yF ? ∃xF[x/y]
Achtung: im Allgemeinen gilt hier nicht.