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.

In natural language:

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.

Sources

• 1998: David Nelson: The Penguin Dictionary of Mathematics (2nd ed.) ... (previous) ... (next): logic
• 2008: David Nelson: The Penguin Dictionary of Mathematics (4th ed.) ... (previous) ... (next): logic
• 2008: David Nelson: The Penguin Dictionary of Mathematics (4th ed.) ... (previous) ... (next): universal instantiation