Results 1 to 4 of 4

Math Help - Fol 5

  1. #1
    Junior Member
    Joined
    Nov 2011
    Posts
    59

    Fol 5

    Enderton 2.5 problem 1.

    (Semantic rule EI) Assume that the constant symbol c does not occur in \phi, \psi, or \Gamma, and that \Gamma;\phi_c^x \models \psi. Show (without using the soundness and completeness theorems) that \Gamma; \exists x \phi \models \psi.

    If I were able to use the soundness theorem, I could use the rule EI and apply the soundness theorem. However, it is not allowed to use the soundness theorem.

    =====

    Let A be a structure for the language and let s:V \rightarrow |A| such that if \models_A \phi_c^x[s], then \models_A \psi[s] . Now it suffices to show that \models_A \exists x \phi[s].

    I can't proceed from here.

    Any help will be appreciated.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,506
    Thanks
    765

    Re: Fol 5

    Quote Originally Posted by logics View Post
    Let A be a structure for the language and let s:V \rightarrow |A| such that if \models_A \phi_c^x[s], then \models_A \psi[s] . Now it suffices to show that \models_A \exists x \phi[s].
    If we forget about \Gamma for a moment, what's the use to select some A and s such that \models_A \phi_c^x[s] implies \models_A \psi[s] ? This implication holds for all A and s. Also, how does it help to prove \models_A \exists x \phi[s]? You need to assume this for some A and s and show that \models_A\psi[s].

    Each structure provides an interpretation for some language. If a constant c is not in the language of structure A and d\in|A|, then by A(c\mid d) I'll denote a structure for the same language with c added which maps c into x. Use the following facts where c does not occur in \phi, \psi, or the language of A.

    Lemma 1. \models_A\phi[s(x\mid d)] iff \models_{A(c\mid d)}\phi^x_c[s].

    Lemma 2. \models_{A(c\mid d)}\psi[s] iff \models_A\psi[s].
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Junior Member
    Joined
    Nov 2011
    Posts
    59

    Re: Fol 5

    Quote Originally Posted by emakarov View Post
    If we forget about \Gamma for a moment, what's the use to select some A and s such that \models_A \phi_c^x[s] implies \models_A \psi[s] ? This implication holds for all A and s. Also, how does it help to prove \models_A \exists x \phi[s]? You need to assume this for some A and s and show that \models_A\psi[s].
    My understanding of " \models_A \phi_c^x[s] implies \models_A \psi[s] " is that for any A and any s, if \models_A \phi_c^x[s], then the same A and s holds for \models_A \psi[s] . By the choices of A and s, we already knew \models_A \psi[s] by hypothesis. That is why I said it suffices to show \models_A \exists x \phi[s]. Is this statement true?

    (substitution lemma) If the term t is substitutable for the variable x in the wff \phi, then
    \models_A \phi_t^x[s] iff  \models_A \phi[s(x | \bar{s}(t))] .

    By the substitution lemma, we have \models_A \phi_c^x[s] iff \models_A \phi[s(x | d) ] (i.e., \bar{s}(t)=d for some d).

    Since \models_A \phi[s(x | d) ] for some d, we have the desired result \models_A \exists \phi[s].

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

    Thank you.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,506
    Thanks
    765

    Re: Fol 5

    Quote Originally Posted by logics View Post
    My understanding of " \models_A \phi_c^x[s] implies \models_A \psi[s] " is that for any A and any s, if \models_A \phi_c^x[s], then the same A and s holds for \models_A \psi[s] .
    Yes, this is the understanding of \phi_c^x\models\psi.

    Quote Originally Posted by logics View Post
    That is why I said it suffices to show \models_A \exists x \phi[s]. Is this statement true?
    You need to prove \exists x \phi \models \psi. This means that for every A and s, you need to assume \models_A(\exists x \phi)[s] and show \models_A\psi[s].

    Quote Originally Posted by logics View Post
    (substitution lemma) If the term t is substitutable for the variable x in the wff \phi, then
    \models_A \phi_t^x[s] iff  \models_A \phi[s(x | \bar{s}(t))] .

    By the substitution lemma, we have \models_A \phi_c^x[s] iff \models_A \phi[s(x | d) ] (i.e., \bar{s}(t)=d for some d).
    Yes, provided \bar{s}(c)=d. But \models_A \phi_c^x[s] is the premise of the assumption; this is what we must show from the fact that \models_B \exists x\,\phi[s] (for a possibly different structure B).

    Now, I don't have the book, so I am not sure how \bar{s} extends s from variables to all terms. Usually, the structure A is responsible for assigning meaning to constants, function symbols and predicate symbols, and the environment s only maps variables to |A|. This means that to interpret terms, \bar{s} must need information from A, so it should in fact be labeled with A: \bar{s}_A.

    We fix arbitrary A and s and assume \models_A(\exists x\,\phi)[s], i.e., \models_A\phi[s(x|d)] for some d\in|A|. If \bar{s}(c) were d, then we would have \models_A\phi[s(x|\bar{s}(c))], and by the substitution lemma we could conclude \models_A\phi^x_c[s]. Then by assumption \phi_c^x\models\psi we would have \models_A\psi[s], as required.

    However, \bar{s}(c) is in fact \bar{s}_A(c), and since c does not occur in \phi or \psi, there is no reason why A has to interpret c at all, and if it does, it may interpret it as something different then the witness for x in \exists x\,\phi. Therefore, we have to modify the structure A by mapping c to d: this is what I denoted by A(c|d). Let B=A(c|d). Then \models_A\phi[s(x|d)] implies \models_{B}\phi[s(x|d)] by Lemma 2 from post #2 (which is pretty obvious), i.e., \models_B\phi[s(x|\bar{s}_B(c))], and you can use the substitution lemma.
    Follow Math Help Forum on Facebook and Google+


/mathhelpforum @mathhelpforum