Prädikatenlogik/Ableitbar/Allquantor/Fakt/Beweis

Beweis

Nach der Allquantorversion von Axiom ist

also

Daher folgt aus

mittels Modus ponens direkt


Es sei umgekehrt gegeben. Es sei ein beliebiger Ausdruck, in dem nicht vorkomme. Nach Axiom  (1) und Modus ponens ergibt sich

und

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 in überhaupt nicht und in nicht frei vorkommt. Man erhält

und

Daraus ergibt sich mit der Fallunterscheidungsregel