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