[proofplan] We prove compactness by the finite-subcover criterion, reducing arbitrary open covers to covers by basic clopen formula sets. The central point is that a family of basic closed sets with the finite intersection property corresponds exactly to a set of formulas whose every finite subset is satisfiable. First-order compactness then produces a realization of all formulas simultaneously, and a maximal consistent extension of its formula set gives a complete type lying in the desired intersection. [/proofplan] [step:Translate finite intersections of basic closed sets into finite satisfiability] Let $x = (x_1,\dots,x_n)$ be the tuple of object variables. For each $L(A)$-formula $\varphi(x)$, recall that \begin{align*} [\varphi(x)] := \{p \in S_n(A) : \varphi(x) \in p\}. \end{align*} Because every complete type decides each $L(A)$-formula, the complement of $[\varphi(x)]$ in $S_n(A)$ is $[\neg \varphi(x)]$. Hence each $[\varphi(x)]$ is clopen. Let $I$ be an index set, and let $(\varphi_i(x))_{i \in I}$ be a family of $L(A)$-formulas such that the family of basic closed sets $([\varphi_i(x)])_{i \in I}$ has the finite intersection property. This means that for every finite subset $F \subseteq I$, \begin{align*} \bigcap_{i \in F} [\varphi_i(x)] \neq \varnothing. \end{align*} Equivalently, for every finite $F \subseteq I$, there exists $p_F \in S_n(A)$ such that $\varphi_i(x) \in p_F$ for all $i \in F$. Since each $p_F$ belongs to $S_n(A)$, it is a complete $n$-type consistent with the full parameter theory of the monster model expanded by constants for $A$. Therefore the finite set of formulas $\{\varphi_i(x) : i \in F\}$ is satisfiable together with every finite fragment of that full parameter theory. [/step] [step:Use first-order compactness to realize all formulas simultaneously] Let $L(A)$ be the language obtained from $L$ by adding a constant symbol $c_a$ for each $a \in A$. Let $\operatorname{Th}_A(\mathfrak{C})$ denote the set of all $L(A)$-sentences true in the expansion of $\mathfrak{C}$ that interprets $c_a$ as $a$ for each $a \in A$. Define the $L(A)$-theory with free tuple $x$ by \begin{align*} \Sigma := \operatorname{Th}_A(\mathfrak{C}) \cup \{\varphi_i(x) : i \in I\}. \end{align*} Every finite subset of $\Sigma$ is satisfiable: the finitely many formulas involving $x$ are contained in $\{\varphi_i(x) : i \in F\}$ for some finite $F \subseteq I$, and the previous step shows that these formulas are satisfiable together with every finite fragment of $\operatorname{Th}_A(\mathfrak{C})$. By the [First-Order Compactness Theorem](/theorems/???), applied to this finitely satisfiable set of $L(A)$-formulas, there exist an $L(A)$-structure $\mathfrak{M}$ and a tuple $b = (b_1,\dots,b_n) \in M^n$ such that \begin{align*} \mathfrak{M} \models \operatorname{Th}_A(\mathfrak{C}) \end{align*} and \begin{align*} \mathfrak{M} \models \varphi_i(b) \end{align*} for every $i \in I$. [guided] The finite intersection property has now been converted into a model-theoretic compactness problem. The formulas $\varphi_i(x)$ are not sentences because they contain the free tuple $x$, so we treat $x$ as a tuple to be realized in some model. We also need the parameters from $A$ to keep all of their first-order properties from the monster model, including quantified properties. This is why we pass to the language $L(A)$ and include the full parameter theory $\operatorname{Th}_A(\mathfrak{C})$, defined as the set of all $L(A)$-sentences true in the expansion of $\mathfrak{C}$ that interprets each constant $c_a$ as the corresponding element $a \in A$. Define \begin{align*} \Sigma := \operatorname{Th}_A(\mathfrak{C}) \cup \{\varphi_i(x) : i \in I\}. \end{align*} To apply first-order compactness, we must verify finite satisfiability. Let $\Sigma_0 \subseteq \Sigma$ be finite. Only finitely many formulas from the family $\{\varphi_i(x) : i \in I\}$ occur in $\Sigma_0$, so there is a finite set $F \subseteq I$ such that those formulas are contained in $\{\varphi_i(x) : i \in F\}$. Since the basic closed sets $[\varphi_i(x)]$ have the finite intersection property, \begin{align*} \bigcap_{i \in F} [\varphi_i(x)] \neq \varnothing. \end{align*} Choose $p_F \in \bigcap_{i \in F} [\varphi_i(x)]$. Then $\varphi_i(x) \in p_F$ for every $i \in F$. Because $p_F \in S_n(A)$, the type $p_F$ is consistent with $\operatorname{Th}_A(\mathfrak{C})$; hence the finite collection $\{\varphi_i(x) : i \in F\}$ is satisfiable together with the finite fragment $\Sigma_0 \cap \operatorname{Th}_A(\mathfrak{C})$. Thus the finite fragment $\Sigma_0$ is satisfiable. Now the [First-Order Compactness Theorem](/theorems/???) applies to the finitely satisfiable set $\Sigma$ of $L(A)$-formulas. It gives an $L(A)$-structure $\mathfrak{M}$ and a tuple $b = (b_1,\dots,b_n) \in M^n$ satisfying all formulas in $\Sigma$. In particular, \begin{align*} \mathfrak{M} \models \varphi_i(b) \end{align*} for every $i \in I$. This tuple $b$ is the simultaneous realization promised by compactness. [/guided] [/step] [step:Extend the realized partial type to a complete type over $A$] Define the $L(A)$-type of $b$ in $\mathfrak{M}$ by \begin{align*} \operatorname{tp}^{\mathfrak{M}}(b/A) := \{\psi(x) : \psi(x) \text{ is an } L(A)\text{-formula and } \mathfrak{M} \models \psi(b)\}. \end{align*} This set is a complete $n$-type over $A$: for every $L(A)$-formula $\psi(x)$, exactly one of $\psi(x)$ and $\neg \psi(x)$ is true of $b$ in $\mathfrak{M}$. It is also consistent with the original parameter structure because $\mathfrak{M} \models \operatorname{Th}_A(\mathfrak{C})$ and every finite subset of $\operatorname{tp}^{\mathfrak{M}}(b/A)$ is realized by $b$ in $\mathfrak{M}$. Hence \begin{align*} p := \operatorname{tp}^{\mathfrak{M}}(b/A) \end{align*} belongs to $S_n(A)$. For every $i \in I$, the previous step gives $\mathfrak{M} \models \varphi_i(b)$, so $\varphi_i(x) \in p$. Therefore \begin{align*} p \in \bigcap_{i \in I} [\varphi_i(x)]. \end{align*} Thus every family of basic closed subsets of $S_n(A)$ with the finite intersection property has nonempty total intersection. [/step] [step:Convert the basic finite intersection property into compactness] Let $(U_j)_{j \in J}$ be an open cover of $S_n(A)$, where $J$ is an index set. Suppose, toward a contradiction, that no finite subfamily covers $S_n(A)$. For each $p \in S_n(A)$, choose an index $j(p) \in J$ such that $p \in U_{j(p)}$. Since the formula sets $[\psi(x)]$ form a basis for the Stone topology, choose an $L(A)$-formula $\psi_p(x)$ such that \begin{align*} p \in [\psi_p(x)] \subseteq U_{j(p)}. \end{align*} Then the basic open family $([\psi_p(x)])_{p \in S_n(A)}$ covers $S_n(A)$. It has no finite subcover, because any finite subcover by these basic opens would give a finite subcover of $(U_j)_{j \in J}$ by the corresponding sets $U_{j(p)}$. Therefore, for every finite subset $F \subseteq S_n(A)$, \begin{align*} S_n(A) \neq \bigcup_{p \in F} [\psi_p(x)]. \end{align*} Taking complements in $S_n(A)$ and using $S_n(A) \setminus [\psi_p(x)] = [\neg \psi_p(x)]$, we obtain \begin{align*} \bigcap_{p \in F} [\neg \psi_p(x)] \neq \varnothing. \end{align*} Thus the family $([\neg \psi_p(x)])_{p \in S_n(A)}$ of basic closed sets has the finite intersection property. By the previous step, there exists $q \in S_n(A)$ such that \begin{align*} q \in \bigcap_{p \in S_n(A)} [\neg \psi_p(x)]. \end{align*} Hence $\neg \psi_p(x) \in q$ for every $p \in S_n(A)$, so $q \notin [\psi_p(x)]$ for every $p \in S_n(A)$. This contradicts that $([\psi_p(x)])_{p \in S_n(A)}$ covers $S_n(A)$. Therefore every open cover of $S_n(A)$ has a finite subcover. Hence $S_n(A)$ is compact. [/step]