[proofplan] We work in the parameter language $\mathcal{L}(A)$, interpreting each parameter from $A$ in the fixed ambient structure $M \models T$ used to define $S_n(A)$, and we set $T_A := \operatorname{Th}_{\mathcal{L}(A)}((M,a)_{a \in A})$. The relation $\equiv_{T,A}$ means equivalence modulo this expanded theory $T_A$, and a point of $S_n(A)$ is a complete consistent $\mathcal{L}(A)$-type extending $T_A$. We prove that formula classes and clopen subsets of the type space carry exactly the same Boolean information. First we check that the assignment is well-defined and respects the Boolean operations because membership in a complete type respects logical negation, conjunction, and disjunction. Then we prove injectivity by extending any consistent symmetric-difference formula to a complete type and deriving separation. Finally, every nonempty clopen subset is a finite union of basic formula neighborhoods by compactness of the Stone space, while the empty clopen set is represented by contradiction. [/proofplan]

[step:Define the map on formula classes and check it is well-defined]Let $M \models T$ be the ambient structure containing $A$ that is used to define $S_n(A)$. Let $\mathcal{L}(A)$ denote the language obtained from $\mathcal{L}$ by adding a constant symbol for each element of $A$, interpreted in $M$ by that element. Define \begin{align*} T_A := \operatorname{Th}_{\mathcal{L}(A)}((M,a)_{a \in A}), \end{align*} the complete $\mathcal{L}(A)$-theory of the resulting parameter expansion. Thus $S_n(A)$ is the set of complete consistent $\mathcal{L}(A)$-types in the variables $x_1,\dots,x_n$ extending $T_A$. Let $\varphi(x_1,\dots,x_n)$ and $\psi(x_1,\dots,x_n)$ be $\mathcal{L}(A)$-formulas such that $\varphi \equiv_{T,A} \psi$. Define \begin{align*} \Theta([\varphi]_{\equiv_{T,A}}) := [\varphi]_{S_n(A)}. \end{align*} If $p \in S_n(A)$, then $p$ is a complete consistent $\mathcal{L}(A)$-type extending $T_A$. Since $T_A \models \forall x_1 \cdots \forall x_n\,(\varphi \leftrightarrow \psi)$, maximal consistency of $p$ implies that $p \cup \{\varphi,\neg\psi\}$ and $p \cup \{\psi,\neg\varphi\}$ are inconsistent. Hence $\varphi \in p$ iff $\psi \in p$. Therefore \begin{align*} [\varphi]_{S_n(A)} = [\psi]_{S_n(A)}. \end{align*} Thus $\Theta$ is well-defined.[/step]

[guided]The possible ambiguity is that an element of $\mathcal{B}_n(A)$ is not a formula itself, but an equivalence class of formulas. Therefore we must prove that replacing a representative by an equivalent formula does not change the subset of $S_n(A)$ obtained. Let $M \models T$ be the ambient structure containing $A$. Let $\mathcal{L}(A)$ denote the language obtained from $\mathcal{L}$ by adding one constant symbol for each parameter from $A$, interpreted in $M$ by that parameter. We define \begin{align*} T_A := \operatorname{Th}_{\mathcal{L}(A)}((M,a)_{a \in A}). \end{align*} Thus $S_n(A)$ consists of complete consistent $\mathcal{L}(A)$-types in the variables $x_1,\dots,x_n$ extending this expanded theory $T_A$. Let $\varphi(x_1,\dots,x_n)$ and $\psi(x_1,\dots,x_n)$ be $\mathcal{L}(A)$-formulas with $\varphi \equiv_{T,A} \psi$. By definition, this means \begin{align*} T_A \models \forall x_1 \cdots \forall x_n\,(\varphi(x_1,\dots,x_n) \leftrightarrow \psi(x_1,\dots,x_n)). \end{align*} Now take any $p \in S_n(A)$. The object $p$ is a complete $n$-type over $A$, so it is a maximal consistent collection of $\mathcal{L}(A)$-formulas in the variables $x_1,\dots,x_n$ extending $T_A$. Since $T_A$ entails that $\varphi$ and $\psi$ are equivalent, no complete type extending $T_A$ can contain exactly one of $\varphi$ and $\psi$. Therefore \begin{align*} \varphi \in p \quad \iff \quad \psi \in p. \end{align*} This equivalence holds for every $p \in S_n(A)$, so the two formula-defined subsets are equal: \begin{align*} [\varphi]_{S_n(A)} = \{p \in S_n(A) : \varphi \in p\} = \{p \in S_n(A) : \psi \in p\} = [\psi]_{S_n(A)}. \end{align*} Thus the formula class $[\varphi]_{\equiv_{T,A}}$ has a well-defined image under $\Theta$.[/guided]

[step:Verify that the map preserves Boolean operations] Let $\varphi(x_1,\dots,x_n)$ and $\psi(x_1,\dots,x_n)$ be $\mathcal{L}(A)$-formulas. Since each $p \in S_n(A)$ is complete, exactly one of $\varphi$ and $\neg\varphi$ lies in $p$, and similarly for Boolean combinations. Hence \begin{align*} [\neg \varphi]_{S_n(A)} &= S_n(A) \setminus [\varphi]_{S_n(A)}, \\ [\varphi \wedge \psi]_{S_n(A)} &= [\varphi]_{S_n(A)} \cap [\psi]_{S_n(A)}, \\ [\varphi \vee \psi]_{S_n(A)} &= [\varphi]_{S_n(A)} \cup [\psi]_{S_n(A)}. \end{align*} Therefore $\Theta$ preserves complements, finite meets, finite joins, the bottom element $[\bot]_{\equiv_{T,A}}$, and the top element $[\top]_{\equiv_{T,A}}$. Thus $\Theta$ is a Boolean algebra homomorphism. [/step]

[step:Prove injectivity by separating inequivalent formulas with a complete type]Suppose $\Theta([\varphi]_{\equiv_{T,A}})=\Theta([\psi]_{\equiv_{T,A}})$. Define the symmetric-difference formula \begin{align*} \delta(x_1,\dots,x_n) := (\varphi(x_1,\dots,x_n) \wedge \neg\psi(x_1,\dots,x_n)) \vee (\psi(x_1,\dots,x_n) \wedge \neg\varphi(x_1,\dots,x_n)). \end{align*} Assume, toward a contradiction, that the $\mathcal{L}(A)$-theory $T_A \cup \{\delta\}$ is consistent. By the type-extension consequence of the first-order [compactness theorem](/theorems/2748), applied to the consistent partial type $\{\delta\}$ over the consistent $\mathcal{L}(A)$-theory $T_A$, there exists a complete type $p \in S_n(A)$ with $\delta \in p$. Since $p$ is complete and contains $\delta$, either $\varphi \in p$ and $\psi \notin p$, or $\psi \in p$ and $\varphi \notin p$. Therefore $p$ lies in exactly one of $[\varphi]_{S_n(A)}$ and $[\psi]_{S_n(A)}$, contradicting \begin{align*} [\varphi]_{S_n(A)} = [\psi]_{S_n(A)}. \end{align*} Thus $T_A \cup \{\delta\}$ is inconsistent, meaning \begin{align*} T_A \models \forall x_1 \cdots \forall x_n\,(\varphi \leftrightarrow \psi). \end{align*} Hence $[\varphi]_{\equiv_{T,A}} = [\psi]_{\equiv_{T,A}}$, so $\Theta$ is injective.[/step]

[guided]We prove injectivity by showing that equality of the type-definable sets forces logical equivalence over the parameter theory $T_A$. Suppose \begin{align*} \Theta([\varphi]_{\equiv_{T,A}})=\Theta([\psi]_{\equiv_{T,A}}). \end{align*} This says exactly that \begin{align*} [\varphi]_{S_n(A)} = [\psi]_{S_n(A)}. \end{align*} Define the $\mathcal{L}(A)$-formula \begin{align*} \delta(x_1,\dots,x_n) := (\varphi(x_1,\dots,x_n) \wedge \neg\psi(x_1,\dots,x_n)) \vee (\psi(x_1,\dots,x_n) \wedge \neg\varphi(x_1,\dots,x_n)). \end{align*} The formula $\delta$ records precisely the failure of $\varphi$ and $\psi$ to agree on an $n$-tuple. If $\delta$ were consistent with the parameter-expanded theory, then the partial type $\{\delta\}$ over $T_A$ would be consistent. The type-extension consequence of the first-order compactness theorem applies because $T_A \cup \{\delta\}$ is, by this assumption, a consistent $\mathcal{L}(A)$-theory in the variables $x_1,\dots,x_n$. Therefore there is a complete consistent $\mathcal{L}(A)$-type $p \in S_n(A)$ extending $T_A \cup \{\delta\}$, so $\delta \in p$. Now completeness of $p$ turns the disjunction defining $\delta$ into an actual separation. Since $p$ is a maximal consistent set of formulas and contains \begin{align*} (\varphi \wedge \neg\psi) \vee (\psi \wedge \neg\varphi), \end{align*} it follows that either $\varphi \in p$ and $\neg\psi \in p$, or $\psi \in p$ and $\neg\varphi \in p$. Equivalently, $p$ belongs to exactly one of the two basic clopen sets $[\varphi]_{S_n(A)}$ and $[\psi]_{S_n(A)}$. This contradicts their equality. Hence $T_A \cup \{\delta\}$ is inconsistent. Inconsistency of the symmetric difference is exactly the statement that the two formulas are equivalent over $T_A$: \begin{align*} T_A \models \forall x_1 \cdots \forall x_n\,(\varphi \leftrightarrow \psi). \end{align*} Thus $[\varphi]_{\equiv_{T,A}} = [\psi]_{\equiv_{T,A}}$, proving that $\Theta$ is injective.[/guided]

[step:Represent every clopen set by a finite disjunction of formulas]Let $C \in \operatorname{Clop}(S_n(A))$. If $C=\varnothing$, then $C=[\bot]_{S_n(A)}$, where $\bot(x_1,\dots,x_n)$ is any contradictory $\mathcal{L}(A)$-formula, so $C$ lies in the image of $\Theta$. We may therefore assume $C \neq \varnothing$. The Stone topology on $S_n(A)$ is the topology whose basis consists of the formula neighborhoods $[\rho]_{S_n(A)}$, where $\rho(x_1,\dots,x_n)$ ranges over $\mathcal{L}(A)$-formulas. Since $C$ is open in this topology, for each $p \in C$ there exists an $\mathcal{L}(A)$-formula $\varphi_p(x_1,\dots,x_n) \in p$ such that \begin{align*} p \in [\varphi_p]_{S_n(A)} \subset C. \end{align*} Thus the family \begin{align*} \{[\varphi_p]_{S_n(A)} : p \in C\} \end{align*} is an open cover of $C$. The Stone space $S_n(A)$ is compact by the usual finite-intersection-property argument from first-order compactness: any family of closed formula conditions with the finite intersection property determines a finitely satisfiable partial type over $T_A$, hence is realized by some complete type in $S_n(A)$. Because $C$ is closed in $S_n(A)$, it is compact. Hence there exist $p_1,\dots,p_m \in C$, with $m \in \mathbb{N}$, such that \begin{align*} C = \bigcup_{i=1}^{m} [\varphi_{p_i}]_{S_n(A)}. \end{align*} Define the $\mathcal{L}(A)$-formula \begin{align*} \theta(x_1,\dots,x_n) := \bigvee_{i=1}^{m} \varphi_{p_i}(x_1,\dots,x_n). \end{align*} Using preservation of finite joins proved above, \begin{align*} [\theta]_{S_n(A)} = \bigcup_{i=1}^{m} [\varphi_{p_i}]_{S_n(A)} = C. \end{align*} Therefore $C$ lies in the image of $\Theta$, so $\Theta$ is surjective.[/step]

[guided]We prove surjectivity by starting with an arbitrary clopen subset $C \in \operatorname{Clop}(S_n(A))$ and building one formula whose basic clopen set is exactly $C$. First handle the degenerate case. If $C=\varnothing$, choose a contradictory $\mathcal{L}(A)$-formula $\bot(x_1,\dots,x_n)$. No complete consistent type contains $\bot$, so \begin{align*} [\bot]_{S_n(A)}=\varnothing=C. \end{align*} Thus the empty clopen set is already in the image. We now assume $C \neq \varnothing$. The Stone topology on $S_n(A)$ is defined by declaring the formula neighborhoods $[\rho]_{S_n(A)}$, with $\rho(x_1,\dots,x_n)$ an $\mathcal{L}(A)$-formula, to be a basis. Therefore, because $C$ is open, each point $p \in C$ has a basic formula neighborhood contained in $C$. Concretely, for each $p \in C$ there is an $\mathcal{L}(A)$-formula $\varphi_p(x_1,\dots,x_n) \in p$ such that \begin{align*} p \in [\varphi_p]_{S_n(A)} \subset C. \end{align*} Therefore the family \begin{align*} \{[\varphi_p]_{S_n(A)} : p \in C\} \end{align*} is an open cover of $C$. Now compactness is the point where clopen, rather than merely open, is used. Since $C$ is clopen, it is closed in $S_n(A)$. The space $S_n(A)$ is compact by the standard finite-intersection-property proof from first-order compactness: a family of closed formula conditions with the finite intersection property is exactly a finitely satisfiable partial type over $T_A$, and compactness extends it to a complete type in $S_n(A)$. A closed subset of a compact [topological space](/page/Topological%20Space) is compact, so $C$ is compact. Hence the open cover above has a finite subcover: there exist $p_1,\dots,p_m \in C$, with $m \in \mathbb{N}$, such that \begin{align*} C = \bigcup_{i=1}^{m} [\varphi_{p_i}]_{S_n(A)}. \end{align*} Define the $\mathcal{L}(A)$-formula \begin{align*} \theta(x_1,\dots,x_n) := \bigvee_{i=1}^{m} \varphi_{p_i}(x_1,\dots,x_n). \end{align*} Because membership in a complete type respects finite disjunctions, the preservation of finite joins proved earlier gives \begin{align*} [\theta]_{S_n(A)} = \bigcup_{i=1}^{m} [\varphi_{p_i}]_{S_n(A)} = C. \end{align*} Thus $C$ is in the image of $\Theta$. Since $C$ was an arbitrary clopen subset of $S_n(A)$, $\Theta$ is surjective.[/guided]

[step:Conclude that the formula algebra is exactly the clopen algebra] The map $\Theta$ is a well-defined Boolean algebra homomorphism, injective by separation through complete types, and surjective because every clopen subset of $S_n(A)$ is either empty or defined by a finite disjunction of basic formula neighborhoods. The completeness of the ambient theory $T$ belongs to the standard setup for type spaces; the Boolean-algebra argument itself uses the precise parameter-expanded theory $T_A = \operatorname{Th}_{\mathcal{L}(A)}((M,a)_{a \in A})$ and maximal completeness of the types themselves. Therefore \begin{align*} \Theta: \mathcal{B}_n(A) \longrightarrow \operatorname{Clop}(S_n(A)) \end{align*} is a Boolean algebra isomorphism. [/step]