Short task in model theory / 1.st order logic

Question

Im having the following problem:
If variable $x$ is bound in formula $\phi$, then $\phi\models\forall x \phi$.

It confuses me becouse if $x$ is already bound in $\phi$, then how is formula $\forall x \phi$ interpreted?

I concluded that if $A$ is a model of $\phi$, where variable is bound, then certainly $\phi$ has a same model as $\forall x \phi$, and $\phi \models \forall x \phi$. But i know this is not formal enough.

Thanks in advance.

Answer 1

In any model $M,$ $M\models\forall x\phi$ is iff for each $c\in M$ if we replace the unbound instances of $x$ in $\phi$ with $c$ then this new formula is also true in $M$.

Thus $M\models\forall x\phi$ since if we replace all free x in $\phi$ (i.e. none) then the new formula is also true. In other words there is nothing which $\forall x$ actually does (no free variables which it quantifies over) thus $M\models \phi$ iff $M\models \forall x \phi$.

This is a bit in the same flavor as saying if $a \in A$ then $a \in A\cup \emptyset$.

Answer 2

The "formality" of the proof depends on the details of the semantics.

See e.g. David Marker, Model Theory: An Introduction, page 11:

If $\phi$ is $\forall v_i \psi(v_i)$, then $\mathcal M \vDash \phi$ if $\mathcal M \vDash \psi(a)$ for all $a \in M$.

If $\mathcal M \vDash \phi(a)$ we say that $\mathcal M$ satisfies $\phi( a )$ or $\phi( a )$ is true in $\mathcal M$.

We say that $\phi$ is a logical consequence of $T$ and write $T \vDash \phi$ if $\mathcal M \vDash \phi$ whenever $\mathcal M \vDash T$.

Thus, consider a structure $\mathcal M$ such that $\mathcal M \vDash \phi$, and consider $\forall x \phi$.

We want that $\mathcal M \vDash \phi(a)$ for every $a \in M$, where $\phi(a) = \phi[a/x]$, i.e. the result of replacing the free occurrences of $x$ in $\phi$ with $a$.

But $\phi$ has no free occurrences of $x$, and thus: $\phi(a)=\phi$.

Thus, $\mathcal M \vDash \phi(a)$, for every $a \in M$, i.e.:

$\mathcal M \vDash \forall x \phi$.