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

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

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

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

${}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 ${}x$ ist

${}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 ${}f$ ein ${}n$-stelliges Funktionssymbol ist und ${}s_{1},\ldots ,s_{n}$ Terme sind, für die die Gleichheit schon bekannt ist, so ist

${}{\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}}$

Zur gelösten Aufgabe