Proving $\forall x (A\to B) \to(A \to \forall x B):x\notin \mbox{free}(A)$ in a Hilbert system where it is not an axiom

Question

I have no idea whether this question is way too specific or whether something similar has already been asked (we still need to work out a way to search for formulas I guess).

Anyways here I go: I want to show that some choice of (logical/quantifier) axioms for a Hilbert derivation system (first order logic, one sort) can prove all the axioms of some other choice.

I have the following at my disposal:

Axioms:

• (fot): first order tautologies (i.e. inserting formulas for the propositions in a propositional tautology)

• (aax): $\forall x A[x] \to A[t]$ (where $t$ is any term and we assume no conflicts with free variables getting bound, $[...]$ denotes replacement)

Inference rules:

• (mp): modus ponens

• (aru): $\frac{A\to B}{A\to\forall x B}$ where $x$ is not free in $A$.

I want to show that this system proves the formula:

$\forall x (A\to B) \to(A \to \forall x B)$ for $x$ not free in $A$ (which I will assume in the following).

This is of course very similar to (aru), but I want this formula, which is of course a stronger statement. I am quite lost here.

Here are my failed attempts: With (aax) and (aru), I easily get the provable rule $\frac{\forall x(A\to B)}{A\to\forall x B}$ which is the formulation of my goal formula as a rule (weaker).

I even get

$$\frac{\bar\forall(A\to B)}{A\to\forall x B}$$ where $\bar\forall$ denotes the universal closure of the following formula.

Using the Deduction Theorem (which I proved for this theory) I get that my system proves $$\bar\forall(A\to B)\to(A\to\forall x B).$$ but that is not exactly what I am looking for.

Answer 1

As you already observed, $$ \vdash \forall x(A\rightarrow B)\rightarrow (A\rightarrow \forall x B) $$ if $x$ is the only free variable in $A, B$, by the deduction theorem. In the general case, you can enlarge your language by new constants and replace the additional free variables (if any) by those constants to prove $$ \vdash \forall x(A(c_j)\rightarrow B(c_j,x))\rightarrow (A(c_j)\rightarrow \forall x B(c_j,x)) $$ in the same way. It is not hard to show, by an induction on formal proofs, that this implies what you want, namely the free variable version of this.

The first volume of Tourlakis, Lectures in logic in set theory discusses this material (in particular, it uses almost the same formalization); see Theorem I.4.15 there.

Answer 2

Using the tips by Christian Remling, I have been able to formulate the following explicit proof, which is quite long due to the removal of the use of the deduction theorem ($\land$ has higher precedence than $\to$):

1 $\vdash \forall x(A \to B) \to (A \to B)$ (aax)

2 $\vdash (\forall x(A \to B) \to (A \to B)) \to (\forall x(A \to B) \land A \to B)) $ (fot)

3 $\vdash \forall x(A \to B) \land A \to B$ (mp 1 2)

4 $\vdash \forall x(A \to B) \land A \to \forall x B$ (aru, applicable since $x$ not free in $\forall x(A \to B) \land A$)

5 $\vdash (\forall x(A \to B) \land A \to \forall x B) \to (\forall x(A \to B) \to ( A \to \forall x B)) $ (fot)

6 $\vdash \forall x(A \to B) \to ( A \to \forall x B) $ (mp 4 5)