1. Introduction

Existential Elimination (EE) is arguably the most complicated rule of inference in the Fitch system. It is difficult for many to understand, and it is not easy to use in generating proofs. This article describes the rule, offers some intuition for why the rule is defined as it is, and offers some tips for using the rule to prove results from existential premises.

2. Existential Elimination

Suppose we have an existentially quantified sentence with scope φ; and suppose we have a universally quantified implication in which the antecedent is the same as the scope of our existentially quantified sentence and suppose that the conclusion does not contain any occurrences of the quantified variable. Then, we can use Existential Elimination to infer the consequent.

For example, if we have the sentence ∃x.p(a,x) and we have the sentence ∀x.(p(a,x) ⇒ q(a)), then we can apply existential elimination to conclude q(a)).

Note that the condition that ν does not occur free in ψ is essential. Consider the following erroneous line of reasoning to see what goes wrong without this condition.

If p is true of an object, then q is also true of that object. We know that p is true of at least one object. And somehow we have shown that q is true of everything, which does not follow from the given premises.

3. Intuition 1

In order to understand why existential elimination works, assume we know ∃x.p(x) and we also know ∀x.(p(x) ⇒ q(c)). The distribution theorem for universal quantifiers tells us that the second sentence is logically equivalent to ∃x.p(x) ⇒ q(c). Given a sentence that matches the first premise of EE, e.g. ∃x.p(x), we can use Implication Elimination to conclude q(c), which is exactly what EE allows us to do.

This intuition raises the question of why EE needs to be so complicated. Why not use the version with an existential in the antecedent? The reason is not easy to explain. Suffice it to say that there are things that are logically entailed that cannot be proved without the version of EE with the universal quantifier wrapped around the entire implication.

4. Intuition 2

An existential sentence is effectively a disjunction. To see this, consider a language with just four object constants a, b, c, d (or equivalently a world with just four objects). Now suppose we learn that there is some object that satisfies the p relation, i.e. ∃x.p(x). Then we know that p must be true of at least one of a, b, c, or dd, i.e. p(a) ∨ p(b) ∨ p(c) ∨ p(d).

Now, recall that, in Or Elimination, we start with a disjunction with n disjuncts and n implications, one for each of the disjuncts and produce as conclusion the consequent shared by all of the implications. An existential sentence (like the first premise in any instance of Existential Elimination) is effectively a disjunction over the set of all ground terms; and a universal implication (like the second premise in any instance of Existential Elimination) is effectively a set of implications, one for each ground term in the language. The conclusion of Existential Elimination is the common consequent of these implications, just as in Or Elimination.

5. Existential Reasoning

Reasoning with existential statements is difficult, and confusion about EE only complicates matters. However, such reasoning can be simplified by thinking about existential reasoning in the right way. The basic idea is illustrated in the following examples.

Suppose we are given the statement ∃x.(p(x) ∧ q(x)) and we are asked to prove the statement ∃x.q(x). We begin our proof with the given premise.

We know there is an object that satisfies both p and q. In order to make progress, let's use a placeholder, e.g. c, to talk about this object, and let us assume that c satisfies the scope of the existential.

At this point, we use and elimination to split the conjunction.

Now, we use existential introduction to derive the sentence we are trying to prove.

That looks good, but our conclusion is embedded in a subproof. We have shown that ∃x.q(x) is true under the assumption that p(c) ∧ q(c) is true. To finish the proof, we need to get the conclusion out of the subproof. Fortunately, this is easy to do, but it takes a few steps.

First, we use Implication Introduction to exit the subproof.

Next, we get rid of our placeholder using Universal Introduction.

Finally, we use existential elimination to get our desired conclusion.

The key to this proof is the subproof. Given an existential statement, we start by assuming the scope of true for some placeholder and we prove our result. Having done this, we use Implication Introduction (II), Universal Introduction (UI), and Existential Elimination (EE) to get the conclusion out of the subproof.

As another example, consider the proof shown below. Here, we have as premises a universal implication ∀x.(p(x) ⇒ q(x)) and an existential statement ∃x.¬q(x), and our goal is to prove ∃x.¬p(x).

The technique here is the same as in the previous example. We start by choosing a fresh placeholder c to replace our existential variable, and we assume that the scope of the existential holds of c. Our goal is to prove ¬p(c), and we can do this using Negation Introduction. We assume p(c), reiterate ¬q(c), and use Implication Introduction to get p(c) ⇒ ¬q(c). We then instantiate our universal premise to get p(c) ⇒ q(c). And we use Negation Introduction to derive ¬p(c) and Existential Introduction to derive ∃x.¬p(x). Finally, we use II, UI, and EE to get this conclusion out of the subproof.

As one final example, consider the slightly more complicated proof shown below. In this case, we have the premise ∃y.∀x.p(x,y), and our job is to prove ∀x.∃y.p(x,y)). The proof is shorter than the last, but more complicated because we need two placeholders.

Existential Elimination is a difficult rule to use. Unfortunately, it is often the only way we can derive conclusions from existential statements. However, as these example illustrate, doing existential proofs is simplified by using the technique described here. Given an existential premise, we name the object that exists, we assume scope of the existential, we prove our result, and we extract our result from the subproof, using II, UI, and EE.