1. ## 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.

2. ## Re: Fol 5

Originally Posted by logics
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]$.

3. ## Re: Fol 5

Originally Posted by emakarov
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.

4. ## Re: Fol 5

Originally Posted by logics
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$.

Originally Posted by logics
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]$.

Originally Posted by logics
(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.