[proofplan] We inspect the term model produced by the [Model Existence Lemma](/theorems/1486) and show that its underlying carrier is countable. The carrier is the quotient of the set of closed terms of an extended language $\bar{L}$ by a provable-equality equivalence relation. Three cardinality facts suffice: (i) a countable language admits only countably many formulas, (ii) the Henkin extension $\bar{L} = \bigcup_{n \in \mathbb{N}} L_n$ adds only countably many witness constants at each stage and involves only countably many stages, so $\bar{L}$ is countable, (iii) the set of closed terms built from a countable signature is countable, hence so is its quotient. Countability of the carrier then transfers to the structure $A$. [/proofplan] [step:Recall the Henkin construction produces a term model whose carrier is a quotient of closed terms of the extended language] By the [Model Existence Lemma](/theorems/1486), from a consistent theory $S$ in a language $L$ one constructs a structure \begin{align*} A = \operatorname{CT}(\bar{L}) / \sim, \end{align*} where $\operatorname{CT}(\bar{L})$ denotes the set of closed terms of the Henkin-extended language $\bar{L}$, and $\sim$ is the equivalence relation \begin{align*} t_1 \sim t_2 \iff \bar{S} \vdash t_1 = t_2, \end{align*} with $\bar{S}$ the maximal consistent Henkin extension of $S$ in $\bar{L}$. The carrier of $A$ is the quotient set $\operatorname{CT}(\bar{L}) / \sim$, so it suffices to prove $\operatorname{CT}(\bar{L})$ is countable. [guided] Let us recall precisely what the Model Existence Lemma gives us. Starting from a consistent theory $S$ in language $L$, the Henkin construction proceeds in two coordinated steps: we enlarge the language and we enlarge the theory. At each stage $n$, every existential sentence $(\exists x)\,\varphi(x)$ currently provable gets a new **witness constant** $c_{\varphi}$ along with the axiom $(\exists x)\,\varphi(x) \Rightarrow \varphi(c_\varphi)$. Iterating, we obtain a chain \begin{align*} L = L_0 \subseteq L_1 \subseteq L_2 \subseteq \cdots, \qquad \bar{L} = \bigcup_{n \in \mathbb{N}} L_n, \end{align*} and a corresponding chain of theories $S = S_0 \subseteq S_1 \subseteq \cdots \subseteq \bar{S}$. The Model Existence Lemma then extends $\bar{S}$ to a maximal consistent theory (still in $\bar{L}$) and builds the term model \begin{align*} A = \operatorname{CT}(\bar{L}) / \sim, \qquad t_1 \sim t_2 \iff \bar{S} \vdash t_1 = t_2. \end{align*} The carrier of $A$ — the set of elements of the structure — is exactly this quotient of closed terms. Our task reduces to bounding its cardinality. Since the cardinality of a quotient is at most the cardinality of the set quotiented, we only need \begin{align*} |\operatorname{CT}(\bar{L})| \le \aleph_0. \end{align*} [/guided] [/step] [step:Show that a countable language has countably many formulas and terms] Let $K$ be any countable signature (a set of constant, function, and relation symbols together with the countably many logical symbols $\neg, \wedge, \forall, =$, the variables $v_0, v_1, \ldots$, and parentheses). The set of finite strings over a countable alphabet is countable: for each $k \in \mathbb{N}$, the set of strings of length exactly $k$ is $K^k$, which is countable as a finite product of countable sets, and \begin{align*} K^{<\omega} = \bigcup_{k \in \mathbb{N}} K^k \end{align*} is a countable union of countable sets, hence countable. Terms and formulas are particular finite strings, so \begin{align*} |\operatorname{Term}(K)| \le |K^{<\omega}| = \aleph_0, \qquad |\operatorname{Form}(K)| \le \aleph_0. \end{align*} In particular the set of existential sentences of $K$ is countable. [guided] The base fact is that the collection of all finite strings over a countable alphabet $K$ is itself countable. We can see this two ways. First, algebraically: for each length $k$, the set of strings of length $k$ is the $k$-fold Cartesian product $K^k$, which is countable because a finite product of countable sets is countable (standard consequence of countable choice or explicit pairing functions). Then $K^{<\omega} = \bigcup_{k=0}^\infty K^k$ is a countable union of countable sets, hence countable. Second, combinatorially: enumerate $K = \{k_0, k_1, k_2, \ldots\}$ and map a string $(k_{i_1}, \ldots, k_{i_r})$ to the integer $\prod_{j=1}^r p_j^{i_j+1}$ where $p_j$ is the $j$-th prime; this gives an explicit injection into $\mathbb{N}$. Now terms and formulas, as defined in first-order logic, are inductively constructed finite strings over the signature plus logical symbols. So both $\operatorname{Term}(K)$ and $\operatorname{Form}(K)$ are subsets of the countable set $K^{<\omega}$ (with $K$ enlarged to include logical symbols, which are themselves countable in number), hence countable. For our purposes we need the case $K = L_n$: at each stage of the Henkin construction, the existential sentences of $L_n$ form a countable set, and therefore only countably many witness constants need to be adjoined to form $L_{n+1}$. [/guided] [/step] [step:Verify inductively that each stage $L_n$ of the Henkin hierarchy is countable] We prove by induction on $n \in \mathbb{N}$ that $L_n$ is countable. **Base case ($n = 0$):** $L_0 = L$ is countable by hypothesis. **Inductive step:** Assume $L_n$ is countable. By the previous step, the set $E_n$ of existential sentences of $L_n$ is countable. The stage $L_{n+1}$ is obtained by \begin{align*} L_{n+1} = L_n \cup \{c_\varphi : \varphi \in E_n\}, \end{align*} that is, by adjoining one fresh witness constant for each existential sentence of $L_n$. This is the union of two countable sets, hence countable. By induction, $L_n$ is countable for every $n \in \mathbb{N}$. [/step] [step:Deduce that the full extended language $\bar{L}$ is countable] The extended language is \begin{align*} \bar{L} = \bigcup_{n \in \mathbb{N}} L_n. \end{align*} This is a countable (indexed over $\mathbb{N}$) union of countable sets by the previous step, hence countable. [guided] We now combine the two countable-union facts. Each stage $L_n$ is countable (previous step), and the indexing set $\mathbb{N}$ is countable. A countable union of countable sets is countable — this is one of the standard consequences of countable choice in ZFC, provable for definable families without choice. Since the Henkin hierarchy $(L_n)_{n \in \mathbb{N}}$ is constructed by an explicit definable recursion, we have a definable family and can conclude \begin{align*} |\bar{L}| = \left|\bigcup_{n \in \mathbb{N}} L_n\right| \le \aleph_0 \cdot \aleph_0 = \aleph_0. \end{align*} Since $L \subseteq \bar{L}$ and $L$ is infinite (or at least non-empty and extended with infinitely many witness constants at the first non-trivial stage — we may assume WLOG that $\bar{L}$ is infinite, since the conclusion "countable" includes "finite"), we have $|\bar{L}| = \aleph_0$. [/guided] [/step] [step:Conclude that the term model $A$ is countable] The set of closed terms of $\bar{L}$ is a subset of the set of all terms of $\bar{L}$, so by Step 2 applied to $K = \bar{L}$: \begin{align*} |\operatorname{CT}(\bar{L})| \le |\operatorname{Term}(\bar{L})| \le \aleph_0. \end{align*} The carrier of $A$ is the quotient $\operatorname{CT}(\bar{L}) / \sim$, and the canonical surjection $\operatorname{CT}(\bar{L}) \twoheadrightarrow \operatorname{CT}(\bar{L})/\sim$ shows \begin{align*} |A| = |\operatorname{CT}(\bar{L}) / \sim| \le |\operatorname{CT}(\bar{L})| \le \aleph_0. \end{align*} Since $A$ is a model of $S$ (by the Model Existence Lemma) with countable carrier, $S$ has a countable model, as required. $\square$ [guided] Let us assemble the final estimate. The carrier of the term model $A$ is the quotient set $\operatorname{CT}(\bar{L}) / \sim$. The cardinality of a quotient set is always bounded by the cardinality of the set being quotiented, because the quotient map is a surjection. Therefore \begin{align*} |A| = |\operatorname{CT}(\bar{L})/\sim| \le |\operatorname{CT}(\bar{L})|. \end{align*} The set of closed terms of $\bar{L}$ is a subset of all terms of $\bar{L}$, and by Step 2 (with $K = \bar{L}$, which is countable by Step 4) we have \begin{align*} |\operatorname{Term}(\bar{L})| \le \aleph_0. \end{align*} Combining these estimates gives $|A| \le \aleph_0$, i.e., $A$ is countable (finite or countably infinite). The Model Existence Lemma guarantees $A \models S$. This establishes: every theory in a countable language that has a model has a countable model. Note that we do not claim $|A| = \aleph_0$ — if $S$ has only finite models (e.g., the theory of a fixed finite group), then $A$ itself may be finite, which still qualifies as countable under our convention. [/guided] [/step]