The text for my course states that "it is easy to prove (using deduction theorem and tautologies) that if $Γ⊢¬∀xψ$ then $Γ⊢¬∀x¬¬ψ$.
For clarification, the axioms of the system are:
$(α → (β → α))$ (A1)
$((α → (β → γ)) → ((α → β) → (α → γ)))$ (A2)
$((¬β → ¬α) → (α → β)) (A3)$
$(∀x_iα → α[t/x_i])$ if t is free for $x_i$ in α (A4)
$(∀x_i(α → β) → (α → ∀xiβ))$ if $x_i∈Free(α)$ (A5)
$∀x_i(x_i = x_i)$(A6)
$(x_i = x_j → (ϕ → ϕ′))$ where $ϕ$ is atomic and $ϕ′$ is obtained from $ϕ$ by replacing some occurrences of $x_i$ by $x_j$, (A7)
The inference rules are modus ponens and "generalisation": ($∀$) From $α$ infer $∀x_iα$ provided that $x_i$ doesn't appear in the premises
I have been trying to figure out how to prove this, but keep on failing - the section of the text that says it can be done using tautologies and DT makes me think that I shouldn't be using any of the rules other than A1,2&3.
I've considered trying to prove that $Γ⊢(∀x¬¬ψ→∀xψ)$ and then using axiom 3 to conclude, but here too I come to a dead end. My intuition is to then use A4 & argue by contradiction (using a proved tautology) in some way, but to get to a contradiction I need to use ($∀$ generalisation), and I can't do that as I don't know whether $x_i$ occurs free in the premises.