Disproving the statement $\alpha\rightarrow\beta\models\forall x.\alpha\rightarrow\forall x.\beta$

Solution 1:

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$.

Solution 2:

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.