Prädikatenlogik/Existenzeinführung im Antezedens/Korrektheit/Fakt/Beweis

Beweis

Es sei ${}\alpha {\frac {y}{x}}\rightarrow \beta$ allgemeingültig, d.h.

$I\vDash \alpha {\frac {y}{x}}\rightarrow \beta$

für jede ${}S$-Interpretation ${}I$. Wir müssen zeigen, dass dann auch ${}\exists x\alpha \rightarrow \beta$ allgemeingültig ist (unter den gegebenen Voraussetzungen). Es sei dazu ${}I$ eine Interpretation mit

$I\vDash \exists x\alpha .$

Aufgrund der Modellbeziehung bedeutet dies, dass es ein ${}m\in M$ (aus der Grundmenge der Interpretation) mit

$I{\frac {m}{x}}\vDash \alpha$

gibt. Die Variable ${}y$ kommt nach Voraussetzung in ${}\exists x\alpha$ nicht frei vor, d.h. bei ${}y\neq x$, dass ${}y$ in ${}\alpha$ nicht frei vorkommt. Wir können daher das Koinzidenzlemma anwenden und erhalten

${\left(I{\frac {m}{x}}\right)}{\frac {m}{y}}\vDash \alpha .$

Diese Aussage gilt trivialerweise auch bei ${}x=y$. Damit gilt auch

${\left(I{\frac {m}{y}}\right)}{\frac {m}{x}}\vDash \alpha .$

Wir schreiben dies (etwas künstlich) als

${\left(I{\frac {m}{y}}\right)}{\frac {{\left(I{\frac {m}{y}}\right)}(y)}{x}}\vDash \alpha .$

Darauf können wir das Substitutionslemma (für die Interpretation ${}J=I{\frac {m}{y}}$ und den Term ${}y$) anwenden und erhalten

$I{\frac {m}{y}}\vDash \alpha {\frac {y}{x}}.$

Wegen der vorausgesetzten Allgemeingültigkeit von ${}\alpha {\frac {y}{x}}\rightarrow \beta$ folgt

$I{\frac {m}{y}}\vDash \beta .$

Da ${}y$ in ${}\beta$ nicht frei vorkommt, liefert das Koinzidenzlemma

$I\vDash \beta .$

Zur bewiesenen Aussage