Is $\lnot\forall x\;\lnot\forall y\;A$ the same as $\forall x\;\forall y\;A$? And if so, by what rule? I am trying to find a rule where the above would apply.
I am currently using Hilbert deduction system for a prove and I need to show that: $$\forall x\;\forall y\;A \implies \forall y\;\forall x\;A$$ But I am currently stuck at: $$\lnot\forall x\;\lnot\forall y\;A \implies \forall y\;\forall x\;A$$
As per previous comments, $¬∀x¬∀y A$ and $∀y∀x A$ are not equivalent; but you do not need it in order to prove that : $∀x∀y A → ∀y∀x A$.
1) $∀x∀y A$ --- assumed
2) $∀yA$ --- from 1) and quantifier axiom : $∀xα → α^x_t$, with $x$ as $t$, by modus ponens
3) $A$ --- from 2) and quantifier axiom again, by modus ponens
4) $∀xA$ --- from 3) by Generalization Theorem : If $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash ∀x \varphi$, where $x$ is not free in $\Gamma = \{ ∀x∀y A \}$
5) $∀y∀xA$ --- from 4) by Gen Th : $y$ is not free in $∀x∀yA$
In the same way for $∀y∀x A \rightarrow ∀x∀yA$.
We can easily "translate" the above proof into Natural Deduction, with two applications of $\forall$-elimination followed by two applications of $\forall$-introduction.