Results 1 to 2 of 2

Thread: Fol 3

  1. #1
    Junior Member
    Nov 2011

    Fol 3

    Show that the formula $\displaystyle x=y \rightarrow Pzfx \rightarrow Pzfy$ (where $\displaystyle f$ is a one-place function symbol and $\displaystyle P$ is a two-place predicate symbol) is valid.


    (*) If $\displaystyle \gamma;\alpha \models \phi$, then $\displaystyle \gamma \models (\alpha \rightarrow \phi)$.

    We show $\displaystyle \models x=y \rightarrow Pzfx \rightarrow Pzfy$.
    By (*), it suffices to show that $\displaystyle \{x=y, Pzfx\} \models Pzfy$. Therefore, we need to show every $\displaystyle A$ that satisfies $\displaystyle x=y$ and $\displaystyle Pzfx$ with every function $\displaystyle s:V \rightarrow |A|$ satisfies $\displaystyle Pzfy$ with $\displaystyle s$. That is, if $\displaystyle \models_Ax=y[s]$ and $\displaystyle \models_A Pzfx[s]$, then $\displaystyle \models_A Pzfy[s]$.

    I am stuck here. Any help will be appreciated.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Oct 2009

    Re: Fol 3

    As you know, given A, the function $\displaystyle s:V\to|A|$ can be extended to a function $\displaystyle s_A$ from the set of all terms to |A|. In particular, A associates some function $\displaystyle \mathbf{f}:|A|\to|A|$ to a unary functional symbol $\displaystyle f$ and some function $\displaystyle \mathbf{P}:|A|\times|A|\to\{T,F\}$ to a binary predicate symbol $\displaystyle P$. Then $\displaystyle s_A(x)=s(x)$, $\displaystyle s_A(fx)=\mathbf{f}(s_A(x))$ and $\displaystyle \models_A Pz(fx)$ iff $\displaystyle \mathbf{P}(s_A(z),s_A(fx))=T$.

    By definition of $\displaystyle \models$, if $\displaystyle \models_Ax=y[s]$, then $\displaystyle s(x) = s(y)$. Therefore,

    $\displaystyle \models_A Pz(fx)$ iff
    $\displaystyle \mathbf{P}(s_A(z),s_A(fx))=T$ iff
    $\displaystyle \mathbf{P}(s_A(z),\mathbf{f}(s(x)))=T$ iff
    $\displaystyle \mathbf{P}(s_A(z),\mathbf{f}(s(y)))=T$ iff
    $\displaystyle \mathbf{P}(s_A(z),s_A(fy))=T$ iff
    $\displaystyle \models_A Pz(fy)$
    Follow Math Help Forum on Facebook and Google+

/mathhelpforum @mathhelpforum