Prädikatenlogik/Substitutionslemma/Fakt/Beweis/Aufgabe/Lösung

Dies wird über den induktiven Aufbau der Terme bewiesen. (1). Für eine Konstante ${\displaystyle {}c}$ ist die Aussage richtig, da ihre Interpretation unverändert ist. Für eine Variable ${\displaystyle {}x}$ macht man eine Fallunterscheidung. Wenn

${\displaystyle {}x=x_{i}\,}$

mit einer der an der Substitution beteiligten Variablen ist, so ist

${\displaystyle {}I{\left(x_{i}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}=I(t_{i})={\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}(x_{i})\,.}$

Bei einer an der Substitution nicht beteiligten Variablen ${\displaystyle {}x}$ ist

${\displaystyle {}I{\left(x{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}=I(x)={\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}(x)\,.}$

Wenn ${\displaystyle {}f}$ ein ${\displaystyle {}n}$-stelliges Funktionssymbol ist und ${\displaystyle {}s_{1},\ldots ,s_{n}}$ Terme sind, für die die Gleichheit schon bekannt ist, so ist

${\displaystyle {}{\begin{aligned}I{\left({\left(fs_{1}\ldots s_{n}\right)}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}&=I{\left(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}}}\right)}\\&=I(f){\left(I{\left(s_{1}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)},\ldots ,I{\left(s_{n}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}\right)}\\&=I(f){\left({\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}(s_{1}),\ldots ,{\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}(s_{n})\right)}\\&={\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}(f){\left({\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}{\left(s_{1}\right)},\ldots ,{\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}{\left(s_{n}\right)}\right)}\\&={\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}{\left(fs_{1}\ldots s_{n}\right)}.\end{aligned}}}$