Universelle Quantifikation (Beweisregeln)

Im System des Natürlichen Schließens wendet man für die universelle Quantifikation ( $\forall$ ) diese beiden Regeln an:

Eliminationsregel ( $\forall E$ ):

\frac{\forall x . φ}{φ [\frac{t}{x}]} unter der Bedingung O K (t, x, φ)

Die Regel besagt: Ist eine Formel allgemeingültig für alle $x$ , so behält sie ihre Gültigkeit auch für jede zulässige Term-Ersetzung $t$ .

Einführungsregel ( $\forall I$ ):

\frac{{x_{0}} ⟹ φ [\frac{x_{0}}{x}]}{\forall x . φ} mit x_{0} als frischer Variable

Lässt sich die Aussage für eine beliebig angenommene, abstrakte Variable $x_{0}$ beweisen, so ist die Formel für alle $x$ gültig.