Results 1 to 2 of 2

Math Help - Fol 2

  1. #1
    Junior Member
    Joined
    Nov 2011
    Posts
    59

    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.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,528
    Thanks
    773

    Re: Fol 2

    Quote Originally Posted by logics View Post
    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.

    Quote Originally Posted by logics View Post
    \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
    Quote Originally Posted by logics View Post
    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)]."
    Follow Math Help Forum on Facebook and Google+


/mathhelpforum @mathhelpforum