Given this expression $\lnot \exists B. \forall n. P$ I just came across the assertion that the negation of said assertion was $\exists B. \lnot \forall n. P$. Then I realized that actually I did not know how to negate a whole proposition at once that has nested quantifiers. I first tried applying the negation from the left

\begin{align} & \lnot [\lnot \exists B. \forall n. P]\\ \iff & \exists B. \forall n. P\\ \end{align}

Well, that apparently was incorrect. Then I tried inverting all quantified propositions, but not the bare propositions (in this case P).

\begin{align} & \lnot [\lnot \exists B. \forall n. P]\\ \iff & \exists B. \lnot \forall n. P \end{align}

This result is the right one, but was the way I did it correct? I know how unquantified propositions are negated based on an intuition. That "not A or not B" or "at most one of A and B" or "either A or B" ($\lnot A \lor \lnot B$) is the negation of "both of A and B" ($A \land B$) makes intuitive sense. I do not have this intuition about quantified expressions however, and I can not claim that it makes intuitive sense to me that $\exists B. \lnot \forall n. P$ is in fact the negation of $\lnot \exists B. \forall n. P$. As a matter of fact, intuitively $\exists B. \forall n. P$ would make more sense to me as the negation of $\lnot \exists B. \forall n. P$.


"There is no snail that eats every salad"


"Yes, there is a snail (at least one) that eats every salad"

Which structurally would correspond to $\lnot \exists B. \forall n. P$ and $\exists B. \forall n. P$ respectively.

So, does this rule of negating all quantified expressions inside a expression that is to be negated follow from something or is it like an axiom? If it follows from other axioms, can you derive it and maybe also argue why it makes intuitive sense?

  • $\begingroup$ You have to "move inside" the negation sign following the rules: $\lnot \exists$ is $\forall \lnot$ and $\lnot \forall$ is $\exists \lnot$. $\endgroup$ Aug 1, 2017 at 19:04
  • $\begingroup$ You must not be mislead by natural language: the negation of "there is (at least) one cat" is "there are no cats". This does not mean that $\lnot \exists$ is the same as $\exists \lnot$. $\endgroup$ Aug 1, 2017 at 19:59

3 Answers 3


The negation of $\varphi$ is $\lnot \varphi$, for every formula $\varphi$.

Thus, regarding your example, the negation of $∃x \ ∀n \ P$ is of course $\lnot ∃x \ ∀n \ P$.

1) We have to "move inside" the negation sign step-by-step following the rules: $¬∃$ is $∀¬$ and $¬∀$ is $∃¬$.

Thus, for $¬∃x \ ∀n \ P$ is equivalent to: $∀x \ ¬∀n \ P$ which in turn is equivalent to: $∀x \ ∃n \ ¬P$.

2) About $¬[¬∃x \ ∀n \ P]$, we have simply to apply double negation to get: $∃x \ ∀n \ P$.

About "intuition", if "there are no $P$" (i.e. $¬∃xPx$) then we must have that "all (objects) are not-$P$" (i.e. $∀x¬Px$).

Assuming for simplicity that "not-black" is "white", we have that if "there are no black cats", then we must have that "all cats are white".

  • $\begingroup$ So, you are saying that $\lnot [\lnot \exists B. \forall n P]$ is not equivalent to $ \exists B. \lnot \forall n P$ afteral, but rather $\exists B. \forall n P$. But then I don't understand why in the source that caused this confusion for me it says otherwise. Unfortunately it is not in English. But the part $\lnot \exists B. \forall n P$ is at the root of the green arrow and the part as the tip of the arrow is $\exists B. \lnot \forall n P]$. "Es gibt" is $\exists$, "Es gibt keinen" is $\lnot \exists$. The arrow here means "assuming completeness" youtube.com/watch?v=BN0rF5lv4Nc $\endgroup$ Aug 1, 2017 at 19:44
  • $\begingroup$ @user3578468 - of course, $¬[¬∃B.∀nP]$ is equivalent to $∃B.∀nP$. Again, in general, $\lnot \lnot \varphi$is equiv to $\varphi$, fior very formula $\varphi$. $\endgroup$ Aug 1, 2017 at 19:48
  • $\begingroup$ @user3578468 - $\exists x$ reads "there exists" while $\lnot \exists x$ reads "does not exists". For $\exists x \lnot$ we have instead the meaning: "there is (there exists) something that does not...". To assert that there is something that is not a cat [i.e. $\exists x \ \lnot \text{Cat}(x)$ ] does not mean that there are no cats at all [i.e. $\lnot \exists x \ \text{Cat}(x)$ ]. $\endgroup$ Aug 2, 2017 at 6:37

The assertion is wrong (or maybe you misunderstood what they tried to do ...)

The negation of $\lnot \exists B. \forall n. P$ is of course just $ \exists B. \forall n. P$, and not $ \exists B. \lnot \forall n. P$

In general, we have:

Quantifier Negation

Where $\varphi$ is any formula:

$\neg \exists x \varphi \Leftrightarrow \forall x \neg \varphi$

$\neg \forall x \varphi \Leftrightarrow \exists x \neg \varphi$

...which makes intuitive sense:

There isn't something with property $\varphi$, if and only if everything lacks the property $\varphi$.

And, not everything has property $\varphi$, if and only if there is something that lacks property $\varphi$

You can also make sense of these equivalences like this:

An existential can be seen as kind of disjunction, that is, if $a,b,c,...$ denote the objects in your domain, then you can think of an existential like this:

$\exists x \: \varphi(x) \approx \varphi(a) \lor \varphi(b) \lor \varphi(c) \lor ...$

Likewise, a universal is a kind of conjunction:

$\forall x \: \varphi(x) \approx \varphi(a) \land \varphi(b) \land \varphi(c) \land ...$


$$\neg \exists x \: \varphi(x) \approx $$

$$\neg (\varphi(a) \lor \varphi(b) \lor \varphi(c) \lor ...) \Leftrightarrow \text{ (DeMorgan)}$$

$$\neg \varphi(a) \land \neg \varphi(b) \land \neg \varphi(c) \land ...) \approx$$

$$\forall x \neg \varphi$$


$$\neg \forall x \: \varphi(x) \approx $$

$$\neg (\varphi(a) \land \varphi(b) \land \varphi(c) \land ...) \Leftrightarrow \text{ (DeMorgan)}$$

$$\neg \varphi(a) \lor \neg \varphi(b) \lor \neg \varphi(c) \lor ...) \approx$$

$$\exists x \neg \varphi$$ (... which is why these equivalences are also known as the 'DeMorgan's Laws for quantifiers)


The negation of $\bbox[lemonchiffon,0.5ex]{\neg \exists B\,\forall n\,P}$ is definitely $\bbox[lemonchiffon,0.5ex]{\exists B\, \forall n\,P}$.   (Well, unless your logic system disallows double negation.)

The negation of $\bbox[lemonchiffon,0.5ex]{\exists B\, \forall n\,P}$ is $\bbox[lemonchiffon,0.5ex]{\forall B\,\exists n\, \neg P}$.

Also $\bbox[lemonchiffon,0.5ex]{\neg \exists B\,\forall n\,P}$ and $\bbox[lemonchiffon,0.5ex]{\forall B\,\exists n\, \neg P}$ are equivalent.   Which is obtained through the property of quantifier duality. That is that $\bbox[lemonchiffon,0.5ex]{\neg\forall x\,\varphi\iff \exists x\,\neg\varphi}$ and $\bbox[lemonchiffon,0.5ex]{\neg\exists x\,\varphi\iff \forall x\,\neg\varphi}$.

$${\neg \exists B\, \forall n\, P \\\Updownarrow\\\forall B\,\neg\forall n\, P \\\Updownarrow\\\forall B\,\exists n\,\neg P}\qquad{\text{There is no snail that eats every salad}\\\Updownarrow\\\text{Every snail does not eat every salad}\\\Updownarrow\\\text{Every snail has some salad that it will not eat}} $$


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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