0
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Brian M. Scott Apr 22 at 17:30
  • $\begingroup$ Awesome, thank you so much. $\endgroup$ – confundido Apr 22 at 17:31
  • $\begingroup$ You’re very welcome. $\endgroup$ – Brian M. Scott Apr 22 at 17:31
  • $\begingroup$ 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. $\endgroup$ – confundido Apr 22 at 17:35
2
$\begingroup$

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'

| cite | improve this answer | |
$\endgroup$
0
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
0
$\begingroup$

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!

| cite | improve this answer | |
$\endgroup$

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.