Are the quantifier negation rules in first-order logic derivable? 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?
 A: 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.

