Name of rule for negating quantifiers

Question

A lot of rules of logic have accepted names:

• $\neg (P\lor Q)\iff(\neg P)\land(\neg Q)$ and $\neg(P\land Q)\iff(\neg P)\lor(\neg Q)$ are called "De Morgan's rules" (or "laws").
• $(P\lor Q)\land R\iff(P\land Q)\lor(P\land R)$ is called "distributivity."
• $(P\to Q)\iff(\neg Q\to\neg P)$ is called "transposition" or "replace with the contrapositive."

But what about the rules for manipulating quantifiers?

• $\neg(\forall x:P(x))\iff\exists x:\neg P(x)$
• $\neg(\exists x:P(x))\iff\forall x:\neg P(x)$

Do these rules have accepted names in English?

In Negating statements with quantifiers, @Bram28 calls it the "dagger rule," but a quick Google search didn't turn up any great textual support for this name.

In Why negating universal quantifier gives existential quantifier? it's opined that it's appropriate to call this rule an axiom of formal logic, but what I want to know is, "What axiom is it?" :)

In A proof of $(\forall x P(x)) \to A) \Rightarrow \exists x (P(x) \to A)$ the questioner uses it in a formal proof under the name of "A Known Identity," which is just beautiful. :)

I'm looking for a name so I can use it in a blog post, where I would first introduce the rule and say "This is called the Rule of Foo," and then farther down, I would say "Now we apply the Rule of Foo to transform this statement into..."

Answer 1

The operators $\forall$ and $\exists$ are so-called duals of each other, which for logic means that each is equivalent to the negation of the other applied to the negated subformula: $Q \phi \iff \neg Q^\delta \neg \phi$. The equivalence is hence commonly called "duality (of quantifiers)".
Note that the same duality property applies to the pair of connectives $\land, \lor$: $\ \phi C \psi \iff \neg(\neg \phi C^\delta \neg \psi)$; so sometimes these rules are also subsumed under "de Morgan's laws (for quantifiers)".