Kurs:Einführung in die mathematische Logik (Osnabrück 2014)/Vorlesung 9/kontrolle

Freie Variablen

In einem Ausdruck ${}\alpha \in L^{S}$ über einem Symbolalphabet ${}S$ nennt man die Variablen, die (und zwar für jedes Vorkommen) innerhalb der Reichweite eines Quantors stehen, gebunden, die anderen frei. Dies wird streng über den Aufbau der Ausdrücke definiert.

1. ${}\operatorname {Frei} \,(t_{1}=t_{2})=\operatorname {Var} \,(t_{1})\cup \operatorname {Var} \,(t_{2})\,.$

2. ${}\operatorname {Frei} \,(Rt_{1}\ldots t_{n})=\operatorname {Var} \,(t_{1})\cup \operatorname {Var} \,(t_{2})\cup \ldots \cup \operatorname {Var} \,(t_{n})\,$

   für ein ${}n$-stelliges Relationssymbol ${}R$ und ${}n$ Terme ${}t_{1},t_{2},\ldots ,t_{n}$.

3. ${}\operatorname {Frei} \,(\neg \alpha )=\operatorname {Frei} \,(\alpha )\,$

   für einen Ausdruck ${}\alpha$.

4. ${}\operatorname {Frei} \,(\alpha \rightarrow \beta )=\operatorname {Frei} \,(\alpha )\cup \operatorname {Frei} \,(\beta )\,$

   für Ausdrücke ${}\alpha$ und ${}\beta$. Ebenso für ${}\leftrightarrow ,\wedge ,\vee$.

5. ${}\operatorname {Frei} \,(\forall x\alpha )=\operatorname {Frei} \,(\alpha )\setminus \{x\}\,$

   für einen Ausdruck ${}\alpha$ und eine Variable ${}x$.

6. ${}\operatorname {Frei} \,(\exists x\alpha )=\operatorname {Frei} \,(\alpha )\setminus \{x\}\,$

   für einen Ausdruck ${}\alpha$ und eine Variable ${}x$.

Einen Ausdruck ohne freie Variablen nennt man einen Satz, auch wenn diese Bezeichnung nicht ganz glücklich ist, da „Satz“ die Gültigkeit einer Aussage suggeriert. Die Menge der Sätze wird mit ${}L_{0}^{S}$ bezeichnet, die Menge der Ausdrücke mit genau einer freien Variablen (die aber in dem Ausdruck beliebig oft vorkommen darf) mit ${}L_{1}^{S}$.

Das Koinzidenzlemma

Die folgende Aussage, das Koinzidenzlemma, zeigt, dass der Wert eines Terms und die Gültigkeit eines Ausdrucks unter einer Interpretation (bei einer fixierten ${}S$-Struktur) nur von den in dem Term vorkommenden Variablen bzw. in dem Ausdruck vorkommenden freien Variablen abhängt. Ihr Beweis ist ein typisches Beispiel für einen Beweis durch Induktion über den Aufbau der Terme bzw. Ausdrücke.

Lemma Referenznummer erstellen

Es sei ${}S$ ein Symbolalphabet erster Stufe und ${}U\subseteq S$ eine Teilmenge. Es sei ${}t$ ein ${}U$- Term und ${}\alpha$ ein ${}U$- Ausdruck. Es seien zwei ${}S$- Interpretationen ${}I_{1}$ und ${}I_{2}$ in einer gemeinsamen Grundmenge ${}M$ gegeben, die auf ${}U$ identisch seien. Dann gelten folgende Aussagen.

1. Es ist ${}I_{1}(t)=I_{2}(t)$.
2. Es ist ${}I_{1}\vDash \alpha$ genau dann, wenn ${}I_{2}\vDash \alpha$ (dazu genügt bereits, dass die Interpretationen auf den Symbolen aus ${}U$ und auf den in ${}\alpha$ frei vorkommenden Variablen identisch sind).

Beweis

(1). Wir führen Induktion über den Aufbau der ${}U$-Terme. Für den Induktionsanfang müssen wir Variablen und Konstanten aus ${}U$ betrachten. Für eine Variable ${}x$ (oder eine Konstante) aus ${}U$ ist nach Voraussetzung ${}I_{1}(x)=I_{2}(x)$. Im Induktionsschritt können wir annehmen, dass ein ${}n$-stelliges Funktionssymbol ${}f$ aus ${}U$ gegeben ist sowie ${}U$-Terme ${}t_{1},\ldots ,t_{n}$, für die die Interpretationsgleichheit schon gezeigt wurde. Nach Voraussetzung wird ${}f$ in beiden Interpretationen durch die gleiche Funktion ${}f^{M}$ interpretiert. Daher ist

${}{\begin{aligned}I_{1}(ft_{1}\ldots t_{n})&=f^{M}(I_{1}(t_{1}),\ldots ,I_{1}(t_{n}))\\&=f^{M}(I_{2}(t_{1}),\ldots ,I_{2}(t_{n}))\\&=I_{2}(ft_{1}\ldots t_{n}).\end{aligned}}$

(2). Wir führen Induktion über den Aufbau der ${}U$-Ausdrücke, wobei die zu beweisende Aussage über je zwei Interpretationen zu verstehen ist. Für die Gleichheit und ein Relationssymbol ${}R$ aus ${}U$ folgt die Aussage unmittelbar aus (1), da ja ${}R$ in beiden Interpretationen als die gleiche Relation zu interpretieren ist. Der Induktionsschritt ist für Ausdrücke der Form ${}\neg \alpha ,\,\alpha \wedge \beta ,\,\alpha \rightarrow \beta$ aufgrund der Modellbeziehung unmittelbar klar. Es sei nun ein ${}U$-Ausdruck der Form ${}\exists x\alpha$ gegeben, und es gelte ${}I_{1}\vDash \exists x\alpha$. Dies bedeutet aufgrund der Modellbeziehung, dass es ein ${}m\in M$ derart gibt, dass ${}I_{1}{\frac {m}{x}}\vDash \alpha$ gilt. Die beiden umbelegten Interpretationen ${}I_{1}{\frac {m}{x}}$ und ${}I_{2}{\frac {m}{x}}$ stimmen auf den Symbolen aus ${}U$ und den in ${}\alpha$ frei vorkommenden Variablen überein: Die Variable ${}x$ wird so oder so als ${}m$ interpretiert und die anderen freien Variablen aus ${}\alpha$ sind auch in ${}\exists x\alpha$ frei. Nach Induktionsvoraussetzung gilt ${}I_{2}{\frac {m}{x}}\vDash \alpha$ und daher wiederum ${}I_{2}\vDash \exists x\alpha$.

$\Box$

Substitution

Wir besprechen nun die Variablensubstitution, wobei wir weitgehend der Darstellung von Ebbinghaus, Flum, Thomas folgen.

Variablen repräsentieren verschiedene Werte, die man für sie einsetzen kann. Auf formaler Ebene bedeutet dies, dass eine oder mehrere Variablen durch gewisse Terme ersetzt werden. Im semantischen Kontext wird dies durch die Uminterpretation von Variablen bei einer Interpretation präzise gemacht. Im syntaktischen Kontext spricht man von Substitution, die wir nun definienren werden. In der Ersetzung macht es einen großen Unterschied, ob gebundene oder freie Variablen vorliegen. Der Ausdruck

$x\geq 0\rightarrow \exists y(x=y\cdot y)$

bedeutet in einem angeordneten Körper interpretiert, dass die nichtnegative Zahl ${}x$ als Quadrat darstellbar ist (also eine Quadratwurzel besitzt), was für ${}\mathbb {R}$ wahr ist, für ${}\mathbb {Q}$ im Allgemeinen (das hängt von der Interpretation für ${}x$ ab) nicht. Gleichbedeutend (bei einer inhaltlichen Interpretation) mit diesem Ausdruck ist

$x\geq 0\rightarrow \exists z(x=z\cdot z),$

aber nicht

$x\geq 0\rightarrow \exists x(x=x\cdot x),$

das nur bei ${}x=0$ oder ${}x=1$ wahr ist. Von daher wird die weiter unten zu gebende Definition für die Substitution von Ausdrücken berücksichtigen, ob Variablen frei oder gebunden sind. Ferner wird es wichtig sein, in einem Ausdruck neue Variablen einzuführen. Damit diese Konstruktion eindeutig definiert ist, legen wir entweder eine durchnummerierte (und abzählbare) Variablenmenge ${}v_{1},v_{2},v_{3}\ldots$ zugrunde, oder aber eine beliebig große Variablenmenge, die mit einer Wohlordnung versehen sei.

Definition Referenznummer erstellen

Es sei ein Symbolalphabet ${}S$ einer Sprache erster Stufe gegeben. Es seien ${}x_{1},\ldots ,x_{k}$ paarweise verschiedene Variablen und ${}t_{1},\ldots ,t_{k}$ fixierte ${}S$- Terme. Dann definiert man rekursiv über den Aufbau der Terme die Substitution ${}s{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}$ für jeden ${}S$-Term ${}s$.

1. Für eine Variable ${}x$ ist

   ${}x{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:={\begin{cases}x,{\text{ falls }}x\neq x_{i}{\text{ für alle }}i\,,\\t_{i},{\text{ falls }}x=x_{i}\,.\end{cases}}\,$

2. Für eine Konstante ${}c$ ist

   ${}c{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:=c\,.$

3. Für ein ${}n$-stelliges Funktionssymbol ${}f$ und ${}n$ Terme ${}s_{1},\ldots ,s_{n}$ ist

   ${}fs_{1}\ldots s_{n}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:=fs_{1}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\ldots s_{n}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\,.$

Beispiel Referenznummer erstellen

Es seien ${}c,d$ Konstanten einer erststufigen Sprache, ${}x,y,z,v$ Variablen, ${}p$ ein einstelliges und ${}f,g,h$ zweistellige Funktionssymbole. Wir betrachten den Term

$t=fpxgcy$

und die Substitution

${\frac {d,\,\,\,hvx,\,\,\,v}{x,\,\,\,\,\,\,y,\,\,\,\,\,\,z}}.$

Die Substitution wird durchgeführt, indem man die kleinsten Bestandteile des Termes, also ${}x,y,c$, ersetzt und ansonsten den funktionalen Aufbau des Termes übernimmt. Für diese gilt

${}x{\frac {d,\,\,\,hvx,\,\,\,v}{x,\,\,\,\,\,\,y,\,\,\,\,\,\,z}}=d\,,$

${}y{\frac {d,\,\,\,hvx,\,\,\,v}{x,\,\,\,\,\,\,y,\,\,\,\,\,\,z}}=hvx\,$

und

${}c{\frac {d,\,\,\,hvx,\,\,\,v}{x,\,\,\,\,\,\,y,\,\,\,\,\,\,z}}=c\,.$

Also ist

${}fpxgcy{\frac {d,\,\,\,hvx,\,\,\,v}{x,\,\,\,\,\,\,y,\,\,\,\,\,\,z}}=fpdgchvx\,.$

Man beachte, dass das letzte ${}x$ nicht zu ersetzen ist.

Definition Definition 9.4 ändern

Es sei ein Symbolalphabet ${}S$ einer Sprache erster Stufe gegeben. Es seien ${}x_{1},\ldots ,x_{k}$ paarweise verschiedene Variablen und ${}t_{1},\ldots ,t_{k}$ fixierte ${}S$- Terme. Dann definiert man rekursiv über den Aufbau der ${}S$- Ausdrücke die Substitution ${}\alpha {\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}$ für jeden ${}S$-Ausdruck ${}\alpha$.

1. Für Terme ${}s_{1},s_{2}$ setzt man

   ${}(s_{1}=s_{2}){\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:=s_{1}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}=s_{2}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\,.$

2. Für ein ${}n$-stelliges Relationssymbol ${}R$ und ${}n$ Terme ${}s_{1},\ldots ,s_{n}$ setzt man

   ${}(Rs_{1}\ldots s_{n}){\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:=Rs_{1}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\ldots s_{n}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\,.$

3. Für einen Ausdruck ${}\alpha$ setzt man

   ${}(\neg \alpha ){\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:=\neg \alpha {\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\,.$

4. Für Ausdrücke ${}\alpha$ und ${}\beta$ setzt man

   ${}(\alpha \wedge \beta ){\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:=\alpha {\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\wedge \beta {\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\,$

   und ebenso für die anderen zweistelligen Junktoren.

5. Für einen Ausdruck ${}\alpha$ seien ${}x_{i_{1}},\ldots ,x_{i_{r}}$ diejenigen Variablen (unter den $x_{1},\ldots ,x_{k}$), die in ${}\forall x\alpha$ frei vorkommen. Es sei ${}v=x$, falls ${}x$ nicht in ${}t_{i_{1}},\ldots ,t_{i_{r}}$ vorkommt. Andernfalls sei ${}v$ die erste Variable (in einer fixierten Variablenaufzählung, falls es abzählbar viele Variablen gibt, bzw. in einer fixierten Wohlordnung der Variablenmenge), die weder in ${}\alpha$ noch in ${}t_{i_{1}},\ldots ,t_{i_{r}}$ vorkommt. Dann setzt man

   ${}(\forall x\alpha ){\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:=\forall v\alpha {\frac {t_{i_{1}},\ldots ,t_{i_{r}},v}{x_{i_{1}},\ldots ,x_{i_{r}},x}}\,$

   und ebenso für den Existenzquantor.

Beispiel Referenznummer erstellen

Es seien ${}c,d$ Konstanten einer erststufigen Sprache, ${}x,y,z,u$ Variablen (so geordnet), ${}f,g$ einstellige Funktionssymbole und ${}R$ ein zweistelliges Relationssymbol. Wir betrachten den Ausdruck

${}\alpha =\forall x\neg Ryfx\,$

und die Substitution

${\frac {u,\,\,\,\,gc}{x,\,\,\,\,\,\,y}}.$

Von den zu substituierenden Variablen ist ${}x$ gebunden und ${}y$ frei. Die Variable ${}x$ kommt in den substituierenden Termen nicht vor. Also ist

${}{\left(\forall x\neg Ryfx\right)}{\frac {u,\,\,\,\,gc}{x,\,\,\,\,\,\,y}}=\forall x{\left(\neg Ryfx{\frac {gc}{y}}\right)}=\forall x\neg Rgcfx\,.$

Bei der Substitution

${\frac {u,\,\,\,\,gx}{x,\,\,\,\,\,\,y}}$

kommt jetzt die gebundene Variable ${}x$ in dem substituierenden Term ${}gx$ vor. Es ist ${}v=z$ die nächste Variable in der gegebenen Reihenfolge. Somit ist

${}{\left(\forall x\neg Ryfx\right)}{\frac {u,\,\,\,\,gx}{x,\,\,\,\,\,\,y}}=\forall z{\left(\neg Ryfx{\frac {gx,\,\,\,\,z}{y,\,\,\,\,\,\,x}}\right)}=\forall z\neg Rgxfz\,.$

Die folgende Aussage, das Substitutionslemma, stiftet eine Beziehung zwischen Substitutionen und Uminterpretationen.

In Verallgemeinerung der Schreibweise ${}I{\frac {m}{x}}$ für eine Uminterpretation schreiben wir ${}I{\frac {m_{1},\ldots ,m_{k}}{x_{1},\ldots ,x_{k}}}$ für die sukzessive Uminterpretation der untereinander verschiedenen Variablen ${}x_{1},\ldots ,x_{k}$ (dabei seien $m_{1},\ldots ,m_{k}$ Elemente der Grundmenge ${}M$ der Interpretation). Es werden also die ${}x_{i}$ als ${}m_{i}$ interpretiert und alle anderen Variablen werden gemäß ${}I$ interpretiert.

Lemma Lemma 9.6 ändern

Es sei ein Symbolalphabet ${}S$ einer Sprache erster Stufe gegeben und es seien ${}x_{1},\ldots ,x_{k}$ paarweise verschiedene Variablen und ${}t_{1},\ldots ,t_{k}$ fixierte ${}S$- Terme. Es sei eine ${}S$- Interpretation ${}I$ gegeben. Dann gelten folgende Aussagen.

1. Für jeden ${}S$- Term ${}s$ gilt

   ${}I{\left(s{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}={\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}(s)\,.$

2. Für jeden ${}S$- Ausdruck ${}\alpha$ gilt

   $I\vDash \alpha {\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}{\text{ genau dann, wenn }}{\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}\vDash \alpha .$

Beweis

Dies wird über den induktiven Aufbau der Terme bzw. der Ausdrücke bewiesen. (1). Für eine Konstante ${}c$ ist die Aussage richtig, da ihre Interpretation unverändert ist. Für eine Variable ${}x$ macht man eine Fallunterscheidung. Wenn

${}x=x_{i}\,$

mit einer der an der Substitution beteiligten Variablen ist, so ist

${}I{\left(x_{i}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}=I(t_{i})={\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}(x_{i})\,.$

Bei einer an der Substitution nicht beteiligten Variablen ${}x$ ist

${}I{\left(x{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}=I(x)={\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}(x)\,.$

Wenn ${}f$ ein ${}n$-stelliges Funktionssymbol ist und ${}s_{1},\ldots ,s_{n}$ Terme sind, für die die Gleichheit schon bekannt ist, so ist

${}{\begin{aligned}I{\left({\left(fs_{1}\ldots s_{n}\right)}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}&=I{\left(fs_{1}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\ldots s_{n}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}\\&=I(f){\left(I{\left(s_{1}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)},\ldots ,I{\left(s_{n}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}\right)}\\&=I(f){\left({\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}(s_{1}),\ldots ,{\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}(s_{n})\right)}\\&={\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}(f){\left({\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}{\left(s_{1}\right)},\ldots ,{\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}{\left(s_{n}\right)}\right)}\\&={\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}{\left(fs_{1}\ldots s_{n}\right)}.\end{aligned}}$

(2). Für einen Ausdruck der Form ${}s=t$ bedeutet

$I\vDash {\left(s=t\right)}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}$

einfach

$I\vDash s{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}=t{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}.$

Dies ist äquivalent zu

${}I{\left(s{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}=I{\left(t{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}\,,$

was nach dem ersten Teil einfach

${}I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}(s)=I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}(t)\,$

bedeutet. Dies wiederum ist äquivalent zu

$I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\vDash s=t.$

Es sei nun ${}R$ ein ${}n$-stelliges Relationssymbol und seien ${}s_{1},\ldots ,s_{n}$ Terme. Die Gültigkeit

$I\vDash {\left(Rs_{1}\ldots s_{n}\right)}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}$

bedeutet

$I\vDash Rs_{1}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\ldots s_{n}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}$

und dies bedeutet, dass

${\left(I{\left(s_{1}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)},\ldots ,I{\left(s_{n}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}\right)}$

zur Relation ${}I(R)$ gehört. Nach dem ersten Teil ist dieses Tupel gleich

${\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}(s_{1}),\ldots ,I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}(s_{n})\right)}.$

Wegen ${}R(I)=R{\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}$ ist dies äquivalent zu

$I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\vDash Rs_{1}\ldots s_{n}.$

Für die weiteren Aussagen beweist man die Äquivalenz durch Induktion über den Aufbau der Ausdrücke, und zwar über alle Interpretationen simultan; dies ist für die aussagenlogischen Junktoren unmittelbar klar. Betrachten wir also einen Ausdruck der Form ${}\forall x\alpha$. Die Gültigkeit

$I\vDash {\left(\forall x\alpha \right)}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}$

bedeutet gemäß der Festlegung in Definition 9.4, dass

$I\vDash \forall v\alpha {\frac {t_{i_{1}},\ldots ,t_{i_{r}},v}{x_{i_{1}},\ldots ,x_{i_{r}},x}}$

gilt, wobei ${}v$ in ${}t_{i_{1}},\ldots ,t_{i_{r}}$ nicht vorkommt. Dies bedeutet, dass für jedes ${}m\in M$ der Grundmenge der Interpretation die Beziehung

$I{\frac {m}{v}}\vDash \alpha {\frac {t_{i_{1}},\ldots ,t_{i_{r}},v}{x_{i_{1}},\ldots ,x_{i_{r}},x}}$

gilt. Nach Induktionsvoraussetzung (angewendet auf die Interpretation $I{\frac {m}{v}}$) bedeutet dies

${\left(I{\frac {m}{v}}\right)}{\frac {{\left(I{\frac {m}{v}}\right)}{\left(t_{i_{1}}\right)},\ldots ,{\left(I{\frac {m}{v}}\right)}{\left(t_{i_{r}}\right)},{\left(I{\frac {m}{v}}\right)}{\left(v\right)}}{x_{i_{1}},\ldots ,x_{i_{r}},x}}\vDash \alpha$

für alle ${}m\in M$. Aufgrund des Koinzidenzlemmas ist dies äquivalent zu

${\left(I{\frac {m}{v}}\right)}{\frac {I{\left(t_{i_{1}}\right)},\ldots ,I{\left(t_{i_{r}}\right)},m}{x_{i_{1}},\ldots ,x_{i_{r}},x}}\vDash \alpha .$

Dies ist äquivalent (für alle ${}m\in M$) zu

$I{\frac {I{\left(t_{i_{1}}\right)},\ldots ,I{\left(t_{i_{r}}\right)},m}{x_{i_{1}},\ldots ,x_{i_{r}},x}}\vDash \alpha ,$

was bei ${}v=x$ klar ist und bei ${}v\neq x$ aus dem Koinzidenzlemma folgt, da dann ${}v$ nicht in ${}\alpha$ vorkommt. Dies bedeutet wiederum

$I{\frac {I{\left(t_{i_{1}}\right)},\ldots ,I{\left(t_{i_{r}}\right)}}{x_{i_{1}},\ldots ,x_{i_{r}}}}\vDash \forall x\alpha$

und damit, wiederum nach dem Koinzidenzlemma, da die von ${}x_{i_{j}}$ verschiedenen Variablen in ${}\forall x\alpha$ nicht frei vorkommen,

$I{\frac {I{\left(t_{1}\right)},\ldots ,I{\left(t_{k}\right)}}{x_{1},\ldots ,x_{k}}}\vDash \forall x\alpha .$

$\Box$

Fußnoten