# Universal Generalisation

## Theorem

### Informal Statement

Let $\mathbf a$ be any arbitrarily selected object in the universe of discourse.

Then:

 $\ds \map P {\mathbf a}$  $\ds$ $\ds \vdash \ \$ $\ds \forall x: \,$ $\ds \map P x$  $\ds$
Suppose $P$ is true of any arbitrarily selected $\mathbf a$ in the universe of discourse.
Then $P$ is true of everything in the universe of discourse.

### Proof System

Let $\LL$ be a specific signature for the language of predicate logic.

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

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

Let $\FF$ be a collection of WFFs of $\LL$.

Let $c$ be an arbitrary constant symbol which is not in $\LL$.

Let $\LL'$ be the signature $\LL$ extended with the constant symbol $c$.

Suppose that we have the provable consequence (in $\LL'$):

$\FF \vdash_{\mathscr H} \map {\mathbf A} c$

Then we may infer (in $\LL$):

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