Prädikatenlogik/Substitution/Ohne Beweis/Einführung/Textabschnitt

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. 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 eine durchnummerierte (und abzählbare) Variablenmenge ${}v_{1},v_{2},v_{3}\ldots$ zugrunde.

Definition

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}}}\,.$

Definition

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.

Die folgende Aussage, das Substitutionslemma, geben wir ohne Beweis. Es stiftet eine Beziehung zwischen Substitutionen und Uminterpretationen.

Lemma

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 .$