Existential Elimination (EE) allows us to reason from an existentially quantified sentence to an instance of the scope of the quantified sentence. Once this is done, we can manipulate the instance and derive conclusions that would not be possible with the quantified sentence as a whole.
The main problem in eliminating an existential quantifier is choosing an expression to replace the existential variable. Should we replace it with a variable? How about an object constant? Unfortuately, neither of these solutions works.
We cannot use a variable since the resulting instance would be equivalent to a universally quantified sentence (given our convention that our free variables are universally quantified). For example, given the sentence ∃x.p(x), we cannot infer p(x) since that would say that p is true of everything.
And we cannot replace the quantified variable with an object constant. Although we know the sentence is true of some object, we do not know which it is. For example, given a language with just two object constants a and b and given the sentence ∃x.p(x), we cannot infer p(a) since we do not know whether or not p is true of a and we cannot infer p(b) since we do not know whether or not p is true of b.
The solution to this problem is to replace the variable in an existentially quantified sentence with a new type of expression, called a Skolem term. A Skolem term is effectively a placeholder for an actual object constant and is treated like an ordinary term by our rules of inference (except for Domain Closure, as described in Section 8.4). For example, in the case above, given the sentence ∃x.p(x), we would infer p([c]), where c is a new constant (one that is not part of our language) and where the square brackets are used to make clear that [c] is a Skolem term rather than an ordinary object constant.
Using the idea of Skolem terms, we can formulate a rule of inference for eliminating existential quantifiers. There are two cases to consider - the case where the quantified sentence is closed and the case where the quantified sentence contains one or more free variables.
Existential Elimination for closed sentences. Suppose we have a closed existentially quantified sentence with variable ν and scope φ[ν]. Then, we can infer an instance of φ in which ν is replaced by a new constant τ. In what follows, we refer to τ as a Skolem constant.
where τ is a not an existing object constant
For example, if we have the sentence ∃x.hates(jane,x), then we can conclude ¬hates(jane,[c]), provided that c is not an existing object constant. This sentence tells us that Jane hates someone; we just do not know who that someone is. If we have the sentence ∃x.hates(x,x), then we can conclude ¬hates([c],[c]), provided that c is not an existing object constant. This sentence tells us that someone hates himself; we just do not know who that someone is.
Unfortunately, things get a little more difficult when the existentially quantified sentence contains free variables. Suppose, for example, we had the sentence ∃y.hates(x,y). Given this sentence, we know that everyone hates someone, but it is possible that different people hate different people. If we were to replace the existential variable with a simple Skolem term [c] we would get the conclusion hates(x,[c]), this would say that there is a single person that everyone hates, which is not the same as the original meaning.
Fortunately, we can solve this problem through the use of more complex Skolem terms that include not just a new constant but also include free variables in the Skolem term.
Existential Elimination for sentences with free variables. Suppose we have an existentially quantified sentence with quantified variable ν and scope φ[ν1,...,νn,ν] where ν1, ..., νn are free variables. Then, we can infer an instance of φ in which ν is replaced by a new term [π(ν1,...,νn)], where π is a new constant. In what follows, we refer to π as a Skolem function.
where π is a not an existing constant
For example, if we have the sentence ∃y.hates(x,y), then we can conclude ∃y.hates(x,[f(x)]). This sentence tells us that everyone hates someone but it allows for the possibility that the hated person is different in each case.
In what follows, we combine these two cases into a single rule, called Existential Elimination, with the understanding that the first case applies in the case of closed existentially quantified sentences and the second applies in the case of existentially quantified sentences with free variables.
By comparison to Existential Elimination, Existential Introduction (EI) is easy. If we believe a sentence involving a term τ, then we can infer an existentially quantified sentence in which one, some, or all occurrences of τ have been replaced by the existentially quantified variable provided that τ does not contain any explicitly quantified variables.
where τ does not contain any universally quantified variables
For example, from the sentence hates(jill,jill), we can infer that there is someone who hates herself, i.e. ∃x.hates(x,x). We can also infer that there is someone Jill hates, i.e. ∃x.hates(jill,x), and there is someone who hates Jill, i.e. ∃y.hates(x,jill). And, by two applications of Existential Introduction, we can infer that someone hates someone, i.e. ∃x.∃y.hates(x,y).
Note that, in Existential Introduction, it is important to avoid variables that appear in the sentence being quantified. Without this restriction, starting from ∃x.hates(jane,x), we might deduce ∃x.∃x.hates(x,x). It is an odd sentence since it contains nested quantifiers of the same variable. However, it is a legal sentence, and it states that there is someone who hates himself, which does not follow from the premise in this case.
Note also that the rule applies only in cases where the term being replaced does not contain any universally quantified variables. This restriction is necessary to avoid incorrect conclusions. Suppose, for example, we had the sentence ∀x.hates(x,[f(x)). If we were to use EI in this case, we would get the conclusion ∃y.∀x.hates(x,y). The original sentence says that everyone hates someone but not necessarily the same person whereas this false conclusion states that there is a single person that everyone hates.