Existential Generalisation
Theorem
This is an extension of the Rule of Addition as follows:
- $P \left({\mathbf a}\right) \vdash \exists x: P \left({x}\right)$
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 EG.
Proof
The propositional expansion of $\exists x: P \left({x}\right)$ is:
- $P \left({\mathbf X_1}\right) \lor P \left({\mathbf X_2}\right) \lor P \left({\mathbf X_3}\right) \lor \ldots$
We have the fact that $P \left({\mathbf a}\right)$ where $\mathbf a$ is one of the above $\mathbf X_1, \mathbf X_2, \mathbf X_3, \ldots$, as it is by definition.
So the above statement $P \left({\mathbf X_1}\right) \lor P \left({\mathbf X_2}\right) \lor P \left({\mathbf X_3}\right) \lor \ldots$ follows by extension of the rule of addition.
$\blacksquare$
Notes
Some authors call this the Rule of Existential Introduction and it is then abbreviated EI.
However, beware the fact that other authors use EI to abbreviate the Rule of Existential Instantiation which is the antithesis of this one.
So make sure you know exactly what terminology is specified.