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

Question

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?

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

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

Answer 3

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.