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?
 A: 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.

A: Jozef, forgive the clumsiness of my notation, since I'm not used to HFOL,I enjoyed the challenge.
I also provided a second proof in Dijsktra's Style, since I found it an useful aid to my intuition, since you mentioned that you tried many things without luck. It may prove useful.

Proof in HFOL:
$\forall x(\neg (A\rightarrow  \neg B))\vdash\neg (\forall xA\rightarrow \neg \forall xB)$
Knowing $(A\rightarrow B)\rightarrow ((A\rightarrow \neg B)\rightarrow \neg A)$, we could try:
$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB\vdash \neg (A\rightarrow \neg B), (A\rightarrow \neg B)$
I picked  $\neg (A\rightarrow \neg B), (A\rightarrow \neg B)$ because we can get $\neg (A\rightarrow \neg B)$ it easily.
We get $\neg (A\rightarrow \neg B)$ from $\forall x(\neg (A\rightarrow \neg B))$
and $ \forall xA\rightarrow A{t/x}$.
Now for the tricky part. $A\rightarrow \neg B$
$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB\vdash A\rightarrow \neg B$
Knowing the MP rule we could try:
$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB,A\vdash \neg B$
We get $\forall xA$ from $A$ and the Gen rule.
We get $\neg \forall xB$ from $\forall xA$, $\forall xA\rightarrow \neg \forall xB$ and the MP rule.
We get $\neg B$ from $\neg \forall xB$ and $\forall xA\rightarrow A\lbrace{ t/x\rbrace}$.
Done.

Now in Dijkstra's Style.
$\forall x(\neg (A \rightarrow  \neg B))\rightarrow \neg (\forall xA \rightarrow  \neg \forall xB)$
$=\lbrace p\rightarrow q = \neg p\vee q \rbrace$
$\forall x(\neg (\neg A \vee \neg B)) \rightarrow  \neg (\neg \forall xA \vee \neg \forall xB)$
$=\lbrace de Morgan\rbrace$
$\forall x(A \wedge B)\rightarrow (\forall xA \wedge \forall xB)$
$=\lbrace Distributivity\,\, of \,\, \forall\,\, over\,\, \wedge \rbrace$
$(\forall xA \wedge \forall xB)\rightarrow (\forall xA \wedge \forall xB)$
Done.
Edit: To clarify why I found the second proof useful for aiding my intuition. As you can see this proof is considerately shorter. This is because the style allows more general laws (instead of a minimal set of axioms) and because it prefers rules that avoid case analysis. This means that it is far easier to prove something in this style.
Now, to me, the hardest step in my first proof was:
$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB\vdash \neg (A\rightarrow \neg B), (A\rightarrow \neg B)$
I knew I had to apply $(A\rightarrow B)\rightarrow ((A\rightarrow \neg B)\rightarrow \neg A)$ But I had to decide, what formula to use as $B$.
Going back to my second proof, $\forall x(\neg (A \rightarrow  \neg B))$ and $\neg (\forall xA \rightarrow  \neg \forall xB)$ are equal.
That meant that whatever I could prove with one, I could prove with the other.
So, when I notice I could prove $\neg (A \rightarrow  \neg B)$ from $\forall x(\neg (A \rightarrow  \neg B))$, I knew I could prove the opposite from $(\forall xA \rightarrow  \neg \forall xB)$. This reduced the amount of things to try immensely.
