Prove by Hilbert deduction: $\vdash _{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$ I'd really like your help proving:
$\vdash_{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$
Where $HFOL$ is the proof system which contains the Hilbert relevant axioms:


*

*$A\rightarrow(B \rightarrow A)$

*$(A\rightarrow(B\rightarrow C))\to((A\rightarrow B)\rightarrow(A\rightarrow C))$

*$(A\rightarrow B)\rightarrow ((A\rightarrow\bar{B})\rightarrow \bar{A})$

*$\bar{\bar{A}} \rightarrow A$


Plus the following two axioms:
$\forall x(B\to A)\to (\exists xB \to A)$
$\forall x(A \to B) \to (A \to \forall x B)$
Restricted to use only while $x$ is not a free variable in $A$.
And other two axioms: $\forall xA \to A \{ t/x \}$, $A\{t/x\} \to \exists xA$ where $t$ is free for assignment instead of $x$ in $A$.
Finally theres the $MP$ rule: From $A, A\to B$ we conclude $B$ and the Gen rule which from $A$ we conclude $\forall xA$.
I tried couple of different ways but didn't come with any smart result.
Any suggestions?

Well, you can use the deduction theorem because ∀x(¬(A→¬B)) has no free variables.
After using it you get: ∀x(¬(A→¬B))⊢HFOL¬(∀xA→¬(∀xB))
Now we will build a proof in HFOL:


*

*∀x(¬(A→¬B)) - by assumption.

*∀x(¬(A→¬B))→¬(A→¬B) - first axiom.

*¬(A→¬B) - MP on 1,2.

*¬(A→¬B)→A - because you can prove it on hpc.

*A - MP on 3,4.

*∀xA - Gen on 5.

*¬(A→¬B)→B - because you can prove it on hpc.

*B - MP on 3,7.

*∀xB - Gen on 8.

*¬(∀xA→¬(∀xB)) - because you can prove it on hpc.

