If $x$ is not a free variable in $A$, then $\vDash (\forall x(A \to B))\to (A\to \forall x B) $

Question

By assuming (towards contradiction) that some model $M$ and assignment $v$ do not satisfy the formula, we gather:

1. $M,v \vDash (\forall x(A \to B))$ and $M,v \not \vDash (A\to \forall x B)$
2. Since $M,v \not \vDash (A\to \forall x B)$, $M,v \vDash A$ and for some $x$-varient assignment (for which, any other variable than $x$ is assigned the same value) $v^\prime$, it holds that $M,v^\prime \not \vDash B$.
3. Since $x$ is not free in $A$ and $M,v \vDash A$, we have $M,v^\prime \vDash A$. This goes to show with (2) that $M,v^\prime \not \vDash A\to B$
4. Therefore we conclude $M,v\not \vDash \forall x(A\to B)$ which contradicts (1).

The only argument I don't quite get is in line (3) - if $x\notin FV(A)$, then either:

• $A$ has no instances of $x$, so surely $M,v^\prime \vDash A$ - it doesn't affect $A$ what $x$ evaluates to.
• $A$ is of the form $\forall x.\phi(x)$, which means for any $x$-varient (like $v^\prime$) it holds that $M, v^\prime \vDash \phi$. So of course $M, v^\prime \vDash A$.
• $A$ is of the form $\exists x.\phi(x)$, which means for some $x$-varient $v^{\prime\prime}$ it holds that $M, v^{\prime\prime} \vDash \phi$. But who is to say that for the specific $v^\prime$ we chose earlier this is also the case (i.e. $v^\prime = v^{\prime \prime}$)?

I guess I'm missing something quite basic.

Answer 1

First note that your three bullet points do not cover all cases: For example $A$ might be such that $x$ appears once under an existential quantifier and once under a universal quantifier. But this is not really relevant to lift your confusion I think.

One way to understand line three is the following: If $x$ is not free in $A$ then it does not matter what value is assigned to $x$ in $v$. Or in other words: Since we have $M, v \models A$ we get $M, v^* \models A$ for any $v^*$ that differs from $v$ only for $x$.

For the 3rd bullet point: You have $M, v'' \models \phi$. What you want to show is that $M, v' \models \exists x \phi(x)$. Because $v''$ differs from $v'$ only in $x$ this follows by the definition of the semantics of the existential quantifier. The definition I found is (note that I use different notation and tried to adjust it accordingly. Hope I didn't make any mistake.): $M, v \models \exists x G \iff$ for some $u$ $M, v[x \rightarrow u] \models G$. Now note that in your case $v'[x \rightarrow u] = v''$ for some $u$. And you have $M, v'' \models \phi \implies M, v'[x \rightarrow u] \models \phi \implies M, v' \models \exists x \phi$