[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.
[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]
[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]
