# How does one prove that if $Γ⊢¬∀xψ$ then $Γ⊢¬∀x¬¬ψ$ using the Hilbert System?

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.

• Ah yes, my mistake - have fixed this! – Maths That Imo Aug 23 '17 at 13:43
• Isn't there a rule similar to "$\Gamma, A\vdash \bot$ implies $\Gamma\vdash \neg A$" where $\bot$ is either a symbol meaning "false" or $B\land \neg B$ for any $B$ ? – Max Aug 23 '17 at 16:11
• You can derive a rule to that effect, yes - I'm unable to form a proof up to that point though. – Maths That Imo Aug 23 '17 at 16:49
• This boils down to showing that $\vdash \forall x \ \neg \neg \psi(x) \rightarrow \forall x \psi(x)$ ... which should be an elementary proof involving quantifiers (yes, you will have to use the quantifier rules, since this is not a propositional logic tautology). However, I am unclear how to do this in this system ... does your book have any example of a proof involving quantifiers? – Bram28 Aug 23 '17 at 21:45
• Assume $\forall x \lnot \lnot \psi$ and derive $\psi$ and then "generalize" to $\forall \psi$. By Ded Th: $\forall x \lnot \lnot \psi \to \forall x \psi$. Note: here we can safely "generalize" because in the premise $\forall x \lnot \lnot \psi$ $x$ is not free. – Mauro ALLEGRANZA Aug 25 '17 at 8:13