Prädikatenlogik/Quantoren/Tautologie/Existenzvertauschung/Fakt/Beweis/Aufgabe/Lösung

Durch Existenzeinführung im Sukzedenz haben wir

$\vdash \alpha \rightarrow \exists x\alpha$

und

$\vdash \exists x\alpha \rightarrow \exists y\exists x\alpha$

und daraus

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

Dabei ist ${}y$ hinten gebunden und somit kann man mit der Existenzeinführung im Antezedens auf

$\vdash \exists y\alpha \rightarrow \exists y\exists x\alpha$

schließen. Da auch ${}x$ hinten gebunden ist, ergibt sich

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

Zur gelösten Aufgabe