I'm reading through Jech's Set Theory, in particular chapter 12 on model theory. After defining an elementary submodel, he writes that
The key lemma in construction of elementary submodels is this: A subset $B\subseteq A$ forms an elementary submodel of $\mathfrak A$ if and only if for every formula $\varphi(u,x_1,\dots,x_n)$ and every $a_1,\dots,a_n\in B$,
$$(\exists a\in A \text{ s.t. } \mathfrak A\models \varphi[a,a_1,\dots,a_n])\to(\exists a\in B \text{ s.t. } \mathfrak A\vDash\varphi[a,a_1,\dots,a_n]).$$
I think I'm fine with the forwards direction, but the backwards direction is giving me trouble. Given an arbitrary formula $\varphi$ and $a_1,\dots,a_n$ in $B$, why does it follow from the above implication that $\mathfrak B \models \varphi[a_1,\dots,a_n]\leftrightarrow \mathfrak A\models \varphi[a_1,\dots,a_n]$?
Best Answer
It would have been better indeed if Jech had inserted an explanatory paragraph or referred the reader to textbooks on model theory to look up the details of the proof.
Apart from the usual method of structural induction on the complexity of $\varphi$, it should be remarked that the lemma has an argument form that is interesting in itself.
The lemma can be expressed in the language of propositional calculus as
$$P\leftrightarrow (Q\rightarrow R)$$
We can break $P$ down further, considering that $\mathcal{B}$, a submodel of $\mathcal{A}$, is called elementary, denoted by $\mathcal{B}\preccurlyeq\mathcal{A}$, if and only if, given any elements $a_1, \ldots, a_n \in B$ and any formula $\varphi$,
$$\mathcal{B}\models\varphi(a_1,\ldots,a_n)\iff\mathcal{A}\models \varphi(a_1,\ldots,a_n)$$
Thus, we can rewrite the lemma replacing $\mathcal{B}\preccurlyeq\mathcal{A}$ with the aforementioned equivalence
$$(P_{B}\leftrightarrow P_{A})\leftrightarrow (Q\rightarrow R)$$
As noted in the question, given a subset $\mathrm{B}\subseteq\mathrm{A}$ and any formula $\varphi(x, a_1,\ldots, a_n)$ where $a_1,\ldots,a_n\in\mathrm{B}$, it is relatively straightforward to show that
$$(P_{B}\leftrightarrow P_{A})\rightarrow (Q\rightarrow R)$$
We shall work out
$$(Q\rightarrow R)\rightarrow(P_{B}\leftrightarrow P_{A})$$
that is, assuming the implication of the lemma.
In case that $\varphi$ is an atomic (quantifier-free and connective-free) formula,
$$\mathcal{B}\models\varphi(a_1,\ldots,a_n)\implies\mathcal{A}\models \varphi(a_1,\ldots,a_n)$$
is agreeably obvious by the given conditions. We get
$$\mathcal{A}\models\varphi(a_1,\ldots,a_n)\implies\mathcal{B}\models \varphi(a_1,\ldots,a_n)$$
by using the assumed implication of the lemma. Hence,
$$\mathcal{A}\models\varphi(a_1,\ldots,a_n)\iff\mathcal{B}\models \varphi(a_1,\ldots,a_n)$$
In case that $\varphi$ is of the form $\neg\psi$, we observe
$$\mathcal{B}\models\neg\psi(a_1,\ldots,a_n)\iff\mathcal{B}\nvDash\psi(a_1,\ldots,a_n)\iff\mathcal{A}\nvDash\psi(a_1,\ldots,a_n)\iff\mathcal{A}\models\neg\psi(a_1,\ldots,a_n)$$
In case that $\varphi$ is of the form $\psi\wedge\theta$
$\mathcal{B}\models\psi(a_1,\ldots,a_n)\wedge\theta(a_1,\ldots,a_n)\iff\mathcal{B}\models\psi(a_1,\ldots,a_n)\text{ and } \mathcal{B}\models\theta(a_1,\ldots,a_n)$
$\iff\mathcal{A}\models\psi(a_1,\ldots,a_n)\text{ and }\mathcal{A}\models\theta(a_1,\ldots,a_n)$
$\iff\mathcal{A}\models\psi(a_1,\ldots,a_n)\wedge\theta(a_1,\ldots,a_n)$
In case that $\varphi$ is of the form $(\exists x)\psi(x, a_1,\ldots,a_n)$, we argue as follows:
If $\mathcal{B}\models\exists\psi(x, a_1,\ldots,a_n)$, then there is an $a_{0}\in\mathrm{B}$ such that $\mathcal{B}\models\psi(a_{0}, a_1,\ldots,a_n)$ which is a quantifier-free formula; therefore, $\mathcal{A}\models\exists\psi(x, a_1,\ldots,a_n)$. Hence, $\mathcal{A}\models\psi(a_{0}, a_1,\ldots,a_n)$. We have shown that
$$\mathcal{B}\models\exists\psi(x, a_1,\ldots,a_n)\implies\mathcal{A}\models\exists\psi(x, a_1,\ldots,a_n)$$
Now, we intend to show that
$$\mathcal{A}\models\exists\psi(x, a_1,\ldots,a_n)\implies\mathcal{B}\models\exists\psi(x, a_1,\ldots,a_n)$$
If $\mathcal{A}\models\exists\psi(x, a_1,\ldots,a_n)$, then there is an $a_{0}\in\mathrm{A}$ such that $\mathcal{A}\models\psi(a_{0}, a_1,\ldots,a_n)$ which is a quantifier-free formula. Therefore, $\mathcal{B}\models\psi(a_{0}, a_1,\ldots,a_n)$. Hence, $a_{0}\in\mathcal{B}$, whereby we obtain the consequent.