Prädikatenlogik/Alleinführung im Sukzedens/Regel/Axiom
Erscheinungsbild
Es sei ein Symbolalphabet erster Stufe, und seien -Ausdrücke, und seien Variablen. Dann gilt unter der Bedingung, dass weder in noch in frei vorkommt die folgende Regel: Aus
folgt