Prädikatenlogik/Existenzeinführung im Antezedens/Regel/Axiom

Existenzeinführung im Antezedens

Es sei ${}S$ ein Symbolalphabet erster Stufe, ${}\alpha$ und ${}\beta$ seien ${}S$-Ausdrücke, ${}x$ und ${}y$ seien Variablen. Dann gilt die folgende Regel: Wenn

$\vdash \alpha {\frac {y}{x}}\rightarrow \beta$

gilt und wenn ${}y$ weder in ${}\exists x\alpha$ noch in ${}\beta$ frei vorkommt, so gilt auch

$\vdash \exists x\alpha \rightarrow \beta .$