Existenzeinführung im Antezedens/Alleinführung im Sukzedens/Aufgabe

Beweise aus der Existenzeinführung im Antezedens die Alleinführung im Sukzedens. Sie besagt, dass man aus

$⊢\beta \to \alpha \frac{y}{x}$

unter der Bedingung, dass $y$ weder in $\mathrm{\forall }x\alpha$ noch in $\beta$ frei vorkommt, auf

$⊢\beta \to \mathrm{\forall }x\alpha$

schließen kann.

Eine Lösung erstellen