Prädikatenlogik/Existenzeinführung im Sukzedens/Axiom

Existenzeinführung im Sukzedens

Es sei $S$ ein Symbolalphabet erster Stufe, $\alpha$ ein $S$-Ausdruck, $x$ eine Variable und $t$ ein $S$-Term. Dann ist

$⊢\alpha \frac{t}{x}\to \mathrm{\exists }x\alpha .$