# Double negation of existential/universal quantifier $\lnot(\exists x(\lnot A(x))$

I have a (simple) question about the double-negation and existential/universal quantifiers.

When negating the following

$$\lnot\exists x(\lnot A(x))$$

I believe you just push the negation in (which swaps the quantifier) making it

$$\forall x[\lnot(\lnot A(x))]$$

and then

$$\forall x A(x)$$

Would that be a correct interpretation? Or would I be losing one of the negations on $$A(x)$$ somewhere earlier?

• Yes, that’s fine. It’s also intuitively clear: the first expression says that there is no $x$ for which $A(x)$ is false, and the last says that $A(x)$ is true for every $x$, clearly the same thing. Apr 22 '20 at 17:30
• Awesome, thank you so much. Apr 22 '20 at 17:31
• You’re very welcome. Apr 22 '20 at 17:31
• Thank you (just read your more detailed answer) - I thought the intuition was clear, but it was part of a larger proof and I was doubting myself as to whether the reduction made sense. I guess I just needed validation. Apr 22 '20 at 17:35

You did that correctly.

Note that going from

$$\lnot\exists x(\lnot A(x))$$

to

$$\forall x[\lnot(\lnot A(x))]$$

is an example of 'Quantifier Negation', but going from:

$$\forall x[\lnot(\lnot A(x))]$$

to

$$\forall x A(x)$$

is an instance of 'Double Negation'

As per the answer by Brian M. Scott:

It’s also intuitively clear: the first expression says that there is no x for which A(x) is false, and the last says that A(x) is true for every x, clearly the same thing.

A word of caution. Of course at the final step $$\forall x\neg\neg Ax$$ entails (or at least, classically entails) $$\forall x Ax$$, and does so because adjacent double negations (classically) cancel each other out.

BUT

The inference is not strictly an application of a standard double negation rule of the form from $$\neg\neg\varphi$$ infer $$\varphi$$. That rule only allows us to remove initial double negations.

SO

To show the entailment in standard proof systems requires a three-step mini-proof:

$$\forall x\neg\neg Ax\quad$$ (given)

$$\neg\neg Aa\quad\quad$$ (universal instantiation with parameter or free variable depending on system)

$$Aa\quad\quad\quad$$ (NOW you can apply the DN rule)

$$\forall x Ax\quad\quad$$ (universal generalization)

So your reasoning is informally just fine, but do be careful about jumping from $$\forall x\neg\neg Ax$$ to $$\forall x Ax$$ in formal proofs!