[proofplan] We build an isomorphism by the usual back-and-forth construction. At each finite stage we maintain a finite partial elementary bijection $f_s: A_s \to B_s$ between finite subsets of $M$ and $N$. Atomicity supplies an isolated type for an enlarged tuple, and completeness of the current partial elementary map transfers the corresponding existential sentence to the other model, giving the needed extension. Alternating forth steps from $M$ and back steps from $N$ makes the final map total and surjective, and preservation of all formulas on finite tuples makes it an isomorphism. [/proofplan]

[step:Enumerate the two countable models and state the invariant] Let $(m_i)_{i \in \mathbb{N}}$ enumerate the underlying set of $M$, and let $(n_i)_{i \in \mathbb{N}}$ enumerate the underlying set of $N$. We shall construct, by induction on $s \in \mathbb{N} \cup \{0\}$, finite subsets $A_s \subset M$ and $B_s \subset N$ and a bijection \begin{align*} f_s: A_s &\to B_s \end{align*} such that $f_s$ is partial elementary: for every integer $r \geq 1$, every tuple $(a_1,\dots,a_r) \in A_s^r$, and every $L$-formula $\psi(x_1,\dots,x_r)$, \begin{align*} M \models \psi(a_1,\dots,a_r) \quad \Longleftrightarrow \quad N \models \psi(f_s(a_1),\dots,f_s(a_r)). \end{align*} We also require $f_s \subset f_{s+1}$ for every $s \in \mathbb{N} \cup \{0\}$. Start with $A_0 = \varnothing$, $B_0 = \varnothing$, and $f_0: \varnothing \to \varnothing$ the empty map. This map is partial elementary because there are no tuples from its domain. [/step]

[step:Extend the partial elementary map to include the next element of $M$]Assume $f_s: A_s \to B_s$ has been constructed. Let $i_s \in \mathbb{N}$ be the least index such that $m_{i_s} \notin A_s$, if such an index exists. If no such index exists, set $f_{s+1/2} := f_s$, $A_{s+1/2}:=A_s$, and $B_{s+1/2}:=B_s$. Suppose such an index exists. List $A_s$ as a tuple $(a_1,\dots,a_r)$ with no repetitions, where $r \geq 0$, and define the corresponding tuple in $N$ by \begin{align*} c_j := f_s(a_j) \qquad \text{for } 1 \leq j \leq r. \end{align*} Since $M$ is atomic, the complete type \begin{align*} \operatorname{tp}^M(a_1,\dots,a_r,m_{i_s}/\varnothing) \end{align*} is isolated by some $L$-formula $\varphi(x_1,\dots,x_r,y)$. Thus \begin{align*} M \models \varphi(a_1,\dots,a_r,m_{i_s}). \end{align*} In particular, \begin{align*} M \models \exists y\,\varphi(a_1,\dots,a_r,y). \end{align*} We now transfer this existential assertion to $N$. If $r \geq 1$, this follows from partial elementarity of $f_s$ applied to the formula $\exists y\,\varphi(x_1,\dots,x_r,y)$. If $r=0$, then $\exists y\,\varphi(y)$ is a sentence true in $M$; since $M \models T$, $N \models T$, and $T$ is complete, the same sentence is true in $N$. Hence in all cases \begin{align*} N \models \exists y\,\varphi(c_1,\dots,c_r,y). \end{align*} Choose $d \in N$ such that \begin{align*} N \models \varphi(c_1,\dots,c_r,d). \end{align*} Define \begin{align*} A_{s+1/2} &:= A_s \cup \{m_{i_s}\},\\ B_{s+1/2} &:= B_s \cup \{d\}, \end{align*} and define \begin{align*} f_{s+1/2}: A_{s+1/2} &\to B_{s+1/2} \end{align*} by $f_{s+1/2}|_{A_s}=f_s$ and $f_{s+1/2}(m_{i_s})=d$. The element $d$ is not already in $B_s$. Indeed, if $d=c_j$ for some $1 \leq j \leq r$, then $N \models y=x_j$ at the tuple $(c_1,\dots,c_r,d)$. Since $\varphi$ isolates the complete type of $(a_1,\dots,a_r,m_{i_s})$, this would imply \begin{align*} M \models m_{i_s}=a_j, \end{align*} contradicting $m_{i_s}\notin A_s$. Hence $f_{s+1/2}$ is a bijection. It remains to check partial elementarity. Let $\theta(x_1,\dots,x_r,y)$ be any $L$-formula. Because $\varphi$ isolates $\operatorname{tp}^M(a_1,\dots,a_r,m_{i_s}/\varnothing)$, either \begin{align*} T \models \forall x_1\cdots \forall x_r \forall y\,(\varphi(x_1,\dots,x_r,y) \to \theta(x_1,\dots,x_r,y)) \end{align*} or \begin{align*} T \models \forall x_1\cdots \forall x_r \forall y\,(\varphi(x_1,\dots,x_r,y) \to \neg\theta(x_1,\dots,x_r,y)). \end{align*} Since both $M$ and $N$ are models of $T$ and both tuples satisfy $\varphi$, we get \begin{align*} M \models \theta(a_1,\dots,a_r,m_{i_s}) \quad \Longleftrightarrow \quad N \models \theta(c_1,\dots,c_r,d). \end{align*} Allowing repeated variables in $\theta$ gives preservation for every tuple from $A_{s+1/2}$, so $f_{s+1/2}$ is partial elementary.[/step]

[guided]We want to add the next unused element of $M$ while keeping the map elementary on its finite domain. Let $i_s$ be the least index with $m_{i_s} \notin A_s$. If there is no such index, no forth extension is needed, and we keep the same map. Assume $m_{i_s}$ exists. Write the finite domain $A_s$ as an ordered tuple $(a_1,\dots,a_r)$ with no repetitions. The existing map sends this tuple to \begin{align*} (c_1,\dots,c_r) := (f_s(a_1),\dots,f_s(a_r)). \end{align*} The key point is that atomicity gives control over the complete type of the enlarged tuple. Since $M$ is atomic, the complete type \begin{align*} \operatorname{tp}^M(a_1,\dots,a_r,m_{i_s}/\varnothing) \end{align*} is isolated by an $L$-formula $\varphi(x_1,\dots,x_r,y)$. This means two things. First, \begin{align*} M \models \varphi(a_1,\dots,a_r,m_{i_s}). \end{align*} Second, any tuple in any model of $T$ satisfying $\varphi$ realizes exactly the same complete type over $\varnothing$ as $(a_1,\dots,a_r,m_{i_s})$. From $M \models \varphi(a_1,\dots,a_r,m_{i_s})$ we get \begin{align*} M \models \exists y\,\varphi(a_1,\dots,a_r,y). \end{align*} Now we must justify why the same existential assertion holds in $N$. If $r \geq 1$, the formula $\exists y\,\varphi(x_1,\dots,x_r,y)$ has free variables $x_1,\dots,x_r$, and the current map $f_s$ is partial elementary, so it transfers the truth of this formula from $(a_1,\dots,a_r)$ in $M$ to $(c_1,\dots,c_r)$ in $N$. If $r=0$, there is no tuple on which partial elementarity can be applied under our definition; instead $\exists y\,\varphi(y)$ is a sentence. Since $M \models T$, $N \models T$, and $T$ is complete, every sentence true in one model of $T$ is true in the other. Therefore in both cases \begin{align*} N \models \exists y\,\varphi(c_1,\dots,c_r,y). \end{align*} Choose $d \in N$ such that \begin{align*} N \models \varphi(c_1,\dots,c_r,d). \end{align*} Now define the extended map by sending the new element $m_{i_s}$ to $d$ and keeping the old values: \begin{align*} A_{s+1/2} &:= A_s \cup \{m_{i_s}\},\\ B_{s+1/2} &:= B_s \cup \{d\},\\ f_{s+1/2}|_{A_s} &= f_s,\\ f_{s+1/2}(m_{i_s}) &= d. \end{align*} We must check that this is actually a bijection, so $d$ must not already lie in $B_s$. Suppose instead that $d=c_j$ for some $1 \leq j \leq r$. Then the tuple $(c_1,\dots,c_r,d)$ satisfies the equality formula $y=x_j$. Since $\varphi$ isolates the complete type of $(a_1,\dots,a_r,m_{i_s})$, every formula true of a tuple satisfying $\varphi$ in a model of $T$ is true of $(a_1,\dots,a_r,m_{i_s})$ in $M$. Hence \begin{align*} M \models m_{i_s}=a_j, \end{align*} which contradicts the choice $m_{i_s}\notin A_s$. Thus $d \notin B_s$, and $f_{s+1/2}$ is a bijection from $A_{s+1/2}$ onto $B_{s+1/2}$. Finally we verify elementarity of the extension. Let $\theta(x_1,\dots,x_r,y)$ be any $L$-formula. Because $\varphi$ isolates the complete type of $(a_1,\dots,a_r,m_{i_s})$, the complete theory $T$ decides whether every realization of $\varphi$ satisfies $\theta$ or every realization of $\varphi$ satisfies $\neg\theta$. Thus either \begin{align*} T \models \forall x_1\cdots \forall x_r \forall y\,(\varphi(x_1,\dots,x_r,y) \to \theta(x_1,\dots,x_r,y)) \end{align*} or \begin{align*} T \models \forall x_1\cdots \forall x_r \forall y\,(\varphi(x_1,\dots,x_r,y) \to \neg\theta(x_1,\dots,x_r,y)). \end{align*} Since both $M$ and $N$ satisfy $T$, and since both enlarged tuples satisfy $\varphi$, we conclude \begin{align*} M \models \theta(a_1,\dots,a_r,m_{i_s}) \quad \Longleftrightarrow \quad N \models \theta(c_1,\dots,c_r,d). \end{align*} This proves preservation for formulas in the displayed tuple. Any tuple from the finite set $A_{s+1/2}$ can be described by repeating and reordering variables among $x_1,\dots,x_r,y$, so the same argument gives preservation for every finite tuple from $A_{s+1/2}$. Therefore $f_{s+1/2}$ is partial elementary.[/guided]

[step:Extend the partial elementary map to include the next element of $N$] Let $j_s \in \mathbb{N}$ be the least index such that $n_{j_s} \notin B_{s+1/2}$, if such an index exists. If no such index exists, define $A_{s+1}:=A_{s+1/2}$, $B_{s+1}:=B_{s+1/2}$, and $f_{s+1}:=f_{s+1/2}$. Suppose such an index exists. List $B_{s+1/2}$ as a tuple $(b_1,\dots,b_q)$ with no repetitions, where $q \geq 0$, and define the corresponding tuple in $M$ by \begin{align*} e_k := f_{s+1/2}^{-1}(b_k) \qquad \text{for } 1 \leq k \leq q. \end{align*} Since $N$ is atomic, the complete type \begin{align*} \operatorname{tp}^N(b_1,\dots,b_q,n_{j_s}/\varnothing) \end{align*} is isolated by some $L$-formula $\rho(z_1,\dots,z_q,w)$. Thus \begin{align*} N \models \rho(b_1,\dots,b_q,n_{j_s}), \end{align*} and hence \begin{align*} N \models \exists w\,\rho(b_1,\dots,b_q,w). \end{align*} We transfer this existential assertion to $M$. If $q \geq 1$, this follows from partial elementarity of $f_{s+1/2}$ applied to the formula $\exists w\,\rho(z_1,\dots,z_q,w)$. If $q=0$, then $\exists w\,\rho(w)$ is a sentence true in $N$; since $M \models T$, $N \models T$, and $T$ is complete, the same sentence is true in $M$. Therefore in all cases \begin{align*} M \models \exists w\,\rho(e_1,\dots,e_q,w). \end{align*} Choose $a \in M$ such that \begin{align*} M \models \rho(e_1,\dots,e_q,a). \end{align*} Define \begin{align*} A_{s+1} &:= A_{s+1/2} \cup \{a\},\\ B_{s+1} &:= B_{s+1/2} \cup \{n_{j_s}\}, \end{align*} and define \begin{align*} f_{s+1}: A_{s+1} &\to B_{s+1} \end{align*} by $f_{s+1}|_{A_{s+1/2}}=f_{s+1/2}$ and $f_{s+1}(a)=n_{j_s}$. The element $a$ is not already in $A_{s+1/2}$. Indeed, if $a=e_k$ for some $1 \leq k \leq q$, then $M \models w=z_k$ at the tuple $(e_1,\dots,e_q,a)$. Since $\rho$ isolates the complete type of $(b_1,\dots,b_q,n_{j_s})$, this implies \begin{align*} N \models n_{j_s}=b_k, \end{align*} contradicting $n_{j_s}\notin B_{s+1/2}$. Hence $f_{s+1}$ is a bijection. It remains to check partial elementarity. Let $\eta(z_1,\dots,z_q,w)$ be any $L$-formula. Because $\rho$ isolates $\operatorname{tp}^N(b_1,\dots,b_q,n_{j_s}/\varnothing)$, either \begin{align*} T \models \forall z_1\cdots \forall z_q \forall w\,(\rho(z_1,\dots,z_q,w) \to \eta(z_1,\dots,z_q,w)) \end{align*} or \begin{align*} T \models \forall z_1\cdots \forall z_q \forall w\,(\rho(z_1,\dots,z_q,w) \to \neg\eta(z_1,\dots,z_q,w)). \end{align*} Since both $M$ and $N$ are models of $T$ and both tuples satisfy $\rho$, we get \begin{align*} M \models \eta(e_1,\dots,e_q,a) \quad \Longleftrightarrow \quad N \models \eta(b_1,\dots,b_q,n_{j_s}). \end{align*} Allowing repeated variables in $\eta$ gives preservation for every tuple from $A_{s+1}$, so $f_{s+1}$ is partial elementary. [/step]

[step:Take the union of the finite partial elementary maps] Define \begin{align*} f: M &\to N \end{align*} by \begin{align*} f(x) := f_s(x) \end{align*} for any $s \in \mathbb{N} \cup \{0\}$ such that $x \in A_s$. This is well-defined because the sequence is increasing: if $x \in A_s \cap A_t$, then $f_s(x)=f_t(x)$ after passing to a later stage. The forth steps ensure every $m_i$ eventually belongs to some $A_s$, so $\operatorname{dom}(f)=M$. The back steps ensure every $n_j$ eventually belongs to some $B_s$, so $\operatorname{Range}(f)=N$. Since every $f_s$ is injective and the maps are nested, $f$ is injective. Hence $f$ is a bijection from $M$ onto $N$. [/step]

[step:Verify that the resulting bijection is an isomorphism] Let $r \geq 1$, let $(x_1,\dots,x_r) \in M^r$, and let $\psi(x_1,\dots,x_r)$ be any $L$-formula. Since the tuple is finite, there exists $s \in \mathbb{N}$ such that $x_1,\dots,x_r \in A_s$. Because $f_s$ is partial elementary, \begin{align*} M \models \psi(x_1,\dots,x_r) \quad \Longleftrightarrow \quad N \models \psi(f_s(x_1),\dots,f_s(x_r)). \end{align*} By definition of $f$, this is \begin{align*} M \models \psi(x_1,\dots,x_r) \quad \Longleftrightarrow \quad N \models \psi(f(x_1),\dots,f(x_r)). \end{align*} Thus $f$ preserves every $L$-formula on every finite tuple. In particular, taking $\psi$ to be each atomic formula of $L$, $f$ preserves all function, relation, and constant symbols of the language. Therefore $f: M \to N$ is an $L$-isomorphism. The final assertion follows by applying the result just proved to two countable prime models, using the standard fact that countable prime models of a complete theory in a countable language are atomic; this is the [Atomicity of Countable Prime Models](/theorems/???). This proves the theorem. [/step]