[proofplan] We compare three incarnations of the same finiteness phenomenon: finitely many complete types, finitely many definable subsets, and finitely many automorphism orbits. The implication from finite type spaces to $\omega$-categoricity is proved by isolating every finite type and running a back-and-forth argument between countable models. The converse uses the countable omitting-types construction: if some $S_n(T)$ were infinite, it would contain a non-isolated type, and one countable model could realize that type while another omits it. The automorphism formulation then follows because, in the unique countable model, two tuples have the same complete type exactly when an automorphism sends one to the other. [/proofplan]

[step:Show that finite type spaces make every finite type isolated]Assume that $S_n(T)$ is finite for every $n \geq 1$. Fix $n \geq 1$ and $p \in S_n(T)$. Write \begin{align*} S_n(T) = \{p, q_1,\dots,q_m\}. \end{align*} For each $i \in \{1,\dots,m\}$, choose an $L$-formula $\varphi_i(x_1,\dots,x_n) \in p \setminus q_i$, which is possible because $p \neq q_i$ and complete types decide every formula. Define \begin{align*} \theta_p(x_1,\dots,x_n) := \bigwedge_{i=1}^m \varphi_i(x_1,\dots,x_n). \end{align*} Then $\theta_p \in p$, while $\theta_p \notin q_i$ for every $i$. Hence the clopen set of types containing $\theta_p$ is exactly $\{p\}$, so $\theta_p$ isolates $p$.[/step]

[guided]The goal is to turn topological finiteness into a syntactic isolating formula. Fix a complete type $p \in S_n(T)$. Since $S_n(T)$ is finite, every other complete $n$-type can be listed as \begin{align*} q_1,\dots,q_m. \end{align*} For each $q_i$, the types $p$ and $q_i$ are distinct complete sets of formulas. Therefore there is some formula $\varphi_i(x_1,\dots,x_n)$ such that $\varphi_i \in p$ and $\varphi_i \notin q_i$. Completeness is used here: if two complete types contained exactly the same formulas, they would be equal. Now combine these separating formulas into one formula: \begin{align*} \theta_p(x_1,\dots,x_n) := \bigwedge_{i=1}^m \varphi_i(x_1,\dots,x_n). \end{align*} Because each $\varphi_i$ belongs to $p$, the conjunction $\theta_p$ belongs to $p$. If $q_i$ is any other type on the list, then $q_i$ omits $\varphi_i$, so $q_i$ also omits the stronger formula $\theta_p$. Thus no type except $p$ contains $\theta_p$. This proves that $\theta_p$ isolates $p$: among all complete $n$-types over $T$, it singles out exactly $p$.[/guided]

[step:Use isolated finite types to build a back-and-forth isomorphism] Let $A \models T$ and $B \models T$ be countable. We construct an isomorphism $A \to B$ by back-and-forth. A finite partial map $f: \bar{a} \mapsto \bar{b}$ is called elementary if $\bar{a}$ and $\bar{b}$ satisfy the same $L$-formulas over $\varnothing$, equivalently $\operatorname{tp}^A(\bar{a}) = \operatorname{tp}^B(\bar{b})$. Suppose $f: \bar{a} \mapsto \bar{b}$ is elementary and $c \in A$. Let $p(x_1,\dots,x_k,y) := \operatorname{tp}^A(\bar{a},c)$, where $k$ is the length of $\bar{a}$. By the previous step, choose a formula $\theta_p(x_1,\dots,x_k,y)$ isolating $p$. Since $A \models \exists y\,\theta_p(\bar{a},y)$, the formula $\exists y\,\theta_p(x_1,\dots,x_k,y)$ belongs to $\operatorname{tp}^A(\bar{a})$. Because $f$ is elementary, $B \models \exists y\,\theta_p(\bar{b},y)$. Choose $d \in B$ such that $B \models \theta_p(\bar{b},d)$. Since $\theta_p$ isolates $p$, we have \begin{align*} \operatorname{tp}^B(\bar{b},d) = p = \operatorname{tp}^A(\bar{a},c). \end{align*} Thus $f \cup \{(c,d)\}$ is elementary. For the range-extension step, suppose $f: \bar{a} \mapsto \bar{b}$ is elementary and $d \in B$. Let \begin{align*} r(x_1,\dots,x_k,y) := \operatorname{tp}^B(\bar{b},d), \end{align*} where $k$ is the length of $\bar{b}$. By the previous step, choose a formula $\theta_r(x_1,\dots,x_k,y)$ isolating $r$. Since $B \models \exists y\,\theta_r(\bar{b},y)$, the formula $\exists y\,\theta_r(x_1,\dots,x_k,y)$ belongs to $\operatorname{tp}^B(\bar{b})$. Because $f$ is elementary, $A \models \exists y\,\theta_r(\bar{a},y)$. Choose $c \in A$ such that $A \models \theta_r(\bar{a},c)$. Since $\theta_r$ isolates $r$, we have \begin{align*} \operatorname{tp}^A(\bar{a},c) = r = \operatorname{tp}^B(\bar{b},d). \end{align*} Thus $f \cup \{(c,d)\}$ is elementary and contains $d$ in its range. Enumerate the underlying sets as $A = \{a_1,a_2,\dots\}$ and $B = \{b_1,b_2,\dots\}$. Starting from the empty elementary map, alternate domain extensions for $a_i$ and range extensions for $b_i$. The union of the resulting increasing chain of finite elementary partial maps is a bijection $F: A \to B$. Since every finite tuple and its image have the same complete type, $F$ preserves and reflects every atomic formula and every relation symbol, and also preserves function symbols by applying elementary equivalence to formulas of the form $z = h(x_1,\dots,x_r)$. Hence $F$ is an $L$-isomorphism. Therefore $T$ is $\omega$-categorical. [/step]

[step:Use omitting types to force finite Stone spaces from $\omega$-categoricity] Assume that $T$ is $\omega$-categorical. We prove that each $S_n(T)$ is finite. Suppose, toward a contradiction, that $S_n(T)$ is infinite for some $n \geq 1$. Since $L$ is countable, the Boolean algebra of $L$-formulas in variables $x_1,\dots,x_n$ modulo $T$ is countable, so $S_n(T)$ is a compact [Hausdorff space](/page/Hausdorff%20Space) with a countable clopen basis. An infinite [compact space](/page/Compact%20Space) cannot have every point isolated: if every point were isolated, compactness would make the open cover by singleton sets admit a finite subcover. Hence choose a non-isolated type $p \in S_n(T)$. We use the standard countable Henkin omitting-types construction for one non-isolated type. It yields a countable model $N \models T$ omitting $p$, meaning no tuple $\bar{c} \in N^n$ realizes $p$. Also, let $L(c_1,\dots,c_n)$ be the language obtained from $L$ by adding new constant symbols $c_1,\dots,c_n$. The $L(c_1,\dots,c_n)$-theory \begin{align*} T \cup \{\varphi(c_1,\dots,c_n) : \varphi \in p\} \end{align*} is finitely satisfiable, because every finite subset of $p$ is consistent with $T$. By the [Compactness Theorem](/theorems/???), it has a model $M^+$. Let $M_0$ be the $L$-reduct of $M^+$, and let $\bar{c}^{M^+} := (c_1^{M^+},\dots,c_n^{M^+}) \in M_0^n$ be the interpretation of the new constants. Since $L$ is countable and $\bar{c}^{M^+}$ is finite, the downward [Löwenheim-Skolem Theorem](/theorems/???) gives a countable elementary substructure $M \preccurlyeq M_0$ containing the entries of $\bar{c}^{M^+}$. Elementarity implies $M \models T$, and the tuple $\bar{c}^{M^+} \in M^n$ realizes $p$ in $M$. Thus $M$ and $N$ are countable models of $T$ with different realized $n$-type spectra: $p$ is realized in $M$ and omitted in $N$. They cannot be isomorphic. This contradicts $\omega$-categoricity. Therefore $S_n(T)$ is finite for every $n \geq 1$. [/step]

[step:Identify finite type spaces with finitely many formulas modulo $T$] Fix $n \geq 1$. Let $\mathcal{B}_n(T)$ be the Boolean algebra of $L$-formulas with free variables among $x_1,\dots,x_n$, modulo $T$-equivalence. Each formula $\varphi(x_1,\dots,x_n)$ determines the clopen subset \begin{align*} [\varphi] := \{p \in S_n(T) : \varphi \in p\} \end{align*} of the Stone space $S_n(T)$. The assignment $\varphi \mapsto [\varphi]$ is a Boolean algebra isomorphism from $\mathcal{B}_n(T)$ onto the Boolean algebra of clopen subsets of $S_n(T)$. Injectivity follows because $[\varphi] = [\psi]$ exactly says that every complete $n$-type over $T$ decides $\varphi \leftrightarrow \psi$ positively, equivalently $T \models \forall x_1\dots\forall x_n\,(\varphi \leftrightarrow \psi)$. Surjectivity follows because the sets $[\varphi]$ form a clopen basis for $S_n(T)$, and every clopen subset $C \subset S_n(T)$ is compact; covering $C$ by basic clopens contained in $C$ and taking a finite subcover expresses $C$ as a finite union of formula clopens, hence as $[\varphi_1 \vee \cdots \vee \varphi_k]$ for suitable formulas $\varphi_1,\dots,\varphi_k$. If $S_n(T)$ is finite, then it has only finitely many subsets, hence only finitely many clopen subsets, so $\mathcal{B}_n(T)$ is finite. Conversely, if $\mathcal{B}_n(T)$ is finite, then only finitely many clopen subsets are available. Distinct complete types are separated by some formula, so distinct points of $S_n(T)$ are separated by clopen sets. Therefore $S_n(T)$ has at most as many points as there are ultrafilters on the finite Boolean algebra $\mathcal{B}_n(T)$, hence is finite. This proves the equivalence of conditions 2 and 3. [/step]

[step:Relate complete types in the unique countable model to automorphism orbits] Assume that $T$ is $\omega$-categorical, and let $M \models T$ be its countable model. Fix $n \geq 1$ and tuples $\bar{a},\bar{b} \in M^n$. We claim that $\bar{a}$ and $\bar{b}$ lie in the same $\operatorname{Aut}(M)$-orbit if and only if \begin{align*} \operatorname{tp}^M(\bar{a}) = \operatorname{tp}^M(\bar{b}). \end{align*} The forward direction holds because automorphisms preserve all first-order formulas. For the reverse direction, start with the finite elementary partial map $\bar{a} \mapsto \bar{b}$. We spell out the two extension moves inside $M$. Suppose $g: \bar{u} \mapsto \bar{v}$ is a finite elementary partial map extending $\bar{a} \mapsto \bar{b}$, and let $c \in M$. Let \begin{align*} p(x_1,\dots,x_k,y) := \operatorname{tp}^M(\bar{u},c), \end{align*} where $k$ is the length of $\bar{u}$. Since $T$ is $\omega$-categorical, condition 2 has already been proved, so $S_{k+1}(T)$ is finite; hence the first step supplies a formula $\theta_p(x_1,\dots,x_k,y)$ isolating $p$. From $M \models \exists y\,\theta_p(\bar{u},y)$ and elementarity of $g$, we get $M \models \exists y\,\theta_p(\bar{v},y)$. Choose $d \in M$ with $M \models \theta_p(\bar{v},d)$. Since $\theta_p$ isolates $p$, \begin{align*} \operatorname{tp}^M(\bar{v},d) = p = \operatorname{tp}^M(\bar{u},c), \end{align*} so $g \cup \{(c,d)\}$ is elementary. The range-extension move is analogous but with the roles of domain and range reversed: for $d \in M$, isolate $\operatorname{tp}^M(\bar{v},d)$ by a formula $\theta_r$, use $M \models \exists y\,\theta_r(\bar{v},y)$ and elementarity of $g$ to find $c \in M$ with $M \models \theta_r(\bar{u},c)$, and conclude that $g \cup \{(c,d)\}$ is elementary. Enumerating the [countable set](/page/Countable%20Set) $M$ and alternating these two moves gives an elementary bijection $F: M \to M$ extending $\bar{a} \mapsto \bar{b}$. As in the earlier back-and-forth construction, preservation of atomic formulas and function-symbol graphs makes $F$ an $L$-automorphism of $M$. Thus an automorphism sends $\bar{a}$ to $\bar{b}$. By condition 2, $S_n(T)$ is finite. Since every tuple in $M^n$ realizes one complete $n$-type, and each complete $n$-type determines at most one orbit by the claim, $\operatorname{Aut}(M)$ has only finitely many orbits on $M^n$. Thus condition 4 holds. [/step]

[step:Recover finite formula classes from an oligomorphic automorphism group] Assume that $M \models T$ is countable and that $\operatorname{Aut}(M)$ is oligomorphic. Fix $n \geq 1$. Let \begin{align*} M^n = O_1 \cup \cdots \cup O_r \end{align*} be the finite decomposition of $M^n$ into $\operatorname{Aut}(M)$-orbits. For any $L$-formula $\varphi(x_1,\dots,x_n)$, its interpretation \begin{align*} \varphi(M) := \{\bar{a} \in M^n : M \models \varphi(\bar{a})\} \end{align*} is invariant under $\operatorname{Aut}(M)$. Hence $\varphi(M)$ is a union of some of the finitely many orbits $O_1,\dots,O_r$. There are only finitely many such unions. If two formulas $\varphi$ and $\psi$ define the same subset of $M^n$, then \begin{align*} M \models \forall x_1\dots \forall x_n\,(\varphi(x_1,\dots,x_n) \leftrightarrow \psi(x_1,\dots,x_n)). \end{align*} Since $M \models T$ and $T$ is complete, this sentence belongs to $T$, so $\varphi$ and $\psi$ are equivalent modulo $T$. Therefore only finitely many formulas in variables $x_1,\dots,x_n$ exist modulo $T$-equivalence. Since $n$ was arbitrary, condition 3 holds. [/step]

[step:Combine the implications] We have proved that condition 2 implies condition 1, and that condition 1 implies condition 2. We have also proved that conditions 2 and 3 are equivalent. Finally, condition 1 implies condition 4 through the orbit-type correspondence in the unique countable model, while condition 4 implies condition 3 because formulas define unions of finitely many automorphism orbits. Therefore all four stated conditions are equivalent. [/step]