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
Some authors call this the Rule of Universal Elimination and it is then abbreviated UE.
Sources
- 2008: David Nelson: The Penguin Dictionary of Mathematics (4th ed.) ... (previous) ... (next): universal instantiation