Prädikatenlogik/Ableitbar/Allquantor/Fakt/Beweis

Beweis

Nach der Allquantorversion von Axiom ist

$\vdash \forall x\alpha \rightarrow \alpha {\frac {x}{x}},$

also

$\vdash \forall x\alpha \rightarrow \alpha .$

Daher folgt aus

$\vdash \forall x\alpha$

mittels Modus ponens direkt

$\vdash \alpha .$

Es sei umgekehrt ${}\vdash \alpha$ gegeben. Es sei ${}\beta$ ein beliebiger Ausdruck, in dem ${}x$ nicht vorkomme. Nach Axiom  (1) und Modus ponens ergibt sich

$\vdash \beta \rightarrow \alpha$

und

$\vdash \neg \beta \rightarrow \alpha .$

Auf diese beiden abgeleiteten Ausdrücke wird nun die Allquantorversion der Existenzeinführung im Antezedens (also die Alleinführung im Sukzedens) angewendet. Dies ist möglich, da ${}x$ in ${}\beta$ überhaupt nicht und in ${}\forall x\alpha$ nicht frei vorkommt. Man erhält

$\vdash \beta \rightarrow \forall x\alpha$

und

$\vdash \neg \beta \rightarrow \forall x\alpha .$

Daraus ergibt sich mit der Fallunterscheidungsregel

$\vdash \forall x\alpha .$

Zur bewiesenen Aussage