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

Question

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?

Answer 1

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'

Answer 2

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.

Answer 3

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!