Substitutionslemma
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
-