[proofplan] We prove the two implications separately. If $M$ is a countable atomic model of $T$, then every non-empty basic [open set](/page/Open%20Set) $[\varphi] \subseteq S_n(T)$ is realized in $M$ by completeness of $T$, and the realizing tuple has an isolated type because $M$ is atomic. Conversely, assuming isolated types are dense in every $S_n(T)$, we build a countable Henkin theory in a countable expansion by constants. The construction simultaneously supplies witnesses for existential formulas and forces every finite tuple from the eventual term model to satisfy an isolating formula; the resulting countable model is therefore atomic. [/proofplan]

[step:Use atomicity of a model to place an isolated type in every non-empty basic open set] Assume that $M$ is a countable atomic model of $T$. Fix an integer $n \geq 1$ and let $[\varphi] \subseteq S_n(T)$ be a non-empty basic open set, where $\varphi(x_1,\dots,x_n)$ is an $\mathcal{L}$-formula. Since $[\varphi]$ is non-empty, the theory \begin{align*} T \cup \{\exists x_1 \cdots \exists x_n\, \varphi(x_1,\dots,x_n)\} \end{align*} is consistent. Because $T$ is complete, every model of $T$ satisfies the sentence $\exists x_1 \cdots \exists x_n\, \varphi(x_1,\dots,x_n)$; in particular, there is a tuple $a = (a_1,\dots,a_n) \in M^n$ such that \begin{align*} M \models \varphi(a_1,\dots,a_n). \end{align*} Let $p := \operatorname{tp}^M(a_1,\dots,a_n)$ be the complete $\mathcal{L}$-type of this tuple over the empty set. Since $M$ is atomic, $p$ is isolated. Also $\varphi \in p$, so $p \in [\varphi]$. Therefore every non-empty basic open subset of $S_n(T)$ contains an isolated point, and the isolated types are dense in $S_n(T)$. [/step]

[step:Prepare a countable Henkin expansion and enumerate the requirements]Assume now that, for every $n \geq 1$, the isolated points are dense in $S_n(T)$. Let $\mathcal{C} = \{c_i : i \in \mathbb{N}\}$ be a [countable set](/page/Countable%20Set) of new constant symbols, disjoint from $\mathcal{L}$, and let \begin{align*} \mathcal{L}_{\mathcal{C}} := \mathcal{L} \cup \mathcal{C}. \end{align*} Since $\mathcal{L}$ and $\mathcal{C}$ are countable, the set of $\mathcal{L}_{\mathcal{C}}$-sentences is countable. We enumerate all pairs \begin{align*} (\exists y\, \psi_i(y,z_i), d_i) \qquad i \in \mathbb{N}, \end{align*} where $\psi_i(y,z_i)$ is an $\mathcal{L}$-formula, $z_i = (z_{i,1},\dots,z_{i,m_i})$ is a finite tuple of variables, and $d_i = (d_{i,1},\dots,d_{i,m_i})$ is a tuple of constants from $\mathcal{C}$ of the same length. These are the Henkin witness requirements. We also enumerate all pairs \begin{align*} (\theta_j(w_j), e_j) \qquad j \in \mathbb{N}, \end{align*} where $\theta_j(w_j)$ is an $\mathcal{L}$-formula, $w_j = (w_{j,1},\dots,w_{j,k_j})$ is a finite tuple of variables with $k_j \geq 1$, and $e_j = (e_{j,1},\dots,e_{j,k_j})$ is a tuple of constants from $\mathcal{C}$ of the same length. These are the atomicity requirements for finite tuples of constants.[/step]

[guided]We enlarge the language only by countably many constants because the desired model must be countable. Let \begin{align*} \mathcal{C} = \{c_i : i \in \mathbb{N}\} \end{align*} be a countable set of new constant symbols disjoint from $\mathcal{L}$, and define the expanded language \begin{align*} \mathcal{L}_{\mathcal{C}} := \mathcal{L} \cup \mathcal{C}. \end{align*} Since both $\mathcal{L}$ and $\mathcal{C}$ are countable, the set of $\mathcal{L}_{\mathcal{C}}$-sentences is countable. The constants serve two purposes. First, they provide Henkin witnesses, so that the final complete theory has a model whose elements are represented by closed terms and, in fact, by named constants. Second, every finite tuple of constants will eventually be forced to satisfy an isolating formula, which is what will make the final model atomic. We enumerate all pairs \begin{align*} (\exists y\, \psi_i(y,z_i), d_i) \qquad i \in \mathbb{N}, \end{align*} where $\psi_i(y,z_i)$ is an $\mathcal{L}$-formula, $z_i = (z_{i,1},\dots,z_{i,m_i})$ is a finite tuple of variables, and $d_i = (d_{i,1},\dots,d_{i,m_i})$ is a tuple of constants from $\mathcal{C}$ of the same length. This enumeration is possible because there are only countably many $\mathcal{L}$-formulas in finitely many variables and only countably many finite tuples of constants from $\mathcal{C}$. These are the Henkin witness requirements: if the current theory permits \begin{align*} \exists y\, \psi_i(y,d_i), \end{align*} then the construction adds a fresh constant witnessing it. We also enumerate all pairs \begin{align*} (\theta_j(w_j), e_j) \qquad j \in \mathbb{N}, \end{align*} where $\theta_j(w_j)$ is an $\mathcal{L}$-formula, $w_j = (w_{j,1},\dots,w_{j,k_j})$ is a finite tuple of variables with $k_j \geq 1$, and $e_j = (e_{j,1},\dots,e_{j,k_j})$ is a tuple of constants from $\mathcal{C}$ of the same length. This enumeration is possible for the same countability reason. These are the atomicity requirements: if the current theory permits \begin{align*} \theta_j(e_j), \end{align*} then the construction strengthens the information about $e_j$ to an isolated complete type extending that formula. This second scheduling is the extra ingredient beyond the ordinary Henkin construction. A Henkin construction alone gives a countable model of $T$, but not necessarily an atomic one. Density of isolated types is used precisely when a finite tuple has some consistent finite description: we replace that description by an isolating formula for a complete type extending it.[/guided]

[step:Build a consistent Henkin theory that isolates every finite tuple of constants] We construct an increasing sequence \begin{align*} \Gamma_0 \subseteq \Gamma_1 \subseteq \Gamma_2 \subseteq \cdots \end{align*} of finite sets of $\mathcal{L}_{\mathcal{C}}$-sentences such that $T \cup \Gamma_s$ is consistent for every $s \in \mathbb{N}$. Set $\Gamma_0 := \varnothing$. At stage $s$, handle the $s$-th Henkin requirement and the $s$-th atomicity requirement. First consider the Henkin requirement $(\exists y\,\psi_s(y,z_s),d_s)$. If \begin{align*} T \cup \Gamma_s \cup \{\exists y\, \psi_s(y,d_s)\} \end{align*} is consistent, choose a constant $c \in \mathcal{C}$ not occurring in $\Gamma_s$, $d_s$, or $\psi_s$, and add the sentence \begin{align*} \exists y\,\psi_s(y,d_s) \to \psi_s(c,d_s). \end{align*} The usual fresh-constant argument preserves consistency: if adding this implication made the theory inconsistent, then $T \cup \Gamma_s \cup \{\exists y\,\psi_s(y,d_s)\}$ would force $\neg \psi_s(c,d_s)$ for a fresh constant $c$, hence would force $\forall y\,\neg \psi_s(y,d_s)$, contradicting the displayed consistency. If the displayed theory is inconsistent, add nothing for this requirement. Next consider the atomicity requirement $(\theta_s(w_s),e_s)$. If \begin{align*} T \cup \Gamma_s \cup \{\theta_s(e_s)\} \end{align*} is inconsistent, add nothing. Otherwise, let $A_s$ be the finite set of constants occurring in $\Gamma_s$ together with the entries of $e_s$, and write \begin{align*} A_s = (a_{s,1},\dots,a_{s,r_s}) \end{align*} as a tuple without repetitions. Let $u_s = (u_{s,1},\dots,u_{s,r_s})$ be a tuple of variables of the same length. Since $\Gamma_s$ is finite, form the conjunction of all sentences in $\Gamma_s$; if $\Gamma_s = \varnothing$, use the tautological formula $u_{s,1}=u_{s,1}$. Define $\gamma_s(u_s)$ to be the $\mathcal{L}$-formula obtained from that conjunction by replacing each occurrence of the constant $a_{s,\ell}$ by the corresponding variable $u_{s,\ell}$. Thus the sentence $\gamma_s(A_s)$ is logically equivalent over first-order logic to the conjunction of the finite set $\Gamma_s$. Let $\eta_s(u_s)$ be the conjunction of $\gamma_s(u_s)$ with the formula $\theta_s(e_s)$ rewritten in the variables $u_s$ according to the positions of the entries of $e_s$ inside $A_s$. The consistency of $T \cup \Gamma_s \cup \{\theta_s(e_s)\}$ says exactly that the basic open set $[\eta_s] \subseteq S_{r_s}(T)$ is non-empty. By the density hypothesis in $S_{r_s}(T)$, there is an isolated type $p_s \in S_{r_s}(T)$ with $\eta_s \in p_s$. Choose an $\mathcal{L}$-formula $\alpha_s(u_s) \in p_s$ isolating $p_s$. Add the sentence \begin{align*} \alpha_s(A_s). \end{align*} Since $\alpha_s \in p_s$ and $\eta_s \in p_s$, the theory \begin{align*} T \cup \{\eta_s(u_s) \wedge \alpha_s(u_s)\} \end{align*} is consistent; therefore replacing the variables $u_s$ by the constants $A_s$ shows that \begin{align*} T \cup \Gamma_s \cup \{\theta_s(e_s),\alpha_s(A_s)\} \end{align*} is consistent. Hence consistency is preserved. Let $\Gamma_{s+1}$ be the finite set obtained after these additions. [/step]

[step:Pass to a countable Henkin model of the completed diagram] Let \begin{align*} \Gamma := \bigcup_{s \in \mathbb{N}} \Gamma_s. \end{align*} Every finite subset of $T \cup \Gamma$ is contained in $T \cup \Gamma_s$ for some $s$, so $T \cup \Gamma$ is consistent by the [Compactness Theorem](/page/Compactness%20Theorem). Extend $T \cup \Gamma$ to a complete consistent $\mathcal{L}_{\mathcal{C}}$-theory $\Delta$ by the [Lindenbaum Extension Lemma](/page/Lindenbaum%20Extension%20Lemma). We verify that $\Delta$ has the Henkin property. Suppose $\exists y\,\psi(y,d) \in \Delta$, where $\psi(y,z)$ is an $\mathcal{L}$-formula and $d$ is a finite tuple of constants from $\mathcal{C}$ of the same length as $z$. Let $s$ be the index at which the Henkin requirement $(\exists y\,\psi(y,z),d)$ appears in the enumeration. Since $\Delta$ extends $T \cup \Gamma$ and contains $\exists y\,\psi(y,d)$, the finite-stage theory \begin{align*} T \cup \Gamma_s \cup \{\exists y\,\psi(y,d)\} \end{align*} is consistent. Therefore the construction at stage $s$ added a Henkin implication \begin{align*} \exists y\,\psi(y,d) \to \psi(c,d) \end{align*} for some fresh constant $c \in \mathcal{C}$. This implication belongs to $\Gamma \subseteq \Delta$, and completeness of first-order consequence inside the theory $\Delta$ gives $\psi(c,d) \in \Delta$. Hence every existential sentence in $\Delta$ has a constant witness in $\Delta$. Let $M_{\mathcal{C}}$ be the term model of $\Delta$. Its universe is the set of closed $\mathcal{L}_{\mathcal{C}}$-terms modulo the [equivalence relation](/page/Equivalence%20Relation) \begin{align*} t \sim_{\Delta} t' \quad \Longleftrightarrow \quad \Delta \vdash t = t'. \end{align*} The interpretation of function and relation symbols is the usual interpretation induced by $\Delta$: function symbols act on equivalence classes of closed terms by applying the function symbol to representatives, and relation symbols are interpreted by membership of the corresponding atomic sentence in $\Delta$. These interpretations are well-defined because $\Delta$ is complete, consistent, and contains the first-order equality axioms, so provably equal representatives may be substituted in atomic formulas. Since $\mathcal{L}_{\mathcal{C}}$ is countable, the set of closed terms is countable, and therefore $M_{\mathcal{C}}$ is countable. By the [Henkin Model Theorem](/page/Henkin%20Model%20Theorem), the truth lemma holds: \begin{align*} M_{\mathcal{C}} \models \sigma \quad \Longleftrightarrow \quad \sigma \in \Delta \end{align*} for every $\mathcal{L}_{\mathcal{C}}$-sentence $\sigma$. In particular, since $T \subseteq \Delta$, the $\mathcal{L}$-reduct $M$ of $M_{\mathcal{C}}$ is a countable model of $T$. [/step]

[step:Show that every realized finite type in the Henkin model is isolated]Let $b = (b_1,\dots,b_n) \in M^n$ be a finite tuple. Choose closed $\mathcal{L}_{\mathcal{C}}$-terms $t_1,\dots,t_n$ representing $b_1,\dots,b_n$ in the term model. By the Henkin property applied to the formulas defining the values of closed terms, there are constants $e_1,\dots,e_n \in \mathcal{C}$ such that \begin{align*} M_{\mathcal{C}} \models t_i = e_i \end{align*} for each $1 \leq i \leq n$. Thus $b$ has the same $\mathcal{L}$-type as the tuple $e = (e_1,\dots,e_n)$ interpreted in $M_{\mathcal{C}}$. Consider the atomicity requirement indexed by a pair $(\theta(w),e)$ such that $\theta(w)$ is any $\mathcal{L}$-formula true of $e$ in $M_{\mathcal{C}}$. Since $M_{\mathcal{C}} \models \theta(e)$, the sentence $\theta(e)$ belongs to $\Delta$. The construction considered this pair at some finite stage. At that stage, the consistency test for $T \cup \Gamma_s \cup \{\theta(e)\}$ succeeded because this theory is contained in the consistent theory $\Delta$. Therefore the construction added a formula \begin{align*} \alpha(A) \end{align*} where $A$ is a finite tuple of constants containing $e$, and $\alpha$ isolates a complete type over $T$ extending the finite information then imposed on $A$. We now project the isolated type of the larger tuple $A$ to the subtuple represented by $e$. Let $u=(u_1,\dots,u_r)$ be a tuple of variables corresponding to $A=(A_1,\dots,A_r)$. Let $w=(w_1,\dots,w_n)$ be a tuple of variables corresponding to $e=(e_1,\dots,e_n)$, and let $\pi:\{1,\dots,n\} \to \{1,\dots,r\}$ be the function such that $e_i = A_{\pi(i)}$ as constant symbols for each $1 \leq i \leq n$. Define the $\mathcal{L}$-formula \begin{align*} \beta(w) := \exists u_1 \cdots \exists u_r\,\left(\alpha(u) \wedge \bigwedge_{i=1}^n w_i = u_{\pi(i)}\right). \end{align*} This definition retains all equalities and inequalities decided by the isolated type of the full tuple $A$, including equalities among distinct constants that may hold in the term model. Since $M_{\mathcal{C}} \models \alpha(A)$ and $e_i=A_{\pi(i)}$ as interpreted elements of $M_{\mathcal{C}}$, we have $M_{\mathcal{C}} \models \beta(e)$; hence $T \cup \{\beta(w)\}$ is consistent. We prove that $\beta$ isolates the complete $n$-type realized by $e$. Let $\rho(w)$ be an arbitrary $\mathcal{L}$-formula. Define the $\mathcal{L}$-formula $\rho_{\pi}(u)$ by \begin{align*} \rho_{\pi}(u_1,\dots,u_r) := \rho(u_{\pi(1)},\dots,u_{\pi(n)}). \end{align*} Because $\alpha(u)$ isolates a complete type over $T$, the complete type isolated by $\alpha$ decides $\rho_{\pi}$, so either \begin{align*} T \vdash \alpha(u) \to \rho_{\pi}(u) \end{align*} or \begin{align*} T \vdash \alpha(u) \to \neg \rho_{\pi}(u). \end{align*} In the first case, first-order logic gives \begin{align*} T \vdash \beta(w) \to \rho(w), \end{align*} because any witness $u$ to $\beta(w)$ satisfies $w_i=u_{\pi(i)}$ for every $i$. In the second case, the same substitution by equality gives \begin{align*} T \vdash \beta(w) \to \neg \rho(w). \end{align*} Thus $\beta$ is consistent with $T$ and decides every $\mathcal{L}$-formula in the variables $w$, so $\beta$ isolates $\operatorname{tp}^M(e)$. Since $b$ and $e$ have the same $\mathcal{L}$-type, $\operatorname{tp}^M(b)$ is isolated.[/step]

[guided]We must prove atomicity for arbitrary finite tuples from the model, not only for constants. In the Henkin term model every element is represented by a closed term. The Henkin witnesses let us replace each closed term by a constant with the same value in the model: if $t$ is a closed term, the formula $\exists y\, (y = t)$ is true, so the Henkin construction supplies a constant $c$ with $c = t$ in the completed theory. Hence any tuple $b = (b_1,\dots,b_n)$ has the same $\mathcal{L}$-type as some tuple of constants $e = (e_1,\dots,e_n)$. Now fix such a tuple of constants $e$. The construction did not merely witness existential formulas; it also scheduled every possible finite condition $\theta(e)$ on this tuple. If $\theta(e)$ is true in the final model, then $\theta(e) \in \Delta$ by the truth lemma. When the pair $(\theta,e)$ appeared in the construction, the theory \begin{align*} T \cup \Gamma_s \cup \{\theta(e)\} \end{align*} was consistent, because it is contained in the final consistent theory $\Delta$. Therefore the construction invoked density of isolated types and chose an isolated complete type extending the finite information about the larger tuple $A$ of constants then in play. It added an isolating formula \begin{align*} \alpha(A) \end{align*} to the diagram. The tuple $A$ may contain constants besides $e$, and distinct constants in $A$ may be identified in the final term model. Therefore we do not merely record the repetitions visible in the written tuple $e$; instead, we project the isolated type of the entire tuple $A$. Write $A=(A_1,\dots,A_r)$. Let $u=(u_1,\dots,u_r)$ be variables corresponding to $A$, let $w=(w_1,\dots,w_n)$ be variables corresponding to $e$, and let $\pi:\{1,\dots,n\} \to \{1,\dots,r\}$ be the function such that $e_i=A_{\pi(i)}$ as constant symbols for each $1 \leq i \leq n$. Define \begin{align*} \beta(w) := \exists u_1 \cdots \exists u_r\,\left(\alpha(u) \wedge \bigwedge_{i=1}^n w_i = u_{\pi(i)}\right). \end{align*} This formula keeps the whole isolated description $\alpha(u)$ and then asks that $w$ be the indicated subtuple of a realization of that description. Any extra equalities among coordinates of $A$, including equalities involving auxiliary coordinates not displayed in $e$, are still controlled because they are decided by the complete type isolated by $\alpha$. Because $\alpha(A)$ holds in $M_{\mathcal{C}}$ and the interpreted tuple $e$ satisfies $e_i=A_{\pi(i)}$ for each $i$, the tuple $A$ itself witnesses the existential quantifiers in $\beta(e)$. Hence $M_{\mathcal{C}} \models \beta(e)$, and $T \cup \{\beta(w)\}$ is consistent. To see that $\beta$ isolates the type of $e$, let $\rho(w)$ be any $\mathcal{L}$-formula. We transfer $\rho$ to a formula in the full tuple variables by defining \begin{align*} \rho_{\pi}(u_1,\dots,u_r) := \rho(u_{\pi(1)},\dots,u_{\pi(n)}). \end{align*} Since $\alpha(u)$ isolates a complete type of the tuple $A$, it decides $\rho_{\pi}(u)$. Thus either \begin{align*} T \vdash \alpha(u) \to \rho_{\pi}(u) \end{align*} or \begin{align*} T \vdash \alpha(u) \to \neg \rho_{\pi}(u). \end{align*} If the first alternative holds and $w$ satisfies $\beta(w)$, choose witnesses $u$ with $\alpha(u)$ and $w_i=u_{\pi(i)}$ for all $i$. By equality substitution, $\rho_{\pi}(u)$ is equivalent to $\rho(w)$, so \begin{align*} T \vdash \beta(w) \to \rho(w). \end{align*} If the second alternative holds, the same equality substitution gives \begin{align*} T \vdash \beta(w) \to \neg \rho(w). \end{align*} Therefore $\beta$ is consistent with $T$ and decides every $\mathcal{L}$-formula in the variables $w$, so it isolates the complete type of $e$. Since $b$ has the same $\mathcal{L}$-type as $e$, the tuple $b$ also realizes an isolated type.[/guided]

[step:Conclude that the constructed model is countable and atomic] The $\mathcal{L}$-reduct $M$ of the Henkin model $M_{\mathcal{C}}$ is countable and satisfies $T$. The previous step shows that every finite tuple from $M$ realizes an isolated complete type over $T$. Therefore $M$ is an atomic model of $T$. Combining this construction with the forward implication proves that $T$ has a countable atomic model if and only if, for every $n \geq 1$, the isolated types are dense in $S_n(T)$. [/step]