Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question
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

1 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)

(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)

share|improve this answer
thank you so much! very helpful –  Henry Mar 21 '13 at 14:32

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.