Are the quantifier negation rules in first-order logic derivable?

Question

Question: Is is possible to derive $\ \vdash \sim\forall xP(x) \leftrightarrow\exists x \sim P(x) \ $ (or any other version of the quantifier negation rule) axiomatically?

Context: I tutor college students in various subjects including symbolic logic. I recently acquired a new student who is using a text that I am unfamiliar with. This text is accompanied by a program called Logic 2010, so by way of preparation, I downloaded the software and began playing with it.

One of the exercises is the above derivation. However, I keep hitting an impasse when attempting it: I can't manage to derive the relationship unless I assume $\sim\exists x\sim P(x)\vdash \forall xP(x)$. Pretty much any logical rule or identity is fair game other than internal substitutions of logical equivalences.

These identities have always been presented to me as intuitively obvious, so now, I am beginning to think that it is not possible to derive them - that they must be axiomatic.

Are the quantifier negation rules axiomatic or derivable?

Answer 1

In Natural Deduction we can prove the "usual" relationships between quantifiers starting from the basic rules.

E.g.

1) $\forall x Px$ --- premise

2) $\exists x \lnot Px$ --- assumed [a]

3) $\lnot Py$ --- assumed [b] from 4) for $\exists$-elim

4) $Py$ --- from 1) by $\forall$-elim (Universal Instantiation)

5) $\bot$ --- contradiction: from 3) and 4)

6) $\bot$ --- from 2), 3) and 4) by $\exists$-elim, discharging [b]

7) $\lnot \exists x \lnot Px$ --- from 2) and 6) by $\to$-intro, dicharging [a]

8) $\forall x Px \vdash \lnot \exists x \lnot Px$ --- from 1) and 7).

---

1) $\lnot \exists x \lnot Px$ --- premise

2) $\lnot Py$ --- assumed [a]

3) $\exists x \lnot Px$ --- from 2) by $\exists$-intro

4) $\bot$ --- contradicition: from 1) and 3)

5) $\lnot \lnot Py$ --- from 2) and 4) by $\to$-intro, discharging [a]

6) $Py$ --- from 5) by Double Negation (it holds only classically)

7) $\forall x Px$ --- from 6) by $\forall$-intro

8) $\lnot \exists x \lnot Px \vdash \forall x Px$ --- from 1) and 7).

As you can see, some of the "usual" equivalences (see also; $¬∀x¬ Px \to ∃xPx$) hold only in classical logic, because their proof needs Double Negation; see Intuitionistic Logic.

For more details, see e.g.:

• Jan von Plato, Elements of Logical Reasoning, Cambridge UP (2013), Part II Logical reasoning with the quantifiers.

For a different approach you can see:

• Elliott Mendelson, Introduction to Mathematical Logic, CRC Press (6th ed 2015), where $\forall$ is primitive and the existential quantifier is defined in terms of it.