Is $A\to B\vdash\forall xA\to \forall xB$ Correct?

Question

Question Is $A\to B\vdash\forall xA\to \forall xB$ correct? If yes and if possible, please prove it.

I am learning Skolem normal form now. I'm trying to prove $A'\vdash A$, where $A$ is a prenex normal form and $A'$ is the Skolem normal form of $A$.

There is one step when proving the theorem.

Because $B_{f(x_1, ..., x_n)}^y\vdash\exists yB$, $\forall x_1 \forall ... \forall x_n B_{f(x_1, ..., x_n)}^y\vdash\forall x_1 \forall ... \forall x_n \exists yB$.

It confused me. I know that $B_{f(x_1, ..., x_n)}^y\vdash\exists yB$ comes from existential generalization, but I don't know how does it imply $\forall x_1 \forall ... \forall x_n B_{f(x_1, ..., x_n)}^y\vdash\forall x_1 \forall ... \forall x_n \exists yB$.

I think this step implies $A\to B\vdash\forall xA\to \forall xB$ , but I don't know if it is correct and how to prove it.

Answer 1

It is correct:

1. $$A\rightarrow B\qquad\text{Hypothesis}$$
2. $$\forall xA\rightarrow A\qquad\text{Axiom 4}$$
3. $$\forall xA\rightarrow B\qquad\text{TI(1, 2)}$$
4. $$\forall x(\forall xA\rightarrow B)\qquad\text{G(3)}$$
5. $$\forall x(\forall xA\rightarrow B)\rightarrow (\forall x A\rightarrow\forall xB)\qquad\text{Axiom 5}$$
6. $$∀xA → ∀xB\qquad\text{MP(4, 5)}$$

where, in a widely used Hilbert-style axiomatic system,

Axiom 4 is $\forall xA(x)\rightarrow A(t)\;t$ is free for $x$ in $A$ (notice that $x$ is free for $x$ as well),

Axiom 5 is $\forall x(A\rightarrow B)\rightarrow (A\rightarrow\forall x B)$ $x$ does not occur free in $A$,

$G$ is the rule of generalisation: From any wff $A$ and for any variable $x$, $\forall xA(x)$ can be derived,

$MP$ is the rule of modus ponens,

$TI$ is the metatheorem stating transitivity of implication.