[proofplan] We pass to the expanded language $L(A)$, so that “over $A$” becomes “over the empty set.” Since $T$ is countable and totally transcendental and $A$ is countable, the expanded theory $T_A$ is still countable and totally transcendental. The key model-theoretic input is that, in a countable totally transcendental theory, isolated types are dense in every finite Stone space; this permits a Henkin construction of a countable atomic model of $T_A$. Atomicity gives primeness by recursively embedding finite tuples using the formulas isolating their complete types, and uniqueness follows by applying primeness in both directions and then using atomic back-and-forth over the named constants. [/proofplan]

[step:Replace the base set by constants in the language]Let $L(A)$ denote the language obtained from $L$ by adjoining a constant symbol $c_a$ for each $a \in A$. Let $T_A := \operatorname{Th}_{L(A)}(\mathfrak{C}, a)_{a \in A}$ be the complete $L(A)$-theory of the expansion of $\mathfrak{C}$ in which $c_a$ is interpreted by $a$. Since $L$ is countable and $A$ is countable, the language $L(A)$ is countable. Since formulas in $L(A)$ are exactly formulas of $L$ with parameters from $A$, the ranks and type-counting assertions used in total transcendence are already among the parameter-definable ranks and types of the original theory. Hence total transcendence is preserved under naming the elements of $A$, and $T_A$ is totally transcendental. A model of $T_A$ is precisely a model of $T$ equipped with an interpretation of the constants $c_a$ as a copy of the parameter set $A$ satisfying the same complete diagram over $A$. Thus a prime model of $T_A$ is the same thing as a model prime over $A$ in the original language.[/step]

[guided]The purpose of naming the elements of $A$ is to remove the base from the notation. Instead of repeatedly saying “types over $A$,” we work in the expanded language $L(A)$ and speak about types over $\varnothing$. Formally, for each $a \in A$ we add a constant symbol $c_a$, and we define \begin{align*} T_A := \operatorname{Th}_{L(A)}(\mathfrak{C}, a)_{a \in A}. \end{align*} This is a complete theory because it is the complete theory of a fixed expanded structure. The language remains countable because it is obtained from the countable language $L$ by adjoining countably many constant symbols. Total transcendence is also unchanged by naming parameters. Every $L(A)$-formula is an $L$-formula with parameters from $A$, and total transcendence of $T$ controls types and Morley ranks over arbitrary parameter sets, not only over the empty set. Thus the definable sets and ranks appearing in $T_A$ are already present in the original parameter-definable setting. A model $M_A \models T_A$ has an underlying $L$-structure $M \models T$, and the interpretations of the constants $c_a$ give distinguished elements corresponding to $a \in A$. Therefore an elementary embedding of $L(A)$-structures is exactly an elementary embedding of the underlying $L$-structures that fixes every named element of $A$. So proving that $T_A$ has a prime model proves the existence of a model prime over $A$, and uniqueness of the prime model of $T_A$ gives uniqueness over $A$.[/guided]

[step:Use density of isolated types in finite Stone spaces] We use the following external model-theoretic input: in a countable totally transcendental complete theory, for every natural number $n \geq 1$, the isolated types are dense in the Stone space $S_n(\varnothing)$ of complete $n$-types over $\varnothing$; equivalently, every consistent formula $\varphi(x_1,\dots,x_n)$ is extended by some formula $\psi(x_1,\dots,x_n)$ which isolates a complete type over $\varnothing$. This is the isolated-types density theorem for countable [totally transcendental theories](/page/Totally%20Transcendental%20Theory), used here as a named standard input. The countability hypothesis is essential for the use made below: it makes the relevant language countable, so the Henkin requirements can be enumerated and the density of isolated types can be applied successively along a countable construction. The theory $T_A$ is countable and totally transcendental by the previous step, so the isolated-types density theorem applies to $T_A$. Hence, whenever $\varphi(x)$ is a consistent $L(A)$-formula in a finite tuple of variables $x$, there is an $L(A)$-formula $\psi(x)$ such that $T_A \models \forall x(\psi(x) \implies \varphi(x))$ and $\psi(x)$ isolates a complete type in $S_{|x|}^{T_A}(\varnothing)$. [/step]

[step:Build a countable atomic model by a Henkin construction]Work inside a sufficiently saturated and strongly homogeneous model $\mathfrak{U} \models T_A$. Enumerate all $L(A)$-formulas with one distinguished existential variable block as $(\exists y_i\,\varphi_i(y_i,z_i))_{i \in \mathbb{N}}$, where $y_i$ and $z_i$ are finite tuples of variables. Let $\mathbb{N}_{\geq 1}:=\{1,2,3,\dots\}$, and let \begin{align*} \rho: \mathbb{N} \to \{(i,s) : i \in \mathbb{N},\ s \in \mathbb{N}_{\geq 1}^{|z_i|}\} \end{align*} be a surjection such that every pair $(i,s)$ occurs infinitely many times, where $s=(s_1,\dots,s_{|z_i|})$ records which previously chosen elements are to be substituted for the variables $z_i$. We construct finite tuples $d_m=(d_{m,1},\dots,d_{m,\ell_m})$ from $\mathfrak{U}$ and formulas $\delta_m(u_1,\dots,u_{\ell_m})$ such that $\delta_m$ isolates $\operatorname{tp}^{\mathfrak{U}}_{L(A)}(d_m/\varnothing)$. Start with the empty tuple $d_0$ and the sentence $\delta_0 := (\top)$, which isolates the unique complete $0$-type. At stage $m$, write $\rho(m)=(i,s)$ with $s=(s_1,\dots,s_{|z_i|})$. If some $s_j>\ell_m$, set $d_{m+1}:=d_m$ and $\delta_{m+1}:=\delta_m$. Otherwise define the parameter tuple \begin{align*} d_m^s := (d_{m,s_1},\dots,d_{m,s_{|z_i|}}). \end{align*} If $\mathfrak{U} \models \neg \exists y_i\,\varphi_i(y_i,d_m^s)$, again set $d_{m+1}:=d_m$ and $\delta_{m+1}:=\delta_m$. If $\mathfrak{U} \models \exists y_i\,\varphi_i(y_i,d_m^s)$, then the formula \begin{align*} \delta_m(u) \wedge \varphi_i(y,u^s) \end{align*} is consistent, where $u=(u_1,\dots,u_{\ell_m})$ and $u^s=(u_{s_1},\dots,u_{s_{|z_i|}})$. By density of isolated types, choose an $L(A)$-formula $\theta_m(u,y)$ isolating a complete type over $\varnothing$ and satisfying \begin{align*} T_A \models \forall u\,\forall y\bigl(\theta_m(u,y) \implies \delta_m(u) \wedge \varphi_i(y,u^s)\bigr). \end{align*} Let $(u^*,e^*)$ realize $\theta_m(u,y)$ in $\mathfrak{U}$. Since $\theta_m(u,y)$ implies $\delta_m(u)$, the tuple $u^*$ realizes the isolated type of $d_m$. Hence $u^*$ and $d_m$ have the same complete type over $\varnothing$. Strong homogeneity of $\mathfrak{U}$ gives an automorphism $\sigma$ of $\mathfrak{U}$ with $\sigma(u^*)=d_m$. Define $e_m:=\sigma(e^*)$. Then $\mathfrak{U} \models \theta_m(d_m,e_m)$, so $e_m$ witnesses $\varphi_i(y_i,d_m^s)$. Set $d_{m+1}$ to be the tuple obtained by appending the coordinates of $e_m$ to $d_m$, and set $\delta_{m+1}:=\theta_m$ after viewing its variables as the variables for the enlarged tuple. Let $D := \bigcup_{m \in \mathbb{N}} \{d_{m,1},\dots,d_{m,\ell_m}\}$, and let $M$ be the $L(A)$-substructure of $\mathfrak{U}$ generated by $D$. The scheduling by $\rho$ gives the Henkin witness property first for parameters from $D$. Indeed, if $\mathfrak{U} \models \exists y_i\,\varphi_i(y_i,a)$ for a parameter tuple $a$ from $D$, choose $m_0$ such that every coordinate of $a$ appears among $d_{m_0,1},\dots,d_{m_0,\ell_{m_0}}$, and let $s$ record those coordinate indices. Since $(i,s)$ occurs infinitely often in $\rho$, some stage $m\geq m_0$ processes $(i,s)$ and adds a witness from $D$. This implies the required witness property for parameters from $M$, not only from $D$. If $b$ is a finite tuple from $M$, then each coordinate of $b$ is the value of an $L(A)$-term in finitely many elements of $D$. Thus an existential instance $\exists y\,\varphi(y,b)$ over $M$ can be rewritten as an $L(A)$-formula $\exists y\,\varphi(y,\tau(a))$ with a finite parameter tuple $a$ from $D$ and a tuple of $L(A)$-terms $\tau$. The witness constructed for this rewritten instance lies in $D \subset M$, so the Tarski-Vaught criterion gives $M \preccurlyeq \mathfrak{U}$, and therefore $M \models T_A$. Every finite tuple from $D$ is contained in some $d_m$, and $\delta_m$ isolates the complete type of $d_m$ over $\varnothing$. If $r$ is a finite tuple from $M$, then each coordinate of $r$ is the value of an $L(A)$-term in finitely many elements of $D$, so $r$ is obtained from some $d_m$ by applying a finite tuple of terms. The image of an isolated complete type under a tuple of terms is again isolated: if the terms are $\tau(u)$, then the formula $\exists u(\delta_m(u) \wedge x=\tau(u))$ isolates the complete type of $\tau(d_m)$. Hence every finite tuple from $M$ realizes an isolated complete type over $\varnothing$, so $M$ is atomic.[/step]

[guided]We now build the model and fix two technical points at the same time. First, every existential formula must be revisited with every finite tuple of parameters that appears later in the construction. Second, when density gives an isolating formula for an enlarged tuple, we must arrange that the old coordinates are the already chosen tuple, rather than merely some other realization of the same old type. Work inside a sufficiently saturated and strongly homogeneous model $\mathfrak{U} \models T_A$. Because $L(A)$ is countable, the set of formulas is countable. Enumerate all existential patterns as \begin{align*} (\exists y_i\,\varphi_i(y_i,z_i))_{i \in \mathbb{N}}, \end{align*} where $y_i$ is the tuple to be witnessed and $z_i$ is the tuple of parameter variables. To make sure that later parameters are not missed, we do not process each formula only once. Instead let $\mathbb{N}_{\geq 1}:=\{1,2,3,\dots\}$ and choose a surjection \begin{align*} \rho: \mathbb{N} \to \{(i,s) : i \in \mathbb{N},\ s \in \mathbb{N}_{\geq 1}^{|z_i|}\} \end{align*} such that every pair $(i,s)$ occurs infinitely many times. Here $s=(s_1,\dots,s_{|z_i|})$ is a positive index tuple telling us to substitute the chosen elements with those indices for the variables $z_i$. Repetition is the Henkin scheduling device: if the relevant parameters do not exist the first time a pair appears, the same pair appears again after they have been added. We construct finite tuples \begin{align*} d_m=(d_{m,1},\dots,d_{m,\ell_m}) \end{align*} and formulas $\delta_m(u_1,\dots,u_{\ell_m})$ such that $\delta_m$ isolates the complete type $\operatorname{tp}^{\mathfrak{U}}_{L(A)}(d_m/\varnothing)$. Begin with the empty tuple $d_0$ and the sentence $\delta_0 := (\top)$, which isolates the unique complete $0$-type. At stage $m$, write $\rho(m)=(i,s)$ with $s=(s_1,\dots,s_{|z_i|})$. If some $s_j>\ell_m$, then the requested parameter has not yet been chosen, so this occurrence cannot define an instance. We set $d_{m+1}:=d_m$ and $\delta_{m+1}:=\delta_m$. If all indices exist, define the parameter tuple \begin{align*} d_m^s := (d_{m,s_1},\dots,d_{m,s_{|z_i|}}). \end{align*} If $\mathfrak{U} \models \neg \exists y_i\,\varphi_i(y_i,d_m^s)$, there is no witness to add for this instance, and again we set $d_{m+1}:=d_m$ and $\delta_{m+1}:=\delta_m$. Now suppose $\mathfrak{U} \models \exists y_i\,\varphi_i(y_i,d_m^s)$. We want to add a witness while preserving the invariant that the enlarged finite tuple has isolated type. The formula \begin{align*} \delta_m(u) \wedge \varphi_i(y,u^s) \end{align*} is consistent, where $u=(u_1,\dots,u_{\ell_m})$ and $u^s=(u_{s_1},\dots,u_{s_{|z_i|}})$, because it is realized by $u=d_m$ together with some witness for $\varphi_i(y_i,d_m^s)$ in $\mathfrak{U}$. By density of isolated types in the finite Stone space of the variables $(u,y)$, choose a formula $\theta_m(u,y)$ which isolates a complete type over $\varnothing$ and strengthens this consistent formula: \begin{align*} T_A \models \forall u\,\forall y\bigl(\theta_m(u,y) \implies \delta_m(u) \wedge \varphi_i(y,u^s)\bigr). \end{align*} The density theorem gives a realization $(u^*,e^*)$ of $\theta_m(u,y)$ in $\mathfrak{U}$. At this point the old coordinates are $u^*$, not necessarily our actual tuple $d_m$. The reason this causes no problem is that $\theta_m(u,y)$ implies $\delta_m(u)$, and $\delta_m$ isolates the complete type of $d_m$. Therefore $u^*$ and $d_m$ realize the same complete type over $\varnothing$. Strong homogeneity of $\mathfrak{U}$ gives an automorphism $\sigma$ of $\mathfrak{U}$ such that $\sigma(u^*)=d_m$. Define $e_m:=\sigma(e^*)$. Applying $\sigma$ to the truth of $\theta_m(u^*,e^*)$ gives \begin{align*} \mathfrak{U} \models \theta_m(d_m,e_m). \end{align*} Since $\theta_m$ implies $\varphi_i(y,u^s)$, the tuple $e_m$ witnesses $\varphi_i(y_i,d_m^s)$. We set $d_{m+1}$ to be the tuple obtained by appending the coordinates of $e_m$ to $d_m$, and we set $\delta_{m+1}:=\theta_m$ with variables renamed to match the enlarged tuple. Let \begin{align*} D := \bigcup_{m \in \mathbb{N}} \{d_{m,1},\dots,d_{m,\ell_m}\}, \end{align*} and let $M$ be the $L(A)$-substructure of $\mathfrak{U}$ generated by $D$. The scheduling now proves the Henkin witness property first for parameters from $D$. Suppose $\mathfrak{U} \models \exists y_i\,\varphi_i(y_i,a)$ for a tuple $a$ from $D$. Choose $m_0$ large enough that all coordinates of $a$ occur in $d_{m_0}$, and let $s$ be the tuple of their indices in $d_{m_0}$. Because the pair $(i,s)$ occurs infinitely many times in $\rho$, some stage $m\geq m_0$ processes that same instance. At that stage the construction adds a witness from $D$. We now pass from parameters in $D$ to parameters in the generated substructure $M$. If $b$ is a finite tuple from $M$, then each coordinate of $b$ has the form $\tau_j(a)$ for some finite tuple $a$ from $D$ and some $L(A)$-term $\tau_j$. Therefore an existential formula $\exists y\,\varphi(y,b)$ over $M$ is the same instance as the formula $\exists y\,\varphi(y,\tau(a))$ over parameters from $D$, where $\tau$ is the tuple of terms producing $b$. If this instance is realized in $\mathfrak{U}$, the previous paragraph supplies a witness from $D$, hence from $M$. Thus every existential formula over parameters from $M$ that is realized in $\mathfrak{U}$ has a witness in $M$. By the Tarski-Vaught criterion, $M \preccurlyeq \mathfrak{U}$, so $M \models T_A$. Finally, take a finite tuple $r$ from $M$. Each coordinate of $r$ is obtained by applying an $L(A)$-term to finitely many elements of $D$, so there is some $d_m$ and a finite tuple of terms $\tau(u)$ such that $r=\tau(d_m)$. Since $\delta_m(u)$ isolates the complete type of $d_m$, the formula \begin{align*} \exists u\bigl(\delta_m(u) \wedge x=\tau(u)\bigr) \end{align*} isolates the complete type of $r$. Thus every finite tuple from $M$ realizes an isolated type over $\varnothing$, which is exactly atomicity of $M$.[/guided]

[step:Embed the atomic model into any model of the expanded theory] Let $N \models T_A$. We construct an elementary embedding $f: M \to N$. Enumerate $M$ as $(m_i)_{i \in \mathbb{N}}$. We define finite partial elementary maps $f_k$ on $\{m_1,\dots,m_k\}$ by induction. Suppose $f_k$ has been defined and is elementary on its finite domain. Let $a_k := (m_1,\dots,m_k,m_{k+1})$. Since $M$ is atomic, the complete type $\operatorname{tp}^{M}_{L(A)}(a_k/\varnothing)$ is isolated by some formula $\alpha_k(x_1,\dots,x_k,x_{k+1})$. The tuple $(f_k(m_1),\dots,f_k(m_k))$ realizes the restriction of this isolated type to the first $k$ coordinates. Since $N \models T_A$ and the existential sentence \begin{align*} \exists x_{k+1}\,\alpha_k(f_k(m_1),\dots,f_k(m_k),x_{k+1}) \end{align*} is forced by that restriction, choose $n_{k+1} \in N$ realizing it. Extend $f_k$ by setting $f_{k+1}(m_{k+1}) := n_{k+1}$. The union \begin{align*} f := \bigcup_{k \in \mathbb{N}} f_k \end{align*} is elementary because every finite tuple from $M$ is sent to a tuple satisfying the same complete isolated type. Since the constants $c_a$ belong to the language $L(A)$, every $L(A)$-elementary embedding fixes their interpretations. Thus the underlying $L$-embedding fixes $A$ pointwise. Therefore $M$ is prime over $A$. [/step]

[step:Show prime models over the base are countable atomic and run a back-and-forth] Let $M_0$ and $M_1$ be two models prime over $A$. In the expanded language $L(A)$, both are prime models of $T_A$. Let $M$ be the countable atomic model of $T_A$ constructed above. By primeness of $M_0$, there is an $L(A)$-elementary embedding \begin{align*} e_0: M_0 \to M. \end{align*} Since $M$ is countable, the injectivity of $e_0$ implies that $M_0$ is countable. Moreover $M_0$ is atomic. Indeed, let $a$ be a finite tuple from $M_0$. The tuple $e_0(a)$ is a finite tuple from the atomic model $M$, so its complete type over $\varnothing$ is isolated by some $L(A)$-formula $\alpha(x)$. Since $e_0$ is elementary, $M_0 \models \alpha(a)$; since $\alpha$ isolates a complete type of $T_A$, the complete type of $a$ over $\varnothing$ is isolated by $\alpha$. Thus every finite tuple from $M_0$ has isolated complete type over $\varnothing$. The same argument, using an elementary embedding of $M_1$ into $M$, shows that $M_1$ is countable and atomic. Enumerate the underlying sets as $(a_i)_{i \in \mathbb{N}}$ for $M_0$ and $(b_i)_{i \in \mathbb{N}}$ for $M_1$. We construct an increasing sequence of finite partial elementary bijections between $M_0$ and $M_1$. Suppose $g$ is a finite partial elementary bijection with domain tuple $a$ and image tuple $b=g(a)$. For the forth step, let $a_* \in M_0$. Since $M_0$ is atomic, choose an $L(A)$-formula $\beta(x,y)$ isolating the complete type of $(a,a_*)$ over $\varnothing$. The tuple $b$ realizes the restriction of this isolated type to the variables $x$, because $g$ is partial elementary. Hence $T_A$ entails the existential requirement \begin{align*} \exists y\,\beta(b,y). \end{align*} Since $M_1 \models T_A$, choose $b_* \in M_1$ with $M_1 \models \beta(b,b_*)$, and extend $g$ by sending $a_*$ to $b_*$. The formula $\beta$ isolates the complete type of the enlarged tuple, so the extension is again partial elementary. The back step is identical with $M_0$ and $M_1$ interchanged: for a new element $b_* \in M_1$, use atomicity of $M_1$ to isolate the type of the enlarged range tuple and realize the corresponding existential formula in $M_0$. Alternating forth steps for the elements $a_i$ and back steps for the elements $b_i$ yields an $L(A)$-elementary bijection \begin{align*} h: M_0 \to M_1. \end{align*} Thus $h$ is an $L(A)$-isomorphism. Since $h$ is an isomorphism in the language $L(A)$, it preserves the interpretation of every constant symbol $c_a$. Passing back to the original language, $h$ fixes every element of $A$ pointwise. Hence the prime model over $A$ is unique up to isomorphism over $A$. [/step]