# Existential Instantiation

## Theorem

### Informal Statement

- $\exists x: \map P x, \map P {\mathbf a} \implies y \vdash y$

Suppose we have the following:

- From our universe of discourse,
*any*arbitrarily selected object $\mathbf a$ which has the property $P$ implies a conclusion $y$ - $\mathbf a$ is not free in $y$
- It is known that there
*does*actually exists an object that has $P$.

Then we may infer $y$.

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

When using this rule of existential instantiation:

- $\exists x: \map P x, \map P {\mathbf a} \implies y \vdash y$

the instance of $\map P {\mathbf a}$ is referred to as the **typical disjunct**.

### Existential Instantiation in Proof Systems

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, \mathbf B$ be WFFs 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, \map {\mathbf A} c \vdash_{\mathscr H} \mathbf B$

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

- $\FF, \exists x: \map {\mathbf A} x \vdash_{\mathscr H} \mathbf B$

## Also known as

Some authors call this the **Rule of Existential Elimination** and it is then abbreviated $\text {EE}$.