Disproving the statement $\alpha\rightarrow\beta\models\forall x.\alpha\rightarrow\forall x.\beta$ Prove or refute: $\alpha\rightarrow\beta\models\forall x.\alpha\rightarrow\forall x.\beta$
I believe that this statement is incorrect and want to provide a refutation for it. I know I should show that there is a structure and variable assignment s.t. $\alpha \to \beta$ is satisfied but $\forall x.\alpha \to \forall x.\beta$ ∀xα → ∀xβ is not satisfied, but I'm a bit lost on what this structure would like. Any hints? Or tips on how to approach this?
 A: Here is a proof of the statement:
Assume towards a contradiction that there is a structure $\mathcal{A}$ such that $\mathcal{A}\vDash \alpha \rightarrow \beta$ but $\mathcal{A}\nvDash \forall x\alpha \rightarrow \forall x \beta$. Then, $\forall s\; \; \mathcal{A}\vDash \alpha \rightarrow \beta (s)$ and therefore $\forall s\; \; \mathcal{A}\vDash \alpha (s)$ implies $\mathcal{A}\vDash \beta (s)$. Moreover, $\mathcal{A}\nvDash \forall x\alpha \rightarrow \forall x \beta$ means that there is some variable assignment function $s_0$ such that $\mathcal{A}\nvDash \forall x\alpha \rightarrow \forall x \beta (s_0)$. This is possible only if $\mathcal{A}\vDash \forall x\alpha(s_0)$ and $\mathcal{A}\nvDash \forall x \beta (s_0)$. But $\mathcal{A}\vDash \forall x\alpha(s_0)$ means that $\forall a \in A\; \; \mathcal{A} \vDash \alpha (s_0[x|a])$. Then, using the first part, we deduce that $\forall a \in A\; \; \mathcal{A} \vDash \beta (s_0[x|a])$. On the other hand, $\mathcal{A}\nvDash \forall x \beta (s_0)$ implies that there is $a\in A$ such that $\mathcal{A}\nvDash \beta (s_0[x|a])$. We get a contradiction. So any structure that models $\alpha \rightarrow \beta$ also models $\forall x\alpha \rightarrow \forall x \beta$.
A: Another important observation is that since our proof system is complete, we must be able to prove the statement, i.e. there is a deduction of $\forall x \alpha \rightarrow \forall x\beta$ from $\alpha \rightarrow \beta$. However, it suffices to show that $\{ \alpha \rightarrow \beta, \forall x\alpha \} \vdash \forall x \beta$. This is because of the deduction theorem. Here is the deduction:
$\forall x\alpha \; \; \; \; \; \; \; \; \; \; \; \;$      a non-logical axiom
$\forall x\alpha \rightarrow \alpha _{x}^x \; \; \; \; $  a logical axiom  (a quantifier axiom)
$\alpha _{x}^x \; \; \; \; \; \; \; \; \; \; \; \; \; \; $ rule of inference   (propositional consequence)
$\alpha \rightarrow \beta  \; \; \; \; \; \; \; \; \; \; $  a non-logical axiom
$\beta \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; $  rule of inference   (propositional consequence)
$y=y   \; \; \; \; \; \; \; \; \; \; $  a logical axiom
$y=y \rightarrow \beta \; \; \; \; \; \; \; \; \; \; \; \; $  rule of inference   ($x$ is bound in $y=y$)
$y=y \rightarrow \forall x\beta  \; \; \; \; \; \; \; \; \; \; $  rule of inference  (quantifier rule)
$\forall x\beta \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; $  rule of inference   (propositional consequence)
Note that $\alpha _{x}^x$ is the same as $\alpha$. They are literally the same formulas.
A: There are 2 common ways of interpreting free variables.  Whether the statement is true or not depends on which way you are using.  See this question: Terminology for free variables
If the intended interpretation of
$$\alpha\rightarrow\beta\models\forall x.\alpha\rightarrow\forall x.\beta$$
is
$$\forall x.(\alpha\rightarrow\beta)\models\forall x.\alpha\rightarrow\forall x.\beta$$
then the statement is true.  Whenever $\alpha$ holds, so does $\beta$, so if $\alpha$ always holds, so should $\beta$ always hold.
On the other hand, if your intended interpretation is that the $x$ in $(\alpha\rightarrow\beta)$ is defined elsewhere (such as an assumption), then you can construct a counter example where:

*

*There is an outstanding like assumption $x=2$

*$\alpha$ is always true

*$\beta$ is that $x$ is even

Then you get
$$x \text{ is even} \models \forall x . x \text{ is even}$$
which the outstanding assumption makes false.
