2 of 2

33.2 Existentials Are Harder

In the previous section we considered the main ideas when your premise or conclusion is a universal quantifier.

In this section we do the same thing for an existential quantifier.

Existential Premise

Existential premise: start EElim.
Existential conclusion: wait! Look around for other ideas. You’ll use EIntro at some point.

When your premise is a wide-scope existential quantifier, you start an EElim proof.

EElim is one of the complicated proof rules. Let’s say your premise is ExP(x). You have to start a subproof and assume an arbitrary name with @n P(n).

Even though EElim is complicated, there is something nice about an existential premise: EElim is always the way to use it.

For example, in the proof below the premise is ExP(x). So on line 2 we need to assume “n” is an arbitrary object from the domain with property P: @n P(n).

Remember, there is a space between the “@n” part and the “P(n)” part, because we are doing two separate things. We assume “n” is an arbitrary name, and we also assume it has property P.

Remember, rules about premises apply any time you have an existential as a premise, temporary assumption, or intermediary conclusion that you’ve already proven.

For example, in the next proof the premise is a disjunction. But once you start proof by cases, you’ll have some wide-scope existentials to work with. So you’ll need EElim.

Existential Conclusion

As you might have guessed, when the conclusion is an existential, we will need EIntro.

But don’t presume that we will always do EIntro on the final line.

Usually we won’t do EIntro on the last line. That means that an existential conclusion is less informative than an existential premise. It doesn’t tell us what to do right away.

For example, in both of the proofs that we just did, the conclusion was existential as well as the premise. But we didn’t even focus on the fact that the conclusion is existential when we were figuring out what to do.

The existential premise was the more important thing to notice.

A common occurrence is that EIntro is used within an EElim subproof.

A common occurrence is that EIntro is used within an EElim subproof. Remember how EElim works: the arbitrary name “n” cannot appear outside the subproof.

One easy way to get rid of a name is to existentially generalize with EIntro.

So it makes sense why EIntro often occurs inside an EElim subproof.

For example, consider this version of null quantification. The conclusion is existential, but that doesn’t tell us where we’ll use EIntro.

What we need to notice to make progress is that the premise is conjunction. Once we bring down the conjuncts, we get an existential sentence that we can do EElim with.

Pay attention to the subproofs to see the order we did all the steps in!