Existential Generalisation/Informal Statement

Theorem

$\map P {\mathbf a} \vdash \exists x: \map P x$

Suppose we have the following:

We can find an arbitrary object $\mathbf a$ in our universe of discourse which has the property $P$.

Then we may infer that:

there exists in that universe at least one object $x$ which has that property $P$.

This is called the Rule of Existential Generalisation and often appears in a proof with its abbreviation $\text {EG}$.

Sources

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