# Thread:

1. ## Fol 3

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

--------------------------------------------------------------------------

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

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

I am stuck here. Any help will be appreciated.

2. ## Re: Fol 3

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

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

$\models_A Pz(fx)$ iff
$\mathbf{P}(s_A(z),s_A(fx))=T$ iff
$\mathbf{P}(s_A(z),\mathbf{f}(s(x)))=T$ iff
$\mathbf{P}(s_A(z),\mathbf{f}(s(y)))=T$ iff
$\mathbf{P}(s_A(z),s_A(fy))=T$ iff
$\models_A Pz(fy)$
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 35, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.8206197023391724, "perplexity_flag": "head"}