# Working with negation of quantifiers

How would you prove $\exists x\neg P(x)$ given $\neg \forall xP(x)$ using first-order logic?

-
What is primitive logic? – Git Gud Mar 20 '13 at 20:29
It depends on exactly how those terms are defined for you. Often $\exists x Q(x)$ is defined to be $\neg\forall x \neg Q(x)$. Conversely $\forall$ could be defined in terms of $\exists$. You get equivalent logics in the end but for a proof like this you really need to use the specific details of how your terms are defined. – Jim Mar 20 '13 at 20:36

As was quite rightly pointed out above, it depends a bit on how you define your quantifiers in the first place. However, I can give you a proof of your theorem that uses only the introduction/elimination rules for the existential and universal quantifier (plus contradiction and other "basic" logic rules) would be the following:

Goal: $[\neg\forall x.\,P(x)] \Longrightarrow \exists x.\,\neg P(x)$

We prove the contraposition of this, which is:

Goal: $[\neg\exists x.\,\neg P(x)] \Longrightarrow \forall x.\,P(x)$

We apply the introduction rule of the forall quantifier, meaning we now have to show that for an arbitrary, but fixed $x$, the following holds:

Goal: $[\neg\exists x.\,\neg P(x)] \Longrightarrow P(x)$

We show this by contradiction, leaving the following goal

Goal: $[\neg P(x)\ \wedge\ \neg\exists x.\,\neg P(x)] \Longrightarrow \textrm{False}$

We use the introduction rule for the existential quantifier, which says that since $P(x)$ holds for some $x$, $\exists x.\,P(x)$ also holds:

Goal: $[\exists x.\,\neg P(x)\ \wedge\ \neg\exists x.\,\neg P(x)] \Longrightarrow \textrm{False}$

Now we apply the elimination rule for the negation, which states that for any statement $P$, we have $[P\ \wedge\ \neg P] \Longrightarrow \textrm{False}$, and we are done.

Proofs like this can be done quite nicely in interactive theorem provers. To prove that the above proof is logically sound, here is the corresponding proof in Isabelle:

lemma "$(\neg(\forall x.\ P\ x)) \Longrightarrow (\exists x.\ \neg P\ x)$"
apply (erule contrapos_np)
apply (intro allI)
apply (rule ccontr)
apply (drule exI[of "$\lambda x.\ \neg P\ x$"])
apply (erule (1) notE)
done

(Of course, the theorem prover can do this automatically as well, since it is a trivial statement, but this illustrates how it is done step-by-step)

-
thank you so much! very helpful – Henry Mar 21 '13 at 14:32