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 \)

In natural language:

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$

Sources

This page may be the result of a refactoring operation. As such, the following source works, along with any process flow, will need to be reviewed. When this has been completed, the citation of that source work (if it is appropriate that it stay on this page) is to be placed above this message, into the usual chronological ordering. In particular: regarding informal statement If you have access to any of these works, then you are invited to review this list, and make any necessary corrections. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{SourceReview}} from the code.

• 1980: D.J. O'Connor and Betty Powell: Elementary Logic ... (previous) ... (next): $\S \text{IV}$: The Logic of Predicates $(2): \ 2$: Universal Instantiation