[proofplan] We compare the usual definition of $\kappa$-saturation, which realizes complete types over parameter sets of size $<\kappa$, with the apparently stronger condition that all finitely satisfiable partial types over such parameter sets are realized. In the forward direction, compactness turns finite satisfiability of a partial type into consistency with the complete parameter theory of $M$, and then a completion of the partial type is realized by saturation. In the reverse direction, every complete type consistent with the parameter theory is finitely satisfiable in $M$, so the assumed partial-type condition realizes it. [/proofplan] [step:Fix the parameter language and the meaning of finite satisfiability] Let $A \subset M$ satisfy $|A| < \kappa$. Define $L(A)$ to be the language obtained from $L$ by adding a constant symbol $c_b$ for each element $b \in A$. Let $M_A$ denote the $L(A)$-structure whose underlying $L$-structure is $M$ and in which $c_b^{M_A} = b$ for every $b \in A$. For a finite tuple of variables $x = (x_1,\dots,x_n)$, a partial $L(A)$-type $\Sigma(x)$ is finitely satisfiable in $M$ precisely when, for every finite subset $\Delta(x) \subset \Sigma(x)$, there exists $a_\Delta \in M^n$ such that \begin{align*} M_A \models \bigwedge_{\varphi \in \Delta} \varphi(a_\Delta). \end{align*} A tuple $a \in M^n$ realizes $\Sigma(x)$ in $M$ precisely when \begin{align*} M_A \models \varphi(a) \end{align*} for every $\varphi(x) \in \Sigma(x)$. [/step] [step:Use compactness to complete a finitely satisfiable partial type] Assume that $M$ is $\kappa$-saturated in the usual sense: for every $A \subset M$ with $|A| < \kappa$, every complete $L(A)$-type in finitely many variables consistent with $\operatorname{Th}(M_A)$ is realized in $M$. Let $\Sigma(x)$ be a partial $L(A)$-type finitely satisfiable in $M$. We claim that \begin{align*} \operatorname{Th}(M_A) \cup \Sigma(x) \end{align*} is consistent. Indeed, let $\Gamma$ be a finite subset of $\operatorname{Th}(M_A) \cup \Sigma(x)$. Write $\Gamma_T := \Gamma \cap \operatorname{Th}(M_A)$ and $\Gamma_\Sigma := \Gamma \cap \Sigma(x)$. Since $\Sigma(x)$ is finitely satisfiable in $M$, choose $a \in M^n$ such that \begin{align*} M_A \models \bigwedge_{\varphi \in \Gamma_\Sigma} \varphi(a). \end{align*} Every sentence in $\Gamma_T$ holds in $M_A$ by definition of $\operatorname{Th}(M_A)$. Hence $M_A$, with the tuple $a$ assigned to $x$, satisfies every formula in $\Gamma$. Therefore every finite subset of $\operatorname{Th}(M_A) \cup \Sigma(x)$ is satisfiable. By the first-order [compactness theorem](/theorems/2748) (citing a result not yet in the wiki: [Compactness Theorem for First-Order Logic](/theorems/4290)), $\operatorname{Th}(M_A) \cup \Sigma(x)$ is consistent. By the type extension lemma obtained from Lindenbaum's construction for complete theories, extend $\Sigma(x)$ to a complete $L(A)$-type $p(x)$ such that \begin{align*} \Sigma(x) \subset p(x) \end{align*} and $p(x)$ is consistent with $\operatorname{Th}(M_A)$. [guided] We want to use $\kappa$-saturation, but the definition of saturation applies to complete types, while $\Sigma(x)$ may be only partial. The first task is therefore to show that $\Sigma(x)$ is compatible with the full parameter theory of $M$. Consider the set of formulas and sentences \begin{align*} \operatorname{Th}(M_A) \cup \Sigma(x). \end{align*} To prove consistency by compactness, we verify finite satisfiability. Let $\Gamma$ be a finite subset of this union. Split it into the part coming from the theory and the part coming from the partial type: \begin{align*} \Gamma_T &:= \Gamma \cap \operatorname{Th}(M_A),\\ \Gamma_\Sigma &:= \Gamma \cap \Sigma(x). \end{align*} The set $\Gamma_\Sigma$ is finite, so finite satisfiability of $\Sigma(x)$ in $M$ gives a tuple $a \in M^n$ such that \begin{align*} M_A \models \bigwedge_{\varphi \in \Gamma_\Sigma} \varphi(a). \end{align*} On the other hand, every sentence in $\Gamma_T$ is true in $M_A$ by the definition of $\operatorname{Th}(M_A)$. Thus the same structure $M_A$, together with the assignment $x \mapsto a$, satisfies all members of $\Gamma$. Since every finite subset of $\operatorname{Th}(M_A) \cup \Sigma(x)$ is satisfiable, the first-order compactness theorem (citing a result not yet in the wiki: Compactness Theorem for First-Order Logic) implies that \begin{align*} \operatorname{Th}(M_A) \cup \Sigma(x) \end{align*} is consistent. This is exactly the bridge from finite satisfiability to type-theoretic consistency. Now we still need a complete type, because saturation is stated for complete types. Using the standard Lindenbaum extension argument for first-order theories, extend the consistent partial type $\Sigma(x)$ to a complete $L(A)$-type $p(x)$ with \begin{align*} \Sigma(x) \subset p(x), \end{align*} while preserving consistency with $\operatorname{Th}(M_A)$. [/guided] [/step] [step:Apply saturation to realize the completion] Since $|A| < \kappa$ and $p(x)$ is a complete $L(A)$-type consistent with $\operatorname{Th}(M_A)$, $\kappa$-saturation of $M$ gives a tuple $a \in M^n$ such that \begin{align*} M_A \models \psi(a) \end{align*} for every $\psi(x) \in p(x)$. Since $\Sigma(x) \subset p(x)$, the same tuple satisfies \begin{align*} M_A \models \varphi(a) \end{align*} for every $\varphi(x) \in \Sigma(x)$. Hence every finitely satisfiable partial type over every parameter set $A \subset M$ of size $<\kappa$ is realized in $M$. [/step] [step:Show that a complete type consistent with the parameter theory is finitely satisfiable in $M$] Conversely, assume the partial-type condition in the statement. Let $A \subset M$ satisfy $|A| < \kappa$, let $x = (x_1,\dots,x_n)$ be a finite tuple of variables with $n \geq 1$, and let $p(x)$ be a complete $L(A)$-type consistent with $\operatorname{Th}(M_A)$. We prove that $p(x)$ is finitely satisfiable in $M$. Let $\Delta(x) \subset p(x)$ be finite, and define the $L(A)$-formula \begin{align*} \theta_\Delta(x) := \bigwedge_{\varphi \in \Delta} \varphi(x). \end{align*} Since $p(x)$ is consistent with $\operatorname{Th}(M_A)$, the set \begin{align*} \operatorname{Th}(M_A) \cup \{\theta_\Delta(x)\} \end{align*} is satisfiable. Therefore the $L(A)$-sentence \begin{align*} \exists x_1 \cdots \exists x_n\, \theta_\Delta(x) \end{align*} is consistent with $\operatorname{Th}(M_A)$. Because $\operatorname{Th}(M_A)$ is the complete theory of $M_A$, this sentence must belong to $\operatorname{Th}(M_A)$, and hence \begin{align*} M_A \models \exists x_1 \cdots \exists x_n\, \theta_\Delta(x). \end{align*} Thus there exists $a_\Delta \in M^n$ such that \begin{align*} M_A \models \bigwedge_{\varphi \in \Delta} \varphi(a_\Delta). \end{align*} Since $\Delta$ was arbitrary, $p(x)$ is finitely satisfiable in $M$. [/step] [step:Realize complete types and conclude saturation] By the assumed partial-type condition, the finitely satisfiable partial type $p(x)$ is realized in $M$. That is, there exists $a \in M^n$ such that \begin{align*} M_A \models \varphi(a) \end{align*} for every $\varphi(x) \in p(x)$. Therefore every complete $L(A)$-type over every parameter set $A \subset M$ with $|A| < \kappa$ that is consistent with $\operatorname{Th}(M_A)$ is realized in $M$. This is precisely the usual definition of $\kappa$-saturation. Hence $M$ is $\kappa$-saturated, completing the proof of the equivalence. [/step]