Kurs:Einführung in die mathematische Logik (Osnabrück 2016)/Vorlesung 9/latex
\setcounter{section}{9}
\zwischenueberschrift{Freie Variablen}
In einem Ausdruck
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{L^S
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
über einem Symbolalphabet $S$ nennt man die Variablen, die
\zusatzklammer {und zwar für jedes Vorkommen} {} {}
innerhalb der Reichweite eines Quantors stehen, \stichwort {gebunden} {,} die anderen \stichwort {frei} {.} Dies wird streng über den Aufbau der Ausdrücke definiert.
\aufzaehlungsechs{
\mavergleichskettedisp
{\vergleichskette
{ \operatorname{Frei} \, (t_1 = t_2)
}
{ =} {\operatorname{Var} \, (t_1) \cup \operatorname{Var} \, (t_2)
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{.}
}{
\mavergleichskettedisp
{\vergleichskette
{ \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
\mathl{t_1,t_2 , \ldots , t_n}{.}
}{
\mavergleichskettedisp
{\vergleichskette
{\operatorname{Frei} \, ( \neg \alpha)
}
{ =} {\operatorname{Frei} \, ( \alpha)
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
für einen Ausdruck $\alpha$.
}{
\mavergleichskettedisp
{\vergleichskette
{\operatorname{Frei} \, (\alpha \rightarrow \beta)
}
{ =} {\operatorname{Frei} \, (\alpha) \cup \operatorname{Frei} \, ( \beta)
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
für Ausdrücke $\alpha$ und $\beta$. Ebenso für
\mathl{\leftrightarrow, \wedge, \vee}{.}
}{
\mavergleichskettedisp
{\vergleichskette
{ \operatorname{Frei} \, ( \forall x \alpha)
}
{ =} {\operatorname{Frei} \, ( \alpha) \setminus \{x\}
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
für einen Ausdruck $\alpha$ und eine Variable $x$.
}{
\mavergleichskettedisp
{\vergleichskette
{\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 \stichwort {Satz} {,} auch wenn diese Bezeichnung nicht ganz glücklich ist, da \anfuehrung{Satz}{} die Gültigkeit einer Aussage suggeriert. Die Menge der Sätze wird mit
\mathl{L^S_0}{} bezeichnet, die Menge der Ausdrücke mit genau einer freien Variablen
\zusatzklammer {die aber in dem Ausdruck beliebig oft vorkommen darf} {} {}
mit
\mathl{L^S_1}{.}
Beispielsweise ist in
\mathdisp {\forall x (\exist ( y fx=z)) \vee \exist x R (yzx)} { }
die Variable $x$ gebunden, während die Variablen $y,z$ frei sind, wobei die Freiheit von $y$ auf dem freien Vorkommen im hinteren Ausdruck beruht.
\zwischenueberschrift{Das Koinzidenzlemma}
Die folgende Aussage, das Koinzidenzlemma, zeigt, dass der Wert eines Terms und die Gültigkeit eines Ausdrucks unter einer Interpretation \zusatzklammer {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.
\inputfaktbeweis
{Prädikatenlogik/Koinzidenzlemma/Fakt}
{Lemma}
{}
{
\faktsituation {Es sei $S$ ein
\definitionsverweis {Symbolalphabet}{}{}
erster Stufe und
\mavergleichskette
{\vergleichskette
{U
}
{ \subseteq }{S
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
eine Teilmenge. Es sei $t$ ein
$U$-\definitionsverweis {Term}{}{} und $\alpha$ ein $U$-\definitionsverweis {Ausdruck}{}{.}
Es seien zwei
$S$-\definitionsverweis {Interpretationen}{}{}
\mathkor {} {I_1} {und} {I_2} {}
in einer gemeinsamen Grundmenge $M$ gegeben, die auf $U$ identisch seien.}
\faktuebergang {Dann gelten folgende Aussagen.}
\faktfolgerung {\aufzaehlungzwei {Es ist
\mavergleichskette
{\vergleichskette
{ I_1(t)
}
{ = }{I_2(t)
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
} {Es ist
\mathl{I_1 \vDash \alpha}{} genau dann, wenn
\mathl{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).
}}
\faktzusatz {}
\faktzusatz {}
}
{
\teilbeweis {}{}{}
{(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$
\zusatzklammer {oder eine Konstante} {} {}
aus $U$ ist nach Voraussetzung
\mavergleichskette
{\vergleichskette
{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
\mathl{t_1 , \ldots , t_n}{,} für die die Interpretationsgleichheit schon gezeigt wurde. Nach Voraussetzung wird $f$ in beiden Interpretationen durch die gleiche Funktion
\mathl{f^M}{} interpretiert. Daher ist
\mavergleichskettealign
{\vergleichskettealign
{ 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)
}
{ } {
}
}
{}
{}{.}}
{}
\teilbeweis {}{}{}
{(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
\mathl{\neg \alpha,\, \alpha \wedge \beta,\, \alpha \rightarrow \beta}{} aufgrund der Modellbeziehung unmittelbar klar. Es sei nun ein $U$-Ausdruck der Form
\mathl{\exists x \alpha}{} gegeben, und es gelte
\mathl{I_1 \vDash \exists x \alpha}{.} Dies bedeutet aufgrund der Modellbeziehung, dass es ein
\mavergleichskette
{\vergleichskette
{m
}
{ \in }{M
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
derart gibt, dass
\mathl{I_1\frac{m}{x} \vDash \alpha}{} gilt. Die beiden umbelegten Interpretationen
\mathkor {} {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
\mathl{\exists x \alpha}{} frei. Nach Induktionsvoraussetzung gilt
\mathl{I_2 \frac{m}{x} \vDash \alpha}{} und daher wiederum
\mathl{I_2 \vDash \exists x \alpha}{.}}
{}
\zwischenueberschrift{Substitution}
Wir besprechen nun die Variablensubstitution, wobei wir weitgehend der Darstellung von Ebbinghaus, Flum, Thomas folgen.
Variablen repräsentieren verschiedene Werte
\zusatzklammer {in einer Grundmenge $M$} {} {,}
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 definieren werden. In der Ersetzung macht es einen großen Unterschied, ob gebundene oder freie Variablen vorliegen. Der Ausdruck
\mathdisp {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 $\R$ wahr ist, für $\Q$ im Allgemeinen (das hängt von der Interpretation für $x$ ab) nicht. Gleichbedeutend (bei einer inhaltlichen Interpretation) mit diesem Ausdruck ist
\mathdisp {x \geq 0 \rightarrow \exists z (x=z \cdot z)} { , }
aber nicht
\mathdisp {x \geq 0 \rightarrow \exists x (x=x \cdot x)} { , }
das nur bei
\mathkor {} {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
\zusatzklammer {und abzählbare} {} {}
Variablenmenge
\mathl{v_1,v_2, v_3 \ldots}{} zugrunde, oder aber eine beliebig große Variablenmenge, die mit einer Wohlordnung versehen sei.
\inputdefinition
{}
{
Es sei ein Symbolalphabet $S$ einer
\definitionsverweis {Sprache erster Stufe}{}{}
gegeben. Es seien
\mathl{x_1 , \ldots , x_k}{} paarweise verschiedene Variablen und
\mathl{t_1 , \ldots , t_k}{} fixierte
$S$-\definitionsverweis {Terme}{}{.}
Dann definiert man rekursiv über den Aufbau der Terme die Substitution
\mathl{s { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }}{} für jeden $S$-Term $s$.
\aufzaehlungdrei{Für eine Variable $x$ ist
\mavergleichskettedisp
{\vergleichskette
{ x { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }
}
{ \defeq} {\begin{cases} x, \text{ falls } x \neq x_i \text{ für alle } i\, , \\ t_i, \text{ falls } x = x_i \, . \end{cases}
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
}{Für eine Konstante $c$ ist
\mavergleichskettedisp
{\vergleichskette
{ c { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }
}
{ \defeq} {c
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{.}
}{Für ein $n$-stelliges Funktionssymbol $f$ und $n$ Terme
\mathl{s_1 , \ldots , s_n}{} ist
\mavergleichskettedisp
{\vergleichskette
{ fs_1 \ldots s_n { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }
}
{ \defeq} { f s_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 } }
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{.}
}
}
\inputbeispiel{}
{
Es seien
\mathl{c,d}{} Konstanten einer
\definitionsverweis {erststufigen Sprache}{}{,}
\mathl{x,y,z,v}{} Variablen, $p$ ein einstelliges und
\mathl{f,g,h}{} zweistellige Funktionssymbole. Wir betrachten den Term
\mathdisp {t= f px gcy} { }
und die Substitution
\mathdisp {{ \frac{ d, \, \, \, hvx , \, \, \, v }{ x, \, \, \,\, \, \, y, \, \, \, \,\, \, z } }} { . }
Die Substitution wird durchgeführt, indem man die kleinsten Bestandteile des Termes, also
\mathl{x,y,c}{,} ersetzt und ansonsten den funktionalen Aufbau des Termes übernimmt. Für diese gilt
\mavergleichskettedisp
{\vergleichskette
{ x { \frac{ d, \, \, \, hvx, \, \, \, v }{ x, \, \, \,\, \, \, y, \, \, \, \,\, \, z } }
}
{ =} { d
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{,}
\mavergleichskettedisp
{\vergleichskette
{ y { \frac{ d, \, \, \, hvx, \, \, \, v }{ x, \, \, \,\, \, \, y, \, \, \, \,\, \, z } }
}
{ =} { hvx
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
und
\mavergleichskettedisp
{\vergleichskette
{ c { \frac{ d ,\, \, \, hvx , \, \, \, v }{ x , \, \, \,\, \, \, y, \, \, \, \,\, \, z } }
}
{ =} { c
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{.}
Also ist
\mavergleichskettedisp
{\vergleichskette
{ fpxgcy { \frac{ d, \, \, \, hvx, \, \, \, v }{ x, \, \, \,\, \, \, y, \, \, \, \,\, \, z } }
}
{ =} { fpd g chvx
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{.}
Man beachte, dass das letzte $x$ nicht zu ersetzen ist.
}
\inputdefinition
{}
{
Es sei ein Symbolalphabet $S$ einer Sprache erster Stufe gegeben. Es seien
\mathl{x_1 , \ldots , x_k}{} paarweise verschiedene Variablen und
\mathl{t_1 , \ldots , t_k}{} fixierte
$S$-\definitionsverweis {Terme}{}{.}
Dann definiert man rekursiv über den Aufbau der
$S$-\definitionsverweis {Ausdrücke}{}{}
die
\definitionswort {Substitution}{}
\mathl{\alpha { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }}{} für jeden $S$-Ausdruck $\alpha$.
\aufzaehlungfuenf{Für Terme
\mathl{s_1,s_2}{} setzt man\zusatzfussnote {Die Klammern unterstreichen hier lediglich den Gesamtausdruck, für den die Substitution durchgeführt wird} {} {}
\mavergleichskettedisp
{\vergleichskette
{ (s_1 = s_2) { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }
}
{ \defeq} { 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 } }
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{.}
}{Für ein $n$-stelliges Relationssymbol $R$ und $n$ Terme
\mathl{s_1 , \ldots , s_n}{} setzt man
\mavergleichskettedisp
{\vergleichskette
{ (R s_1 \ldots s_n) { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }
}
{ \defeq} { R s_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 } }
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{.}
}{Für einen Ausdruck $\alpha$ setzt man
\mavergleichskettedisp
{\vergleichskette
{ (\neg \alpha) { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }
}
{ \defeq} { \neg \alpha { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{.}
}{Für Ausdrücke $\alpha$ und $\beta$ setzt man
\mavergleichskettedisp
{\vergleichskette
{ (\alpha \wedge \beta) { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }
}
{ \defeq} { \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.
}{Für einen Ausdruck $\alpha$ seien
\mathl{x_{i_1} , \ldots , x_{i_r}}{} diejenigen Variablen
\zusatzklammer {unter den \mathlk{x_1 , \ldots , x_k}{}} {} {,}
die in
\mathl{\forall x \alpha}{} frei vorkommen. Es sei
\mavergleichskette
{\vergleichskette
{v
}
{ = }{x
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
falls $x$ nicht in
\mathl{t_{i_1} , \ldots , t_{i_r}}{} vorkommt. Andernfalls sei $v$ die erste Variable
\zusatzklammer {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
\mathl{t_{i_1} , \ldots , t_{i_r}}{} vorkommt. Dann setzt man
\mavergleichskettedisp
{\vergleichskette
{ (\forall x \alpha ) { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }
}
{ \defeq} { \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.
}
}
\inputbeispiel{}
{
Es seien
\mathl{c,d}{} Konstanten einer
\definitionsverweis {erststufigen Sprache}{}{,}
\mathl{x,y,z,u}{} Variablen
\zusatzklammer {so geordnet} {} {,}
$f,g$ einstellige Funktionssymbole und $R$ ein zweistelliges Relationssymbol. Wir betrachten den Ausdruck
\mavergleichskettedisp
{\vergleichskette
{ \alpha
}
{ =} { \forall x \neg R y fx
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
und die Substitution
\mathdisp {{ \frac{ u,\, \, \, \, g c }{ 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
\mavergleichskettedisp
{\vergleichskette
{ { \left( \forall x \neg R y fx \right) } { \frac{ u, \, \, \, \, g c }{ x, \, \, \,\, \, \, y } }
}
{ =} { \forall x { \left( \neg R y f x { \frac{ g c }{ y } } \right) }
}
{ =} { \forall x \neg R gc f x
}
{ } {
}
{ } {
}
}
{}{}{.}
Bei der Substitution
\mathdisp {{ \frac{ u, \, \, \, \, g x }{ x , \, \, \, \, \, \, y } }} { }
kommt jetzt die gebundene Variable $x$ in dem substituierenden Term $gx$ vor. Es ist
\mavergleichskette
{\vergleichskette
{v
}
{ = }{z
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
die nächste Variable in der gegebenen Reihenfolge. Somit ist
\mavergleichskettedisp
{\vergleichskette
{ { \left( \forall x \neg R y fx \right) } { \frac{ u, \, \, \, \, g x }{ x , \, \, \, \, \, \, y } }
}
{ =} { \forall z { \left( \neg R y f x { \frac{ g x, \, \, \, \, z }{ y,\, \, \, \, \, \, x } } \right) }
}
{ =} { \forall z \neg R gx f z
}
{ } {
}
{ } {
}
}
{}{}{.}
}
Die folgende Aussage, das Substitutionslemma, stiftet eine Beziehung zwischen Substitutionen und Uminterpretationen.
In Verallgemeinerung der Schreibweise
\mathl{I { \frac{ m }{ x } }}{} für eine Uminterpretation schreiben wir
\mathl{I { \frac{ m_1 , \ldots , m_k }{ x_1 , \ldots , x_k } }}{} für die sukzessive Uminterpretation der untereinander verschiedenen Variablen
\mathl{x_1 , \ldots , x_k}{}
\zusatzklammer {dabei seien \mathlk{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.
\inputfaktbeweis
{Prädikatenlogik/Substitutionslemma/Fakt}
{Lemma}
{}
{
\faktsituation {Es sei ein Symbolalphabet $S$ einer Sprache erster Stufe gegeben und es seien
\mathl{x_1 , \ldots , x_k}{} paarweise verschiedene Variablen und
\mathl{t_1 , \ldots , t_k}{} fixierte
$S$-\definitionsverweis {Terme}{}{.}
Es sei eine
$S$-\definitionsverweis {Interpretation}{}{}
$I$ gegeben.}
\faktuebergang {Dann gelten folgende Aussagen.}
\faktfolgerung {\aufzaehlungzwei {Für jeden
$S$-\definitionsverweis {Term}{}{}
$s$ gilt
\mavergleichskettedisp
{\vergleichskette
{ 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)
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{.}
} {Für jeden
$S$-\definitionsverweis {Ausdruck}{}{}
$\alpha$ gilt
\mathdisp {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} { . }
}}
\faktzusatz {}
\faktzusatz {}
}
{
Dies wird über den induktiven Aufbau der Terme bzw. der Ausdrücke bewiesen. \teilbeweis {}{}{}
{(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
\mavergleichskettedisp
{\vergleichskette
{x
}
{ =} {x_i
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
mit einer der an der Substitution beteiligten Variablen ist, so ist
\mavergleichskettedisp
{\vergleichskette
{ 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
\mavergleichskettedisp
{\vergleichskette
{ 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
\mathl{s_1 , \ldots , s_n}{} Terme sind, für die die Gleichheit schon bekannt ist, so ist
\mavergleichskettealignhandlinks
{\vergleichskettealignhandlinks
{ I { \left( { \left( f s_1 \ldots s_n \right) } { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } } \right) }
}
{ =} { I { \left( f s_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) }
}
}
{
\vergleichskettefortsetzungalign
{ =} { { \left( I { \frac{ I(t_1) , \ldots , I(t_k) }{ x_1 , \ldots , x_k } } \right) } { \left( f s_1 \ldots s_n \right) }
}
{ } {}
{ } {}
{ } {}
}
{}{.}}
{}
\teilbeweis {}{}{}
{(2). Für einen Ausdruck der Form
\mavergleichskette
{\vergleichskette
{s
}
{ = }{t
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
bedeutet
\mathdisp {I \vDash { \left( s=t \right) } { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }} { }
einfach
\mathdisp {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
\mavergleichskettedisp
{\vergleichskette
{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
\mavergleichskettedisp
{\vergleichskette
{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
\mathdisp {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
\mathl{s_1 , \ldots , s_n}{} Terme. Die Gültigkeit
\mathdisp {I \vDash { \left( R s_1 \ldots s_n \right) } { \frac{ t_1 , \ldots , t_k }{ x_1 , \ldots , x_k } }} { }
bedeutet
\mathdisp {I \vDash R s_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
\mathdisp {{ \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
\mathl{I(R)}{} gehört. Nach dem ersten Teil ist dieses Tupel gleich
\mathdisp {{ \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
\mavergleichskette
{\vergleichskette
{R(I)
}
{ = }{R { \left( I { \frac{ I(t_1) , \ldots , I(t_k) }{ x_1 , \ldots , x_k } } \right) }
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
ist dies äquivalent zu
\mathdisp {I { \frac{ I(t_1) , \ldots , I(t_k) }{ x_1 , \ldots , x_k } } \vDash R s_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
\mathl{\forall x \alpha}{.} Die Gültigkeit
\mathdisp {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
\mathdisp {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
\mathl{t_{i_1} , \ldots , t_{i_r}}{} nicht vorkommt. Dies bedeutet, dass für jedes
\mavergleichskette
{\vergleichskette
{m
}
{ \in }{M
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
der Grundmenge der Interpretation die Beziehung
\mathdisp {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
\zusatzklammer {angewendet auf die Interpretation \mathlk{I \frac{m}{v}}{}} {} {}
bedeutet dies
\mathdisp {{ \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
\mavergleichskette
{\vergleichskette
{m
}
{ \in }{M
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Aufgrund
des Koinzidenzlemmas
ist dies äquivalent zu
\mathdisp {{ \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
\zusatzklammer {für alle
\mavergleichskettek
{\vergleichskettek
{m
}
{ \in }{M
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}} {} {}
zu
\mathdisp {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
\mavergleichskette
{\vergleichskette
{v
}
{ = }{x
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
klar ist und bei
\mavergleichskette
{\vergleichskette
{v
}
{ \neq }{x
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
aus dem Koinzidenzlemma
folgt, da dann $v$ nicht in $\alpha$ vorkommt. Dies bedeutet wiederum
\mathdisp {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
\mathl{x_{i_j}}{} verschiedenen Variablen in
\mathl{\forall x \alpha}{} nicht frei vorkommen,
\mathdisp {I { \frac{ I { \left( t_{1} \right) } , \ldots , I { \left( t_{k} \right) } }{ x_{1} , \ldots , x_{k} } } \vDash \forall x \alpha} { . }
}
{}