Existential Generalisation

From ProofWiki
Jump to navigation Jump to search

Theorem

Informal Statement

$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.


Existential Generalisation in Models

Let $\mathbf A \left({x}\right)$ be a WFF of predicate logic.

Let $\tau$ be a term which is freely substitutable for $x$ in $\mathbf A$.


Then $\mathbf A \left({\tau}\right) \implies \exists x: \mathbf A \left({x}\right)$ is a tautology.


Also known as

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.