Prädikatenlogik/Substitutionslemma/Fakt/Beweis

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 .$

Zur bewiesenen Aussage