I am reading the proof of omitting types theorem (page 125 – 127) in Marker's Model Theory: An Introduction (the same proof is in https://proofwiki.org/wiki/Omitting_Types_Theorem) and having the following problem.
On page 127 line 5 of Marker's book (or Stage $k+1=3i+3$ in the link), there is $\phi \in p$ s.t. $T \not\models \psi(\bar v) \rightarrow \phi(\bar v)$, because $p$ is not isolated.
Then there is an $\mathcal{L}$-structure $\mathcal{N} \models T$ and $\bar a \in N^n$ s.t. $\mathcal{N} \models \psi(\bar a) \wedge \neg \phi(\bar a)$.
However, $\phi$ may contain constant symbols from $\mathcal{L}$ and some $e_i$ may also be in $\mathcal{L}$ (only considering $n$-tuples from the new constants $C = \{c_0, c_1, …\}$ rather than from all constant symbols of $\mathcal{L}^*$ is not sufficient). Then, we may not make $\mathcal{N}$ a model of $\theta_s \wedge \neg\phi(e_1,…,e_n)$ by interpreting $e_i$ as $a_i$ and $c \in C – \{e_1,…,e_n\}$ as the witness of $v_c$.
My attempt: add $c_{2i} = d_i$ (where $c_i \in C$) to $T$ for each constant symbol $d_i$ in $\mathcal{L}$ at stage $0$. Then, we only need to consider $n$-tuples from the new constants $C$ by the definition of Henkin construction. The reason why I use $2i$ is that it ensures stage $k+1=3s+2$ still works. However, we cannot take an "infinite conjunction" at stage $k+1=3s+3$ to find $\phi(\bar v)$. My attempt works if $\mathcal{L}$ only contains finitely many constant symbols.
Thanks in advance for any help.
Best Answer
I answer my own question. The same Henkin construction as in the proof of compactness theorem is not used here. Alternatively, we only consider the $n$-tuples from new constants $C$ in stage $k+1=3s+3$. The "witness property" from stage $k+1=3s+2$ is actually a stronger version of witness property (it is over $C$ rather than all constant symbols). There is $\mathcal{M} \models T^*$. By the witness property, we can prove that the interpretation of $C$ is actually a substructure of $\mathcal{M}$, call it $\mathcal{M}'$. Tarski-Vaught test is then used to show that $\mathcal{M}'$ is an elementary substructure of $\mathcal{M}$.