1. ## Fol 2

Show that if $x$ does not occur free in $\alpha$, then $\alpha \models \forall x \alpha$.

-----------------------------------------------------------
(*) $\models_A \forall x \phi[s]$ iff for every $d \in |A|$, we have $\models_A \phi[s(x|d)]$.

Let $A$ be any structure for the language and $s$ be any function $s: V \rightarrow |A|$ that satisfies $\alpha$. Therefore, $\models_A \alpha[s]$. Since x does not occur free in $\alpha$, $\alpha[s]=\alpha[s(x | d)]$. It follows that $\models_A \alpha[s(x|d)]$. Therefore, $\models_A \forall x \alpha[s]$ by (*). Now the conclusion follows.

Is this proof O.K or am I missing something?

Thank you.

2. ## Re: Fol 2

Originally Posted by logics
Let $A$ be any structure for the language and $s$ be any function $s: V \rightarrow |A|$ that satisfies $\alpha$.
I think it should say "satisfy" because A and s together satisfy $\alpha$.

The proof is OK. Here are some small details.

Originally Posted by logics
$\alpha[s]=\alpha[s(x | d)]$.
Do you mean they are equal as predicates on structures? If so, it's fine; otherwise, it is safer to say " $\models_B\alpha[s]$ iff $\models_B\alpha[s(x | d)]$ for any structure B," or " $\models_A\alpha[s]$ iff $\models_A\alpha[s(x | d)]$." This equivalence (or equality) is the key lemma in the proof, which has to be proved before, probably by induction on formulas using the precise definition of free occurrence.

Also, it would be better to make the scope of d more explicit. This means writing "for all d" and making sure that when you conclude $\models_A \forall x \alpha[s]$, no open assumption contains d. So, instead of
Originally Posted by logics
Since x does not occur free in $\alpha$, $\alpha[s]=\alpha[s(x | d)]$. It follows that $\models_A \alpha[s(x|d)]$.
I would write,

Since x does not occur free in $\alpha$, for all d we have that $\models_A\alpha[s]$ iff $\models_A\alpha[s(x | d)]$, and so $\models_A \alpha[s(x|d)]$.

Then the scope of d is the sentence above, which proves "for all d, $\models_A \alpha[s(x|d)]$."