Prädikatenlogik/Variablensubstitution/Ausdrücke/Definition

Variablensubstitution für Ausdrücke

Es sei ein Symbolalphabet $S$ einer Sprache erster Stufe gegeben. Es seien $x_1,\dots ,x_k$ paarweise verschiedene Variablen und $t_1,\dots ,t_k$ fixierte $S$-Terme. Dann definiert man rekursiv über den Aufbau der $S$-Ausdrücke die Substitution $\alpha \frac{t_1,\dots ,t_k}{x_1,\dots ,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,\dots ,t_k}{x_1,\dots ,x_k}:=s_1\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}=s_2\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}.$

2. Für ein $n$-stelliges Relationssymbol $R$ und $n$ Terme $s_1,\dots ,s_n$ setzt man

   $(R{s}_1\dots s_n)\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}:=R{s}_1\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}\dots s_n\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}.$

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

   $(\mathrm{\neg }\alpha )\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}:=\mathrm{\neg }\alpha \frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}.$

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

   $(\alpha \wedge \beta )\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}:=\alpha \frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}\wedge \beta \frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}$

   und ebenso für die anderen zweistelligen Junktoren.

5. Für einen Ausdruck $\alpha$ seien $x_{i_1},\dots ,x_{i_r}$ diejenigen Variablen (unter den $x_1,\dots ,x_k$), die in $\mathrm{\forall }x\alpha$ frei vorkommen. Es sei  $v=x$,  falls $x$ nicht in $t_{i_1},\dots ,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},\dots ,t_{i_r}$ vorkommt. Dann setzt man

   $(\mathrm{\forall }x\alpha )\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}:=\mathrm{\forall }v\alpha \frac{t_{i_1},\dots ,t_{i_r},v}{x_{i_1},\dots ,x_{i_r},x}$

   und ebenso für den Existenzquantor.