Thread: 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.

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)$