CS 245 — Lecture 17

Existential quantifier elimination

For $\exists$e, we can think back to how $\vee$e worked. To apply $\vee$e on a formula $(\varphi \vee \psi)$, we needed to recognize that we did not know which of $\varphi$ or $\psi$ we had a proof for, so we needed to proceed assuming each in its own subproof. If we were able to arrive at the same conclusion $\eta$, then we could conclude that $\eta$ could be proved from $(\varphi \vee \psi)$.

We are faced with the same challenge with $\exists$e. A forumla $(\exists x \alpha)$ says that there is some element of the domain for which $\alpha$ holds, but we don't know which one. Just like with $\forall$i, we have a seemingly impossible task, searching for a suitable $x$ from a possibly infinite set of values. Luckily, the same sort of idea that we used to resolve $\forall$i can be used for $\exists$e. Let's look at the rule $\exists$e.

Definition 17.1. $$\frac{\begin{matrix} \quad \\ \quad \\ (\exists x \alpha) \end{matrix} \quad \boxed{\begin{matrix} \alpha[u/x], \text{$u$ fresh} \\ \vdots \\ \beta \end{matrix}}}{\beta} \exists e$$

Again, let's think about how we'd prove that there's some natural number that satisfies some property we want to prove. We would say something like, suppose $n$ is a natural number that has this property, and then proceed. In essence, we are making the assumption that one of the values that we need holds and we give it a name. We then proceed with the proof and arrive at a conclusion. That is what this rule encapsulates: we assume that there exists an element that satisfies $\alpha$ and we call this element some name $u$ that hasn't been used before. Again, this all takes place within a subproof and the same subproof rules apply.

Example 17.2. We will show $\{(\exists x P(x))\} \vdash (\exists y P(y))$.

Here, $(\exists x P(x))$ says that there is some value out there that $P(x)$ holds. Since we know this value exists, we will arbitrarily name it $u$, which we have not used before. So, assuming that this value called $u$ is such that $P(u)$ holds, we can conclude that there exists some value for which $P(y)$ holds and therefore $(\exists y P(y))$.

Example 17.3. We will show $\{(\forall x(P(x) \vee Q(x))), (\exists x(\neg P(x)))\} \vdash (\exists x Q(x))$.

Example 17.4. Now, to finish off the equivalence from earlier, we will show that $\{(\forall x (S(x) \rightarrow (\neg L(x,c))))\} \vdash (\neg (\exists x (S(x) \wedge L(x,c))))$.

Some more examples

Example 17.5. $\{(\forall x (Q(x) \rightarrow R(x))), (\exists x (P(x) \wedge Q(x)))\} \vdash (\exists x (P(x) \wedge R(x)))$.

Example 17.6. Here, we'll try to prove something where we need to consider more than one variable. We will show $\{(\exists x P(x)), (\forall x (\forall y (P(x) \rightarrow Q(y))))\} \vdash (\forall y Q(y))$.

Example 17.7. Here is an example of a De Morgan's law that is generalized to quantifiers. We will show $\{(\neg (\forall x P(x)))\} \vdash (\exists x (\neg P(x)))$.

Example 17.8. Recall our discussion from propositional logic about the classical and intuitionist interpretations of proofs. We can have the same discussion in the context of first-order logic, but we won't get into it. Instead, we'll have a look at an example of a statement that is valid in the classical interpretation of predicate logic, but is not provable in the intuitionistic interpretation of predicate logic. The statement is as follows:

In any bar, there is a person such that if he or she drinks, then everyone drinks.

So if $P$ is the unary predicate symbol defined by $P(x)$ is "$x$ drinks", then the Drinker Paradox is $(\exists x (P(x) \rightarrow (\forall y P(y))))$. We will show $\emptyset \vdash (\exists x (P(x) \rightarrow (\forall y P(y))))$.