Existentielle Quantifikation (Beweisregeln)

Die Handhabung der existentiellen Quantifikation ( $\exists$ ) erfolgt im Natürlichen Schließen über zwei Regeln:

Einführungsregel ( $\exists I$ ):

\frac{φ [\frac{t}{x}]}{\exists x . φ} mit t \in T_{σ} und O K (t, x, φ)

Es reicht aus, einen konkreten und gültigen "Zeugen" $t$ vorzuweisen, um die Existenz zu belegen.

Eliminationsregel ( $\exists E$ ):

\frac{\exists x . φ {x_{0}, φ [\frac{x_{0}}{x}]} \overset{!}{⟹} ψ}{ψ}

Ist die bloße Existenz bekannt, wird abstrakt ein Zeuge $x_{0}$ angenommen. Kann man mit dessen Hilfe das gewünschte Beweisziel $ψ$ herleiten, so gilt $ψ$ .