Deduction and universal generalization in FOL

Question

I'm working on a problem in Enderton's A Mathematical Introduction to Logic, Section 2.4, but having some trouble.

I need to prove that if $\vdash$ $\alpha$ $\rightarrow$ $\beta$, then $\vdash$ $\forall$x$\alpha$ $\rightarrow$ $\forall$x$\beta$

In the system, we have some axioms and modus ponens. The axioms are:

1. Tautologies.
2. $\forall$x$\alpha$ $\rightarrow$ $\alpha$$_t$$^x$, where $t$ is substitutable for $x$ in $\alpha$
3. $\forall$x($\alpha$ $\rightarrow$ $\beta$) $\rightarrow$ $\forall$x$\alpha$ $\rightarrow$ $\forall$x$\beta$
4. $\alpha$ $\rightarrow$ $\forall$x$\alpha$, when $x$ does not occur free in $\alpha$.

If we assume that $x$ doesn't occur free in $\alpha$ $\rightarrow$ $\beta$, then the deduction is straightforward.

5. $\alpha$ $\rightarrow$ $\beta$ (Assumption)
6. $\forall$x($\alpha$ $\rightarrow$ $\beta$) (Axiom 4)
7. $\forall$x$\alpha$ $\rightarrow$ $\forall$x$\beta$ (Axiom 3)

I do not know what to do when we haven't assumed that $x$ isn't free in $\alpha$ $\rightarrow$ $\beta$. Any help is appreciated.

One thought I had is that I'll need to do two proofs: one where I assume $\alpha$ $\rightarrow$ $\beta$ and $\beta$, and one where I assume $\alpha$ $\rightarrow$ $\beta$ and $\neg$$\alpha$. Does this sound like the right strategy?

Answer 1

Of course, the problem ask you to prove it in the "general case", i.e. with $x$ possibly free in $\alpha \rightarrow \beta$.

We have to note that :

$\vdash \alpha \rightarrow \beta$;

thus, we can apply [see page 117] the

GENERALIZATION THEOREM : If $\Gamma \vdash \varphi$ and $x$ do not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$.

In our case, we have $\Gamma = \emptyset$ and there are no free vars in it (simply because there are no formulae).

Thus we can apply the theorem to get :

$\vdash \forall x(\alpha \rightarrow \beta)$.

Now the conclusion is straightforward with Ax.3 and modus ponens.