- Freie Variablen
In einem Ausdruck
über einem Symbolalphabet
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.
-
![{\displaystyle {}\operatorname {Frei} \,(t_{1}=t_{2})=\operatorname {Var} \,(t_{1})\cup \operatorname {Var} \,(t_{2})\,.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/356a758f6de777e363f3170f1c7175ef4de165fd)
-
![{\displaystyle {}\operatorname {Frei} \,(Rt_{1}\ldots t_{n})=\operatorname {Var} \,(t_{1})\cup \operatorname {Var} \,(t_{2})\cup \ldots \cup \operatorname {Var} \,(t_{n})\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/33bd432693824ebf4189f9959f26301c2959065c)
für ein
-stelliges Relationssymbol
und
Terme
.
-
![{\displaystyle {}\operatorname {Frei} \,(\neg \alpha )=\operatorname {Frei} \,(\alpha )\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2614f7f390e366e14cabcf25aacc917e89ef1579)
für einen Ausdruck
.
-
![{\displaystyle {}\operatorname {Frei} \,(\alpha \rightarrow \beta )=\operatorname {Frei} \,(\alpha )\cup \operatorname {Frei} \,(\beta )\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/697689828e25283c79af088dbb2edbe12b1c719b)
für Ausdrücke
und
. Ebenso für
.
-
![{\displaystyle {}\operatorname {Frei} \,(\forall x\alpha )=\operatorname {Frei} \,(\alpha )\setminus \{x\}\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/11a5ee577a767c6c9688c319c5640a62639539ad)
für einen Ausdruck
und eine Variable
.
-
![{\displaystyle {}\operatorname {Frei} \,(\exists x\alpha )=\operatorname {Frei} \,(\alpha )\setminus \{x\}\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3b5b3f626c58623dee56269de272a858876af387)
für einen Ausdruck
und eine Variable
.
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
bezeichnet, die Menge der Ausdrücke mit genau einer freien Variablen
(die aber in dem Ausdruck beliebig oft vorkommen darf)
mit
.
Beispielsweise ist in
-
die Variable
gebunden, während die Variablen
frei sind, wobei die Freiheit von
auf dem freien Vorkommen im hinteren Ausdruck beruht.
- 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
-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.
(1). Wir führen Induktion über den Aufbau der
-Terme. Für den Induktionsanfang müssen wir Variablen und Konstanten aus
betrachten. Für eine Variable
(oder eine Konstante)
aus
ist nach Voraussetzung
.
Im Induktionsschritt können wir annehmen, dass ein
-stelliges Funktionssymbol
aus
gegeben ist sowie
-Terme
, für die die Interpretationsgleichheit schon gezeigt wurde. Nach Voraussetzung wird
in beiden Interpretationen durch die gleiche Funktion
interpretiert. Daher ist
![{\displaystyle {}{\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5209eee7eae6607d7c921d69b9e98f63f1f2b4db)
(2). Wir führen Induktion über den Aufbau der
-Ausdrücke, wobei die zu beweisende Aussage über je zwei Interpretationen zu verstehen ist. Für die Gleichheit und ein Relationssymbol
aus
folgt die Aussage unmittelbar aus (1), da ja
in beiden Interpretationen als die gleiche Relation zu interpretieren ist. Der Induktionsschritt ist für Ausdrücke der Form
aufgrund der Modellbeziehung unmittelbar klar. Es sei nun ein
-Ausdruck der Form
gegeben, und es gelte
. Dies bedeutet aufgrund der Modellbeziehung, dass es ein
derart gibt, dass
gilt. Die beiden umbelegten Interpretationen
und
stimmen auf den Symbolen aus
und den in
frei vorkommenden Variablen überein: Die Variable
wird so oder so als
interpretiert und die anderen freien Variablen aus
sind auch in
frei. Nach Induktionsvoraussetzung gilt
und daher wiederum
.
![{\displaystyle \Box }](https://wikimedia.org/api/rest_v1/media/math/render/svg/029b77f09ebeaf7528fc831fe57848be51f2240b)
- Substitution
Wir besprechen nun die Variablensubstitution, wobei wir weitgehend der Darstellung von Ebbinghaus, Flum, Thomas folgen.
Variablen repräsentieren verschiedene Werte
(in einer Grundmenge
),
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
-
bedeutet in einem angeordneten Körper interpretiert, dass die nichtnegative Zahl
als Quadrat darstellbar ist (also eine Quadratwurzel besitzt), was für
wahr ist, für
im Allgemeinen (das hängt von der Interpretation für
ab) nicht. Gleichbedeutend (bei einer inhaltlichen Interpretation) mit diesem Ausdruck ist
-
aber nicht
-
das nur bei
oder
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
zugrunde, oder aber eine beliebig große Variablenmenge, die mit einer Wohlordnung versehen sei.
Es sei ein Symbolalphabet
einer
Sprache erster Stufe
gegeben. Es seien
paarweise verschiedene Variablen und
fixierte
-
Terme.
Dann definiert man rekursiv über den Aufbau der Terme die Substitution
für jeden
-Term
.
- Für eine Variable
ist
-
![{\displaystyle {}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}}\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b5a0ab8e6336a6a22933ff22e7bc1e6373fa2069)
- Für eine Konstante
ist
-
![{\displaystyle {}c{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:=c\,.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f0da523f18d737821b66ea7197cfde3b758a8885)
- Für ein
-stelliges Funktionssymbol
und
Terme
ist
-
![{\displaystyle {}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}}}\,.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/05a8a6d846a74900a184d6fa4383262d6d8bd6bf)
Es sei ein Symbolalphabet
einer Sprache erster Stufe gegeben. Es seien
paarweise verschiedene Variablen und
fixierte
-
Terme.
Dann definiert man rekursiv über den Aufbau der
-
Ausdrücke
die
Substitution
für jeden
-Ausdruck
.
- Für Terme
setzt man[1]
-
![{\displaystyle {}(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}}}\,.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/009863d408348f36edd23cd5e947bd2cdb14ffd7)
- Für ein
-stelliges Relationssymbol
und
Terme
setzt man
-
![{\displaystyle {}(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}}}\,.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a9941983fee0acba3ca32ed4a049c7a557f832d0)
- Für einen Ausdruck
setzt man
-
![{\displaystyle {}(\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}}}\,.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/61fc4c7f687a356ca5707d89dabb22686a896d81)
- Für Ausdrücke
und
setzt man
-
![{\displaystyle {}(\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}}}\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0810efea11a6733899d32168d19721cad27f55ee)
und ebenso für die anderen zweistelligen Junktoren.
- Für einen Ausdruck
seien
diejenigen Variablen
(unter den
),
die in
frei vorkommen. Es sei
,
falls
nicht in
vorkommt. Andernfalls sei
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
noch in
vorkommt. Dann setzt man
-
![{\displaystyle {}(\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}}\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cbac9e7baad12fbeb0e8b181b7614896e73ae4a8)
und ebenso für den Existenzquantor.
Die folgende Aussage, das Substitutionslemma, stiftet eine Beziehung zwischen Substitutionen und Uminterpretationen.
In Verallgemeinerung der Schreibweise
für eine Uminterpretation schreiben wir
für die sukzessive Uminterpretation der untereinander verschiedenen Variablen
(dabei seien
Elemente der Grundmenge
der Interpretation).
Es werden also die
als
interpretiert und alle anderen Variablen werden gemäß
interpretiert.
Es sei ein Symbolalphabet
einer Sprache erster Stufe gegeben und es seien
paarweise verschiedene Variablen und
fixierte
-
Terme.
Es sei eine
-
Interpretation
gegeben. Dann gelten folgende Aussagen.
- Für jeden
-
Term
gilt
-
![{\displaystyle {}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)\,.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6af422342abe8fe9dc9c48be6a05c50702d3418f)
- Für jeden
-
Ausdruck
gilt
-
Dies wird über den induktiven Aufbau der Terme bzw. der Ausdrücke bewiesen. (1). Für eine Konstante
ist die Aussage richtig, da ihre Interpretation unverändert ist. Für eine Variable
macht man eine Fallunterscheidung. Wenn
-
![{\displaystyle {}x=x_{i}\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f27a93dcd7644d471dfd62eede871874ec836f52)
mit einer der an der Substitution beteiligten Variablen ist, so ist
-
![{\displaystyle {}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})\,.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/22dcc7dfe943c2bb2e59cdfbaefcf470d03fbc10)
Bei einer an der Substitution nicht beteiligten Variablen
ist
-
![{\displaystyle {}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)\,.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c67b42339d387e636a569b12a0c27bef28525134)
Wenn
ein
-stelliges Funktionssymbol ist und
Terme sind, für die die Gleichheit schon bekannt ist, so ist
![{\displaystyle {}{\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/de0c6247b02f6bc076c3fb89adb6873bed99cc24)
(2). Für einen Ausdruck der Form
bedeutet
-
einfach
-
Dies ist äquivalent zu
-
![{\displaystyle {}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)}\,,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/60d3fbc9215361ecabdf3940895a0859fba5d78b)
was nach dem ersten Teil einfach
-
![{\displaystyle {}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)\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/28fee2dab30ebe67c9f5790864eec00f1736514e)
bedeutet. Dies wiederum ist äquivalent zu
-
Es sei nun
ein
-stelliges Relationssymbol und seien
Terme. Die Gültigkeit
-
bedeutet
-
und dies bedeutet, dass
-
zur Relation
gehört. Nach dem ersten Teil ist dieses Tupel gleich
-
Wegen
ist dies äquivalent zu
-
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
. Die Gültigkeit
-
bedeutet gemäß der Festlegung in
Definition 9.4,
dass
-
gilt, wobei
in
nicht vorkommt. Dies bedeutet, dass für jedes
der Grundmenge der Interpretation die Beziehung
-
gilt. Nach Induktionsvoraussetzung
(angewendet auf die Interpretation
)
bedeutet dies
-
für alle
.
Aufgrund
des Koinzidenzlemmas
ist dies äquivalent zu
-
Dies ist äquivalent
(für alle
)
zu
-
was bei
klar ist und bei
aus dem Koinzidenzlemma
folgt, da dann
nicht in
vorkommt. Dies bedeutet wiederum
-
und damit, wiederum nach dem Koinzidenzlemma, da die von
verschiedenen Variablen in
nicht frei vorkommen,
-
![{\displaystyle \Box }](https://wikimedia.org/api/rest_v1/media/math/render/svg/029b77f09ebeaf7528fc831fe57848be51f2240b)
- Fußnoten
- ↑ Die Klammern unterstreichen hier lediglich den Gesamtausdruck, für den die Substitution durchgeführt wird