Working with negation of quantifiers

Question

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

Answer 1

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)