Prädikatenlogik/Variablensubstitution/Terme/Definition

Variablensubstitution für Terme

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