[proofplan] We build a complete Henkin theory in a countable expansion of $L$ by constants, while adding extra requirements that force every closed-term tuple to miss each type $p_i$. The local avoidance argument says that whenever a finite condition is consistent, and a closed-term tuple is under consideration, non-principality gives a formula from the relevant type whose negation may be added without destroying consistency. The resulting complete Henkin theory has a countable term model. Since every element of the term model is represented by a closed term, the avoidance requirements ensure that no tuple realizes any of the types. [/proofplan]

[step:Expand the language by constants and enumerate all requirements] Let $C=\{c_n:n\in\mathbb N\}$ be a countably infinite set of new constant symbols disjoint from $L$, and let \begin{align*} L^*:=L\cup C \end{align*} denote the expanded language. Since $L$ is countable and $C$ is countable, the set of $L^*$-formulas is countable. We fix an enumeration of three kinds of requirements: 1. every $L^*$-sentence $\sigma$ must eventually be decided; 2. every existential $L^*$-sentence $\exists z\,\psi(z)$ must receive a Henkin witness; 3. for every $i\in\mathbb N$ and every closed $L^*$-term tuple $t$ of the same length as $x_i$, the tuple $t$ must be forced not to realize $p_i$. More explicitly, let $(R_n)_{n\in\mathbb N}$ be an enumeration in which every requirement of the following forms appears at least once: \begin{align*} &\text{decide } \sigma,\\ &\text{witness } \exists z\,\psi(z),\\ &\text{avoid } (i,t), \end{align*} where $\sigma$ ranges over all $L^*$-sentences, $\exists z\,\psi(z)$ ranges over all existential $L^*$-sentences with $z$ a single variable, and $(i,t)$ ranges over all pairs such that $i\in\mathbb N$ and $t$ is a closed $L^*$-term tuple of length $|x_i|$. [/step]

[step:Prove the local avoidance lemma][claim:Local avoidance for a non-principal type] Let $i\in\mathbb N$. Let $\chi(x_i)$ be an $L$-formula such that \begin{align*} T\cup\{\exists x_i\,\chi(x_i)\} \end{align*} is consistent. If $p_i(x_i)$ is non-principal over $T$, then there exists $\varphi(x_i)\in p_i$ such that \begin{align*} T\cup\{\exists x_i\,(\chi(x_i)\wedge \neg\varphi(x_i))\} \end{align*} is consistent. [/claim] [proof] Suppose, toward a contradiction, that for every $\varphi(x_i)\in p_i$ the theory \begin{align*} T\cup\{\exists x_i\,(\chi(x_i)\wedge \neg\varphi(x_i))\} \end{align*} is inconsistent. Then for every $\varphi(x_i)\in p_i$ we have \begin{align*} T\models \forall x_i\,(\chi(x_i)\to \varphi(x_i)). \end{align*} Since $T\cup\{\exists x_i\,\chi(x_i)\}$ is consistent, the formula $\chi(x_i)$ is consistent with $T$. Therefore $\chi(x_i)$ is a principal formula for $p_i$ over $T$, contradicting the hypothesis that $p_i$ is non-principal over $T$. Hence some $\varphi(x_i)\in p_i$ has the asserted consistency property. [/proof][/step]

[guided]Fix $i\in\mathbb N$ and an $L$-formula $\chi(x_i)$ such that $T\cup\{\exists x_i\,\chi(x_i)\}$ is consistent. The formula $\chi$ describes a possible tuple in a model of $T$. We want to strengthen this possible description so that it avoids at least one formula from $p_i$. Assume the desired conclusion fails. Then for every $\varphi(x_i)\in p_i$, adding the assertion that $\chi$ holds while $\varphi$ fails makes the theory inconsistent: \begin{align*} T\cup\{\exists x_i\,(\chi(x_i)\wedge \neg\varphi(x_i))\} \end{align*} is inconsistent. Equivalently, every model of $T$ satisfies that any tuple satisfying $\chi$ also satisfies $\varphi$: \begin{align*} T\models \forall x_i\,(\chi(x_i)\to \varphi(x_i)). \end{align*} This holds for every $\varphi(x_i)\in p_i$. But $\chi(x_i)$ is itself consistent with $T$, because $T\cup\{\exists x_i\,\chi(x_i)\}$ is consistent. Thus $\chi$ is a single $T$-consistent formula implying every formula in $p_i$. That is exactly the assertion that $p_i$ is principal over $T$, contrary to the hypothesis. Therefore there must be some $\varphi(x_i)\in p_i$ such that \begin{align*} T\cup\{\exists x_i\,(\chi(x_i)\wedge \neg\varphi(x_i))\} \end{align*} is consistent.[/guided]

[step:Construct a finite-consistency chain meeting all requirements] We construct an increasing sequence $(\Delta_n)_{n\in\mathbb N}$ of finite sets of $L^*$-sentences such that $T\cup\Delta_n$ is consistent for every $n\in\mathbb N$. Put $\Delta_0=\varnothing$. Assume $\Delta_n$ has been defined and $T\cup\Delta_n$ is consistent. If $R_n$ is the requirement to decide an $L^*$-sentence $\sigma$, then at least one of \begin{align*} T\cup\Delta_n\cup\{\sigma\},\qquad T\cup\Delta_n\cup\{\neg\sigma\} \end{align*} is consistent. Define $\Delta_{n+1}$ by adding one of $\sigma$ or $\neg\sigma$ that preserves consistency. If $R_n$ is the requirement to witness an existential sentence $\exists z\,\psi(z)$, choose a constant $c_m\in C$ that does not occur in any sentence of $\Delta_n$ or in $\exists z\,\psi(z)$. Define \begin{align*} \eta:=\exists z\,\psi(z)\to \psi(c_m). \end{align*} Then $T\cup\Delta_n\cup\{\eta\}$ is consistent. To justify this, suppose it were inconsistent. Since $c_m$ does not occur in $T$, in $\Delta_n$, or in $\exists z\,\psi(z)$, the new-constant generalization lemma implies that $T\cup\Delta_n$ proves \begin{align*} \neg\exists z\,\bigl(\exists w\,\psi(w)\to \psi(z)\bigr). \end{align*} But first-order logic proves \begin{align*} \exists z\,\bigl(\exists w\,\psi(w)\to \psi(z)\bigr): \end{align*} if $\exists w\,\psi(w)$ is false, any $z$ witnesses the implication, while if $\exists w\,\psi(w)$ is true, a witness to $\psi$ witnesses the implication. Thus $T\cup\Delta_n$ would be inconsistent, contradicting the induction hypothesis. Set \begin{align*} \Delta_{n+1}:=\Delta_n\cup\{\eta\}. \end{align*} If $R_n$ is the requirement to avoid $(i,t)$, where $t$ is a closed $L^*$-term tuple of length $|x_i|$, let $d=(d_1,\dots,d_m)$ be the finite tuple of all new constants from $C$ occurring in $\Delta_n$ or in $t$. Let $y=(y_1,\dots,y_m)$ be a tuple of distinct variables of the same length as $d$. Let $\theta(y)$ be the $L$-formula obtained from the finite conjunction of all sentences in $\Delta_n$ by replacing each $d_j$ with $y_j$. Let $t(y)$ be the $L$-term tuple obtained from $t$ by the same replacement. Since $T\cup\Delta_n$ is consistent, the $L$-formula \begin{align*} \chi(x_i):=\exists y\,(\theta(y)\wedge x_i=t(y)) \end{align*} is consistent with $T$. By the [local avoidance lemma](/theorems/5071), choose $\varphi(x_i)\in p_i$ such that \begin{align*} T\cup\{\exists x_i\,(\chi(x_i)\wedge\neg\varphi(x_i))\} \end{align*} is consistent. Substituting the definition of $\chi$ gives the consistency of \begin{align*} T\cup\{\exists y\,(\theta(y)\wedge\neg\varphi(t(y)))\}. \end{align*} Replacing the variables $y_j$ back by the corresponding constants $d_j$ preserves consistency. Indeed, if \begin{align*} T\cup\Delta_n\cup\{\neg\varphi(t)\} \end{align*} were inconsistent, then replacing the finitely many new constants $d_j$ by variables $y_j$ and existentially quantifying them would imply the inconsistency of \begin{align*} T\cup\{\exists y\,(\theta(y)\wedge\neg\varphi(t(y)))\}, \end{align*} contradicting the consistency just obtained; this use of the new-constants lemma is valid because the constants $d_j$ are not symbols of the original language $L$ and do not occur in $T$. Hence \begin{align*} T\cup\Delta_n\cup\{\neg\varphi(t)\} \end{align*} is consistent. Define \begin{align*} \Delta_{n+1}:=\Delta_n\cup\{\neg\varphi(t)\}. \end{align*} This completes the recursive construction. [/step]

[step:Form the complete Henkin theory generated by the construction] Define the $L^*$-theory \begin{align*} \Gamma:=T\cup\bigcup_{n\in\mathbb N}\Delta_n. \end{align*} Every finite subset of $\Gamma$ is contained in $T\cup\Delta_n$ for some $n\in\mathbb N$, so $\Gamma$ is consistent by the [compactness theorem for first-order logic](/theorems/4290). The decision requirements imply that $\Gamma$ is complete as an $L^*$-theory: for every $L^*$-sentence $\sigma$, either $\sigma\in\Gamma$ or $\neg\sigma\in\Gamma$. We also record the closure under logical consequence that will be used below. If $\Gamma\vdash \tau$ for an $L^*$-sentence $\tau$, then $\Gamma\cup\{\neg\tau\}$ is inconsistent. Since $\Gamma$ is complete, either $\tau\in\Gamma$ or $\neg\tau\in\Gamma$; the second alternative contradicts the consistency of $\Gamma$. Therefore $\tau\in\Gamma$. The Henkin requirements imply that if $\exists z\,\psi(z)\in\Gamma$, then for some constant $c_m\in C$ we have $\psi(c_m)\in\Gamma$. Indeed, the witness requirement for $\exists z\,\psi(z)$ appears in the enumeration, and the implication \begin{align*} \exists z\,\psi(z)\to\psi(c_m) \end{align*} is then added to $\Gamma$; completeness and closure under logical consequence give $\psi(c_m)\in\Gamma$. [/step]

[step:Build the countable term model of the Henkin theory] Let $\mathcal T$ be the set of closed $L^*$-terms. Define an [equivalence relation](/page/Equivalence%20Relation) $\sim$ on $\mathcal T$ by \begin{align*} s\sim t \quad\Longleftrightarrow\quad \Gamma\vdash s=t. \end{align*} Let $M^*$ be the set of equivalence classes $[t]$ for $t\in\mathcal T$. Since $L^*$ is countable, $\mathcal T$ is countable, and therefore $M^*$ is countable. Interpret each function symbol $f$ of arity $r$ by \begin{align*} f^{M^*}([t_1],\dots,[t_r]):=[f(t_1,\dots,t_r)], \end{align*} and interpret each relation symbol $R$ of arity $r$ by \begin{align*} M^*\models R([t_1],\dots,[t_r]) \quad\Longleftrightarrow\quad R(t_1,\dots,t_r)\in\Gamma. \end{align*} The equality axioms contained in first-order logic ensure that these interpretations are well-defined with respect to $\sim$. The Henkin term model truth lemma, proved by induction on formulas, gives: for every $L^*$-formula $\alpha(u_1,\dots,u_r)$ and every closed $L^*$-term tuple $(t_1,\dots,t_r)$, \begin{align*} M^*\models \alpha([t_1],\dots,[t_r]) \quad\Longleftrightarrow\quad \alpha(t_1,\dots,t_r)\in\Gamma. \end{align*} The atomic cases are the definitions of the interpretation, the Boolean cases use completeness of $\Gamma$, and the existential case uses the Henkin property. In the existential step, if $\exists z\,\beta(z,t)\in\Gamma$, then the Henkin property gives a closed term $s$ such that $\beta(s,t)\in\Gamma$, and the induction hypothesis gives \begin{align*} M^*\models \beta([s],[t]). \end{align*} Thus $M^*\models\exists z\,\beta(z,[t])$. The converse existential implication follows from the induction hypothesis applied to a witnessing closed term. Since $T\subseteq\Gamma$, the reduct $M$ of $M^*$ to the original language $L$ satisfies $T$. The underlying set of $M$ is still countable. [/step]

[step:Use the avoidance requirements to show that every type is omitted] Fix $i\in\mathbb N$ and a tuple $a\in M^{|x_i|}$. Because $M$ is the reduct of the term model $M^*$, every component of $a$ is represented by a closed $L^*$-term. Thus there is a closed $L^*$-term tuple $t$ of length $|x_i|$ such that \begin{align*} a=[t]. \end{align*} The avoidance requirement for the pair $(i,t)$ appears in the construction, so for some formula $\varphi(x_i)\in p_i$ we added \begin{align*} \neg\varphi(t) \end{align*} to $\Gamma$. By the truth lemma, \begin{align*} M^*\models \neg\varphi([t]). \end{align*} Since $\varphi$ is an $L$-formula, satisfaction of $\varphi$ is unchanged when passing from the expanded structure $M^*$ to its $L$-reduct $M$. Hence \begin{align*} M\models \neg\varphi(a). \end{align*} Therefore $a$ does not realize $p_i$. Since $i$ and $a$ were arbitrary, $M$ omits every type $p_i$. [/step]