# 31.4 EElim

The only formal proof rule for quantifiers we haven’t covered is EElim.

It works just like the informal method Existential Instantiation (EI), by allowing us to talk about the object we know exists from an existential claim.

Say we know ∃xP(x). Then we need to start a subproof by assuming an arbitrary name n: @n.

But we don’t leave the rest of the subproof assumption blank. We don’t want to talk about a totally arbitrary member of the domain.

We want to talk about the object we know exists with property P.

We want to talk about the object we know exists with property P.

(Of course, there could be several such objects. We just need to talk arbitrarily about any one of them.)

Then, if we can prove some random sentence R, which does not have the name “n” in it, we can export R out of the subproof with EElim.

When we do so, we must cite the existential sentence that we are eliminating, plus the subproof that we created.

Let’s see an example.

Notice that line 3 starts a subproof assuming an arbitrary n, @n, but then it also has P(n). That is how we assume we are talking about an arbitrary object with property P.

When we write “@n P(n)” there is exactly one space between the @n part and the P(n) part.

You might think that violates the rule of having no spaces in sentences of FOL, but it doesn’t.

“@n P(n)” does two things at once, which is why they are separated by a space.

“@n P(n)” is not a sentence of FOL. It does two things at once, which is why they are separated by a space: it assumes an arbitrary name, @n, and it assumes that n has property P, P(n).

If you are ever wondering what to include in the sentence part, like “P(n),” you just need to look at the existential sentence that you are using for EElim.

When you cite EElim, you cite the existential line you are eliminating, as well as the subproof.

It is sort of like proof by cases, vElim, where we first needed to cite the disjunction we were eliminating, and then all the subproofs.

Now you try it.

On the last line we cite the existential we are eliminating, and then the subproof in which we talk about that @n with P(n)&Q(n,a).

With EElim we export the last line, just like in vElim.

Also notice that the sentence on line 7 is identical to line 8. With EElim we export the last line, just like in vElim.

The use of arbitrary names here is similar, but not exactly like, arbitrary names in AIntro (Universal Generalization).

The arbitrary name cannot appear anywhere outside the subproof. Since the last line of the subproof gets exported, that means that the arbitrary “n” cannot appear in the last line.

But the assumption line for EElim is different from an assumption line for AIntro. For EElim, there will always be a formula we know about @n, given by the existential sentence we are using for the elimination.