# Universal Instantiation

## Theorem

### Informal Statement

Suppose we have a universal statement:

$\forall x: \map P x$

where $\forall$ is the universal quantifier and $\map P x$ is a propositional function.

Then we can deduce:

$\map P {\mathbf a}$

where $\mathbf a$ is any arbitrary object we care to choose in the universe of discourse.

Suppose $P$ is true of everything in the universe of discourse.
Let $\mathbf a$ be an element of the universe of discourse."
Then $P$ is true of $\mathbf a$.

### Universal Instantiation in Models

Let $\map {\mathbf A} x$ be a WFF of predicate logic.

Let $\tau$ be a term which is freely substitutable for $x$ in $\mathbf A$.

Then $\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau$ is a tautology.

### Universal Instantiation in Proof Systems

Let $\map {\mathbf A} x$ be a WFF of predicate logic.

Let $\tau$ be a term which is freely substitutable for $x$ in $\mathbf A$.

Let $\mathscr H$ be Hilbert proof system instance 1 for predicate logic.

Then:

$\forall x: \map {\mathbf A} x \vdash_{\mathscr H} \map {\mathbf A} \tau$

is a provable consequence in $\mathscr H$.

## Also known as

The Rule of Universal Instantiation can be abbreviated UI.

The Rule of Universal Instantiation can also be referred to as the Rule of Universal Elimination and it is then abbreviated UE.

The reasoning behind the name Universal Elimination is that it is used to "eliminate" the universal quantifier from a logical argument.