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