# Prädikatenlogik/Substitutionslemma/Fakt/Beweis

Dies wird über den induktiven Aufbau der Terme bzw. der Ausdrücke 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}}$
(2). Für einen Ausdruck der Form $s=t$ bedeutet
    $I\vDash {\left(s=t\right)}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}$
einfach
    $I\vDash s{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}=t{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}.$
Dies ist äquivalent zu
    $I{\left(s{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}=I{\left(t{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\right)}\,,$
was nach dem ersten Teil einfach
    $I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}(s)=I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}(t)\,$
bedeutet. Dies wiederum ist äquivalent zu
    $I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\vDash s=t.$
Es sei nun $R$ ein $n$-stelliges Relationssymbol und seien $s_{1},\ldots ,s_{n}$ Terme. Die Gültigkeit
    $I\vDash {\left(Rs_{1}\ldots s_{n}\right)}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}$
bedeutet
    $I\vDash 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}}}$
und dies bedeutet, dass
    ${\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)}$
zur Relation $I(R)$ gehört. Nach dem ersten Teil ist dieses Tupel gleich
    ${\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}(s_{1}),\ldots ,I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}(s_{n})\right)}.$
Wegen $R(I)=R{\left(I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\right)}$ ist dies äquivalent zu
    $I{\frac {I(t_{1}),\ldots ,I(t_{k})}{x_{1},\ldots ,x_{k}}}\vDash Rs_{1}\ldots s_{n}.$
Für die weiteren Aussagen beweist man die Äquivalenz durch Induktion über den Aufbau der Ausdrücke, und zwar über alle Interpretationen simultan; dies ist für die aussagenlogischen Junktoren unmittelbar klar. Betrachten wir also einen Ausdruck der Form $\forall x\alpha$. Die Gültigkeit
    $I\vDash {\left(\forall x\alpha \right)}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}$
bedeutet gemäß der Festlegung in Definition, dass
    $I\vDash \forall v\alpha {\frac {t_{i_{1}},\ldots ,t_{i_{r}},v}{x_{i_{1}},\ldots ,x_{i_{r}},x}}$
gilt, wobei $v$ in $t_{i_{1}},\ldots ,t_{i_{r}}$ nicht vorkommt. Dies bedeutet, dass für jedes $m\in M$ der Grundmenge der Interpretation die Beziehung
    $I{\frac {m}{v}}\vDash \alpha {\frac {t_{i_{1}},\ldots ,t_{i_{r}},v}{x_{i_{1}},\ldots ,x_{i_{r}},x}}$
gilt. Nach Induktionsvoraussetzung (angewendet auf die Interpretation $I{\frac {m}{v}}$) bedeutet dies
    ${\left(I{\frac {m}{v}}\right)}{\frac {{\left(I{\frac {m}{v}}\right)}{\left(t_{i_{1}}\right)},\ldots ,{\left(I{\frac {m}{v}}\right)}{\left(t_{i_{r}}\right)},{\left(I{\frac {m}{v}}\right)}{\left(v\right)}}{x_{i_{1}},\ldots ,x_{i_{r}},x}}\vDash \alpha$
für alle $m\in M$. Aufgrund des Koinzidenzlemmas ist dies äquivalent zu
    ${\left(I{\frac {m}{v}}\right)}{\frac {I{\left(t_{i_{1}}\right)},\ldots ,I{\left(t_{i_{r}}\right)},m}{x_{i_{1}},\ldots ,x_{i_{r}},x}}\vDash \alpha .$
Dies ist äquivalent (für alle $m\in M$) zu
    $I{\frac {I{\left(t_{i_{1}}\right)},\ldots ,I{\left(t_{i_{r}}\right)},m}{x_{i_{1}},\ldots ,x_{i_{r}},x}}\vDash \alpha ,$
was bei $v=x$ klar ist und bei $v\neq x$ aus dem Koinzidenzlemma folgt, da dann $v$ nicht in $\alpha$ vorkommt. Dies bedeutet wiederum
    $I{\frac {I{\left(t_{i_{1}}\right)},\ldots ,I{\left(t_{i_{r}}\right)}}{x_{i_{1}},\ldots ,x_{i_{r}}}}\vDash \forall x\alpha$
und damit, wiederum nach dem Koinzidenzlemma, da die von $x_{i_{j}}$ verschiedenen Variablen in $\forall x\alpha$ nicht frei vorkommen,
    $I{\frac {I{\left(t_{1}\right)},\ldots ,I{\left(t_{k}\right)}}{x_{1},\ldots ,x_{k}}}\vDash \forall x\alpha .$