[proofplan] We define a global set of formulas by using the given definitional scheme on arbitrary parameters from the monster model: $\varphi(x;b)$ is declared to belong to the global type exactly when $\mathfrak C \models d_p\varphi(b)$. Coherence of the scheme turns finite collections of declarations into a single declaration for a conjunction, which lets us prove finite consistency. Compactness then gives a complete global type, and the Boolean coherence of the scheme shows that this type already decides every formula. Finally, agreement over $M$ gives the extension property, and $M$-definability of each $d_p\varphi$ gives $M$-invariance. [/proofplan]

[step:Define the global candidate by evaluating the scheme in the monster model] For every formula $\varphi(x;y)$ and every tuple $b \in \mathfrak C^{|y|}$, declare \begin{align*} \varphi(x;b) \in q_0 \quad \iff \quad \mathfrak C \models d_p\varphi(b). \end{align*} Here $q_0$ denotes the resulting set of formulas with free variables $x$ and parameters from $\mathfrak C$. We will prove that $q_0$ is a complete type over $\mathfrak C$. Once this is shown, we set $q := q_0$. [/step]

[step:Prove finite consistency by reducing finite declarations to one conjunction]Let $\varphi_0(x;y_0),\dots,\varphi_{n-1}(x;y_{n-1})$ be formulas, let $b_i \in \mathfrak C^{|y_i|}$ for each $i<n$, and suppose \begin{align*} \varphi_i(x;b_i) \in q_0 \end{align*} for every $i<n$. Define the conjunction formula \begin{align*} \psi(x;y_0,\dots,y_{n-1}) := \bigwedge_{i=0}^{n-1} \varphi_i(x;y_i). \end{align*} By coherence of the definitional scheme with finite conjunctions, \begin{align*} \mathfrak C \models d_p\psi(b_0,\dots,b_{n-1}). \end{align*} We claim that the finite set $\{\varphi_i(x;b_i): i<n\}$ is consistent with $T$. First observe that the definitional scheme forces realizability of every $M$-parameter instance it declares. Indeed, if $c=(c_0,\dots,c_{n-1}) \in M^{|y_0|+\cdots+|y_{n-1}|}$ and \begin{align*} M \models d_p\psi(c_0,\dots,c_{n-1}), \end{align*} then the defining property of $d_p\psi$ over $M$ gives $\psi(x;c_0,\dots,c_{n-1}) \in p$. Since $p \in S_x(M)$ is a complete type, the formula $\psi(x;c_0,\dots,c_{n-1})$ is consistent with the elementary diagram of $M$, hence it is realized in some elementary extension of $M$. Therefore \begin{align*} M \models \exists x\,\psi(x;c_0,\dots,c_{n-1}), \end{align*} because existential formulas with parameters from $M$ are preserved by elementary equivalence between $M$ and its elementary extensions. Thus \begin{align*} M \models \forall y_0 \cdots \forall y_{n-1}\,\bigl(d_p\psi(y_0,\dots,y_{n-1}) \to \exists x\,\psi(x;y_0,\dots,y_{n-1})\bigr). \end{align*} Since $M \preceq \mathfrak C$, elementarity gives \begin{align*} \mathfrak C \models \forall y_0 \cdots \forall y_{n-1}\,\bigl(d_p\psi(y_0,\dots,y_{n-1}) \to \exists x\,\psi(x;y_0,\dots,y_{n-1})\bigr). \end{align*} Combining this implication with $\mathfrak C \models d_p\psi(b_0,\dots,b_{n-1})$, we obtain \begin{align*} \mathfrak C \models \exists x\,\psi(x;b_0,\dots,b_{n-1}). \end{align*} Equivalently, $\{\varphi_i(x;b_i): i<n\}$ is realized in $\mathfrak C$, and hence it is consistent with $T$. Thus every finite subset of $q_0$ is consistent with $T$.[/step]

[guided]The point of coherence is that finitely many membership decisions can be tested by one formula. Suppose we have finitely many formulas already declared to lie in $q_0$: \begin{align*} \varphi_i(x;b_i) \in q_0 \qquad (i<n). \end{align*} By definition of $q_0$, this means \begin{align*} \mathfrak C \models d_p\varphi_i(b_i) \end{align*} for each $i<n$. To test whether these formulas are jointly consistent, form the single conjunction \begin{align*} \psi(x;y_0,\dots,y_{n-1}) := \bigwedge_{i=0}^{n-1} \varphi_i(x;y_i). \end{align*} The coherence hypothesis says that the definition assigned to the conjunction agrees with the conjunction of the definitions assigned to the pieces. Hence the individual declarations imply \begin{align*} \mathfrak C \models d_p\psi(b_0,\dots,b_{n-1}). \end{align*} Now we need to turn this definable declaration into actual consistency of the formulas with the chosen parameters $b_0,\dots,b_{n-1}$. The correct route is not to claim that inconsistency for this particular tuple is uniform in all parameter tuples. Instead, we prove over $M$ that whenever the scheme declares $\psi(x;y_0,\dots,y_{n-1})$, an $x$ satisfying the corresponding instance exists. Let $c=(c_0,\dots,c_{n-1}) \in M^{|y_0|+\cdots+|y_{n-1}|}$, and suppose \begin{align*} M \models d_p\psi(c_0,\dots,c_{n-1}). \end{align*} Since $d_p\psi$ defines membership in $p$ over $M$, this gives \begin{align*} \psi(x;c_0,\dots,c_{n-1}) \in p. \end{align*} Because $p \in S_x(M)$ is a complete type, every formula in $p$ is consistent with the elementary diagram of $M$. Therefore $\psi(x;c_0,\dots,c_{n-1})$ is realized in some elementary extension of $M$. The statement that such a realization exists is the existential formula \begin{align*} \exists x\,\psi(x;c_0,\dots,c_{n-1}). \end{align*} Since the parameters $c_0,\dots,c_{n-1}$ lie in $M$, elementarity between $M$ and that elementary extension brings the existential statement back down to $M$: \begin{align*} M \models \exists x\,\psi(x;c_0,\dots,c_{n-1}). \end{align*} Thus, for every tuple from $M$, the implication from declaration to realizability holds. Equivalently, \begin{align*} M \models \forall y_0 \cdots \forall y_{n-1}\,\bigl(d_p\psi(y_0,\dots,y_{n-1}) \to \exists x\,\psi(x;y_0,\dots,y_{n-1})\bigr). \end{align*} Because $M \preceq \mathfrak C$, elementarity transfers this first-order sentence to the monster model: \begin{align*} \mathfrak C \models \forall y_0 \cdots \forall y_{n-1}\,\bigl(d_p\psi(y_0,\dots,y_{n-1}) \to \exists x\,\psi(x;y_0,\dots,y_{n-1})\bigr). \end{align*} Applying the transferred implication to the tuple $(b_0,\dots,b_{n-1})$ and using \begin{align*} \mathfrak C \models d_p\psi(b_0,\dots,b_{n-1}), \end{align*} we obtain \begin{align*} \mathfrak C \models \exists x\,\psi(x;b_0,\dots,b_{n-1}). \end{align*} Unwinding the definition of $\psi$, this says that some element of $\mathfrak C^{|x|}$ satisfies all formulas $\varphi_i(x;b_i)$ for $i<n$. Therefore the finite set $\{\varphi_i(x;b_i):i<n\}$ is consistent with $T$.[/guided]

[step:Use compactness and Boolean coherence to obtain a complete global type] By finite consistency and the [compactness theorem for first-order logic](/theorems/4290) (citing a result not yet in the wiki: [Compactness Theorem](/theorems/2748)), $q_0$ is consistent with $T$. We now show that $q_0$ is complete over $\mathfrak C$. Let $\varphi(x;y)$ be a formula and let $b \in \mathfrak C^{|y|}$. Coherence with negation gives \begin{align*} \mathfrak C \models d_p(\neg \varphi)(b) \iff \mathfrak C \models \neg d_p\varphi(b). \end{align*} Therefore exactly one of the two formulas $\varphi(x;b)$ and $\neg\varphi(x;b)$ belongs to $q_0$. Thus $q_0$ is a complete type over $\mathfrak C$. Set $q := q_0$, so $q \in S_x(\mathfrak C)$. [/step]

[step:Verify that the global type extends the original type over $M$] Let $\varphi(x;y)$ be a formula and let $b \in M^{|y|}$. By the definition of $q$ and by the defining property of the scheme over $M$, \begin{align*} \varphi(x;b) \in q &\iff \mathfrak C \models d_p\varphi(b) \\ &\iff M \models d_p\varphi(b) \\ &\iff \varphi(x;b) \in p. \end{align*} The middle equivalence uses $M \preceq \mathfrak C$ and the fact that $d_p\varphi$ has parameters from $M$. Hence $q|_M=p$, so $q$ extends $p$. [/step]

[step:Check invariance under automorphisms fixing $M$ pointwise] Let $\sigma \in \operatorname{Aut}(\mathfrak C/M)$ be an automorphism fixing $M$ pointwise. Let $\varphi(x;y)$ be a formula and let $b \in \mathfrak C^{|y|}$. Since $d_p\varphi(y)$ is $M$-definable, $\sigma$ fixes its parameters. Therefore \begin{align*} \mathfrak C \models d_p\varphi(b) \quad \iff \quad \mathfrak C \models d_p\varphi(\sigma(b)). \end{align*} Using the definition of $q$ on both sides, \begin{align*} \varphi(x;b) \in q \quad \iff \quad \varphi(x;\sigma(b)) \in q. \end{align*} This is precisely $M$-invariance of $q$. Therefore $q$ is a global $M$-invariant extension of $p$. [/step]