[proofplan] The proof identifies complete types with Boolean decisions in the Lindenbaum-Tarski algebra $\mathcal{B}_n(A)$. Starting from a complete type $p$, consistency gives propriety, closure under conjunction gives closure under finite meets, closure under consequence gives upward closure, and completeness gives the ultrafilter decision property. Conversely, an ultrafilter $U$ determines the set of all formulas whose Boolean classes lie in $U$; finite intersections in $U$ give finite satisfiability, compactness gives consistency, and the ultrafilter decision property gives completeness. Uniqueness follows because membership of a formula in the type is exactly membership of its Boolean class in the ultrafilter. [/proofplan]

[step:Send a complete type to a proper filter] Let $p \in S_n(A)$ be a complete $n$-type over $A$. Define \begin{align*} U_p := \{[\varphi]_{\equiv_{T,A}} \in \mathcal{B}_n(A) : \varphi \in p\}. \end{align*} Let $0_{\mathcal{B}} := [x \neq x]_{\equiv_{T,A}}$ denote the bottom element of $\mathcal{B}_n(A)$ and let $1_{\mathcal{B}} := [x = x]_{\equiv_{T,A}}$ denote the top element. Since $p$ is $T$-consistent, $x \neq x \notin p$, and therefore $0_{\mathcal{B}} \notin U_p$. Since every realization of a type satisfies the tautology $x = x$, equivalently since $p$ contains all $T$-logical consequences of the empty set, we have $x = x \in p$, hence $1_{\mathcal{B}} \in U_p$. If $[\varphi]_{\equiv_{T,A}},[\psi]_{\equiv_{T,A}} \in U_p$, then $\varphi,\psi \in p$. Since a complete type is closed under finite conjunctions, $\varphi \wedge \psi \in p$. The meet operation in $\mathcal{B}_n(A)$ is given by \begin{align*} [\varphi]_{\equiv_{T,A}} \wedge [\psi]_{\equiv_{T,A}} = [\varphi \wedge \psi]_{\equiv_{T,A}}, \end{align*} so $[\varphi]_{\equiv_{T,A}} \wedge [\psi]_{\equiv_{T,A}} \in U_p$. Finally, suppose $[\varphi]_{\equiv_{T,A}} \in U_p$ and \begin{align*} [\varphi]_{\equiv_{T,A}} \leq [\psi]_{\equiv_{T,A}} \end{align*} in $\mathcal{B}_n(A)$. By definition of the Boolean order, this means \begin{align*} T \models \forall x\,(\varphi(x) \to \psi(x)). \end{align*} Since $\varphi \in p$ and $p$ is closed under $T$-logical consequence, $\psi \in p$. Hence $[\psi]_{\equiv_{T,A}} \in U_p$. Thus $U_p$ is a proper filter on $\mathcal{B}_n(A)$. [/step]

[step:Use completeness of the type to obtain the ultrafilter decision property] Let $[\varphi]_{\equiv_{T,A}} \in \mathcal{B}_n(A)$ be arbitrary. Since $p$ is complete, exactly one of $\varphi$ and $\neg \varphi$ belongs to $p$. Therefore exactly one of \begin{align*} [\varphi]_{\equiv_{T,A}}, \qquad [\neg \varphi]_{\equiv_{T,A}} \end{align*} belongs to $U_p$. The Boolean complement of $[\varphi]_{\equiv_{T,A}}$ is $[\neg \varphi]_{\equiv_{T,A}}$, so every Boolean element or its complement lies in $U_p$. A proper filter with this decision property is an ultrafilter. Therefore $U_p$ is an ultrafilter on $\mathcal{B}_n(A)$. [/step]

[step:Build a type from an ultrafilter]Let $U$ be an ultrafilter on $\mathcal{B}_n(A)$. Define the set of formulas \begin{align*} p_U := \{\varphi(x) : [\varphi]_{\equiv_{T,A}} \in U\}. \end{align*} We prove that $p_U$ is $T$-consistent. Let $\Delta \subset p_U$ be a finite subset. Write \begin{align*} \Delta = \{\varphi_1,\dots,\varphi_m\} \end{align*} for some $m \in \mathbb{N}$, where each $\varphi_i$ is an $\mathcal{L}(A)$-formula in the free variables among $x$. Since $\varphi_i \in p_U$, we have $[\varphi_i]_{\equiv_{T,A}} \in U$ for every $i \in \{1,\dots,m\}$. Because $U$ is closed under finite meets, \begin{align*} [\varphi_1 \wedge \cdots \wedge \varphi_m]_{\equiv_{T,A}} = [\varphi_1]_{\equiv_{T,A}} \wedge \cdots \wedge [\varphi_m]_{\equiv_{T,A}} \in U. \end{align*} Since $U$ is proper, $0_{\mathcal{B}} \notin U$. Hence \begin{align*} [\varphi_1 \wedge \cdots \wedge \varphi_m]_{\equiv_{T,A}} \neq 0_{\mathcal{B}}. \end{align*} Equivalently, \begin{align*} T \not\models \forall x\,\neg(\varphi_1(x) \wedge \cdots \wedge \varphi_m(x)). \end{align*} Thus $\Delta$ is $T$-consistent. Since every finite subset of $p_U$ is $T$-consistent, the First-Order [Compactness Theorem](/theorems/2748) applies (citing a result not yet in the wiki: First-Order Compactness Theorem), and $p_U$ is $T$-consistent.[/step]

[guided]We want to show that the ultrafilter $U$ really determines a type. The natural candidate is the set of all formulas whose Boolean classes lie in $U$: \begin{align*} p_U := \{\varphi(x) : [\varphi]_{\equiv_{T,A}} \in U\}. \end{align*} The main issue is consistency. A type cannot contain a finite contradictory collection of formulas, so we check finite consistency first. Let $\Delta \subset p_U$ be finite. Choose an enumeration \begin{align*} \Delta = \{\varphi_1,\dots,\varphi_m\} \end{align*} with $m \in \mathbb{N}$, where each $\varphi_i$ is an $\mathcal{L}(A)$-formula in the variables among $x$. Since each $\varphi_i$ belongs to $p_U$, the class $[\varphi_i]_{\equiv_{T,A}}$ lies in $U$. An ultrafilter is, in particular, a filter, so it is closed under finite meets. Therefore \begin{align*} [\varphi_1]_{\equiv_{T,A}} \wedge \cdots \wedge [\varphi_m]_{\equiv_{T,A}} \in U. \end{align*} The meet in $\mathcal{B}_n(A)$ is represented by conjunction, so this is the same as \begin{align*} [\varphi_1 \wedge \cdots \wedge \varphi_m]_{\equiv_{T,A}} \in U. \end{align*} Now we use propriety of the filter. Since $U$ is an ultrafilter, it is a proper filter, so it does not contain the bottom element \begin{align*} 0_{\mathcal{B}} = [x \neq x]_{\equiv_{T,A}}. \end{align*} Hence \begin{align*} [\varphi_1 \wedge \cdots \wedge \varphi_m]_{\equiv_{T,A}} \neq 0_{\mathcal{B}}. \end{align*} This inequality says exactly that the conjunction is not $T$-equivalent to a contradiction. Equivalently, \begin{align*} T \not\models \forall x\,\neg(\varphi_1(x) \wedge \cdots \wedge \varphi_m(x)). \end{align*} Thus the finite set $\Delta$ is $T$-consistent. We have proved that every finite subset of $p_U$ is $T$-consistent. The First-Order Compactness Theorem states that if every finite subset of a set of first-order formulas is satisfiable with a theory $T$, then the entire set is satisfiable with $T$; we cite this as a result not yet in the wiki: First-Order Compactness Theorem. Applying compactness to the set $p_U$ gives that $p_U$ is $T$-consistent.[/guided]

[step:Use the ultrafilter decision property to prove completeness] Let $\varphi(x)$ be any $\mathcal{L}(A)$-formula in the free variables among $x$. Since $U$ is an ultrafilter, exactly one of the Boolean elements \begin{align*} [\varphi]_{\equiv_{T,A}}, \qquad [\neg \varphi]_{\equiv_{T,A}} \end{align*} lies in $U$. Therefore exactly one of $\varphi$ and $\neg \varphi$ lies in $p_U$. Since $p_U$ is already $T$-consistent, this decision property shows that $p_U$ is a complete $n$-type over $A$. Thus $p_U \in S_n(A)$. [/step]

[step:Verify that the two constructions are inverse] First let $p \in S_n(A)$. For any $\mathcal{L}(A)$-formula $\varphi(x)$, \begin{align*} \varphi \in p \quad \Longleftrightarrow \quad [\varphi]_{\equiv_{T,A}} \in U_p \quad \Longleftrightarrow \quad \varphi \in p_{U_p}. \end{align*} Hence $p_{U_p} = p$. Now let $U$ be an ultrafilter on $\mathcal{B}_n(A)$. For any Boolean element $b \in \mathcal{B}_n(A)$, choose an $\mathcal{L}(A)$-formula $\varphi(x)$ such that \begin{align*} b = [\varphi]_{\equiv_{T,A}}. \end{align*} Then \begin{align*} b \in U_{p_U} &\Longleftrightarrow [\varphi]_{\equiv_{T,A}} \in U_{p_U} \\ &\Longleftrightarrow \varphi \in p_U \\ &\Longleftrightarrow [\varphi]_{\equiv_{T,A}} \in U \\ &\Longleftrightarrow b \in U. \end{align*} Therefore $U_{p_U} = U$. The constructions $p \mapsto U_p$ and $U \mapsto p_U$ are inverse to each other, so every ultrafilter on $\mathcal{B}_n(A)$ arises from a unique complete type over $A$. [/step]