1. ## Fol 5

Enderton 2.5 problem 1.

(Semantic rule EI) Assume that the constant symbol $\displaystyle c$ does not occur in $\displaystyle \phi, \psi$, or $\displaystyle \Gamma$, and that $\displaystyle \Gamma;\phi_c^x \models \psi$. Show (without using the soundness and completeness theorems) that $\displaystyle \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 $\displaystyle s:V \rightarrow |A|$ such that if $\displaystyle \models_A \phi_c^x[s]$, then $\displaystyle \models_A \psi[s]$. Now it suffices to show that $\displaystyle \models_A \exists x \phi[s]$.

I can't proceed from here.

Any help will be appreciated.

2. ## Re: Fol 5

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

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

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

Lemma 2. $\displaystyle \models_{A(c\mid d)}\psi[s]$ iff $\displaystyle \models_A\psi[s]$.

3. ## Re: Fol 5

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

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

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

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

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

Thank you.

4. ## Re: Fol 5

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

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

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

By the substitution lemma, we have $\displaystyle \models_A \phi_c^x[s]$ iff $\displaystyle \models_A \phi[s(x | d) ]$ (i.e., $\displaystyle \bar{s}(t)=d$ for some d).
Yes, provided $\displaystyle \bar{s}(c)=d$. But $\displaystyle \models_A \phi_c^x[s]$ is the premise of the assumption; this is what we must show from the fact that $\displaystyle \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 $\displaystyle \bar{s}$ extends $\displaystyle 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, $\displaystyle \bar{s}$ must need information from A, so it should in fact be labeled with A: $\displaystyle \bar{s}_A$.

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

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