定義による拡大

1（存在）：$M\models T$ なので、$M\models\forall\bar x\,\exists!\,y\,\psi_f$ であり、各 $\bar a\in M^n$ に対し $M\models\psi_f[\bar a,b]$ となる $b$ がただ 1 つある。よって上の式で $f^{M'}$ は写像 $M^n\to M$ として定まる（$n=0$ なら $M$ の元が 1 つ定まる）。$R^{M'}$ も上の式で定め、$L$ の記号は $M$ と同じに解釈して $M'$ を作る。$M'|_L=M$ なので、簡約で $L$ の論理式の真偽は変わらず、$M'\models T$ である。$\bar a\in M^n$ と $b\in M$ について
$$ M'\models R[\bar a]\iff\bar a\in R^{M'}\iff M\models\varphi_R[\bar a]\iff M'\models\varphi_R[\bar a], $$
$$ M'\models(f(\bar x)=y)[\bar a,b]\iff f^{M'}(\bar a)=b\iff M\models\psi_f[\bar a,b]\iff M'\models\psi_f[\bar a,b] $$
であり（各行の最後の同値は $\varphi_R,\psi_f$ が $L$ の論理式であることによる）、$M'$ はすべての定義公理を満たす。
1（一意性）：$M''$ も $M''|_L=M$ を満たす $T'$ のモデルとする。$M''\models\delta_R$ なので、上と同じ計算で $\bar a\in R^{M''}\iff M\models\varphi_R[\bar a]\iff\bar a\in R^{M'}$ である。$M''\models\delta_f$ なので、$b:=f^{M''}(\bar a)$ について $M''\models(f(\bar x)=y)[\bar a,b]$ から $M\models\psi_f[\bar a,b]$ が従い、$\psi_f$ を満たす $b$ はただ 1 つなので $f^{M''}(\bar a)=f^{M'}(\bar a)$ である。台集合と $L$ の記号の解釈はどちらも $M$ と同じなので、$M''=M'$ である。
2：$T\subset T'$ なので $N'|_L$ は $T$ のモデルである。$N'$ は $T'$ のモデルで簡約が $N'|_L$ なので、1 の一意性により、$N'$ は $N'|_L$ の 1 の拡張に等しい。$\square$

thm-defext-unique-expansion の 2 により $T'$ のモデルの簡約は $T$ のモデルであり、1 により $T$ のどのモデルも $T'$ のモデルに拡張できる。保存拡大 の記事の定理「モデルの拡張による判定」により、$T'$ は $T$ の保存拡大である。直接に書けば、$L$ の文 $\sigma$ について $T'\vdash\sigma$ なら、$T$ の任意のモデル $M$ の拡張 $M'$ で $\sigma$ が真なので、簡約 $M$ でも真であり、$T\models\sigma$、すなわち $T\vdash\sigma$ となる。後半は同記事の命題「保存拡大の基本性質」の 2 による。$\square$

$t$ の組み立てについての帰納法で示す。$t$ が変数 $x$ なら、両辺とも $s(y)=s(x)$ である。$t=f(t_1,\dots,t_n)$（$f$ は新しい関数記号）とする。$M\models E_t(y)[s]$ は、ある $b_1,\dots,b_n\in M$ があって、$s$ の $u_i$ での値を $b_i$ に替えた割り当て $s'$ について、すべての $i$ で $M\models E_{t_i}(u_i)[s']$、かつ $M\models\psi_f(u_1,\dots,u_n,y)[s']$、すなわち代入補題と $s'(y)=s(y)$ により $M\models\psi_f[\bar b,s(y)]$ となることである。$u_i$ は新しい変数なので $t_i$ に現れず、$E_{t_i}(u_i)$ の自由変数は $t_i$ の変数と $u_i$ だけである。帰納法の仮定と一致補題（一階述語論理 の記事の補題「一致補題」）により、$M\models E_{t_i}(u_i)[s']$ は $b_i=t_i^{M'}[s']=t_i^{M'}[s]$ と同値である。また $M'$ の作り方により、$M\models\psi_f[\bar b,s(y)]$ は $s(y)=f^{M'}(\bar b)$ と同値である。よって
$$ M\models E_t(y)[s]\iff s(y)=f^{M'}\bigl(t_1^{M'}[s],\dots,t_n^{M'}[s]\bigr)=t^{M'}[s] $$
である。$t=g(t_1,\dots,t_k)$（$g$ は $L$ の記号）の場合も、最後の連言肢 $y=g(\bar u)$ について同じ議論をすればよい。$\square$

まず、$T$ のモデル $M$、その拡張 $M'$、割り当て $s$ について
$$ M'\models\theta[s]\iff M\models\theta^*[s] $$
を $\theta$ の組み立てについての帰納法で示す（以下この同値を ($\dagger$) と呼ぶ）。$\theta=R(t_1,\dots,t_n)$（$R$ は新しい関係記号）なら、lem-defext-term、代入補題と一致補題により、$M\models\theta^*[s]$ は「$b_i=t_i^{M'}[s]$ となる $b_i$ について $M\models\varphi_R[\bar b]$」、すなわち $(t_1^{M'}[s],\dots,t_n^{M'}[s])\in R^{M'}$ と同値であり、これは $M'\models\theta[s]$ である。$t_1=t_2$ と $L$ の関係記号の場合も同じである。論理結合子の段は帰納法の仮定から直ちに従う。$\theta=\forall x\,\theta_1$ なら、$M$ と $M'$ の台集合は同じなので
$$ M'\models\theta[s]\iff\text{すべての }a\in M\text{ で }M'\models\theta_1[s_x^a]\iff\text{すべての }a\in M\text{ で }M\models\theta_1^*[s_x^a]\iff M\models\theta^*[s] $$
である。$\exists$ も同様である。
次に $T'$ の任意のモデル $N'$ をとる。thm-defext-unique-expansion の 2 により、$N:=N'|_L$ は $T$ のモデルで、$N'$ は $N$ の拡張である。($\dagger$) と、簡約で $L$ の論理式の真偽が変わらないことから、どの割り当て $s$ についても
$$ N'\models\theta[s]\iff N\models\theta^*[s]\iff N'\models\theta^*[s] $$
である。よって $T'\models\forall\bar z\,(\theta\leftrightarrow\theta^*)$、すなわち $T'\vdash\forall\bar z\,(\theta\leftrightarrow\theta^*)$ である。
$\theta$ が文なら $\operatorname{FV}(\theta^*)\subset\operatorname{FV}(\theta)=\emptyset$ である。$T'\vdash\theta$ なら $T'\vdash\theta^*$ であり、$\theta^*$ は $L$ の文なので、cor-defext-conservative により $T\vdash\theta^*$ である。逆に $T\vdash\theta^*$ なら、$T'$ は $T$ の拡大なので $T'\vdash\theta^*$、したがって $T'\vdash\theta$ である。$\square$

定義可能な関係は 一階述語論理 の記事の定義「定義可能な関係」の意味とする。$L$ の論理式は $L'$ の論理式でもあり、簡約で真偽は変わらないので、$M$ で定義可能な関係は $M'$ でも同じ論理式で定義可能である。逆に $L'$ の論理式 $\theta$ が定義する関係は、($\dagger$) により $L$ の論理式 $\theta^*$ が $M$ で定義する関係に等しい。$\square$

$L''\setminus L'$ の記号 $X$ の定義の右辺を $\chi_X$（$L'$ の論理式）とし、thm-defext-elimination の $L$ の論理式 $\chi_X^*$ をとる。$X$ が関数記号 $f$ なら、$T'\vdash\forall\bar x\,\exists!\,y\,\chi_f$ と $T'\vdash\forall\bar x\,\forall y\,(\chi_f\leftrightarrow\chi_f^*)$ から $T'\vdash\forall\bar x\,\exists!\,y\,\chi_f^*$ が従う。これは $L$ の文なので、cor-defext-conservative により $T\vdash\forall\bar x\,\exists!\,y\,\chi_f^*$ である。よって $\chi_X^*$ を右辺とする定義公理 $\delta_X^*$ は $T$ 上の正しい定義であり、
$$ U:=T\cup\{\delta_X\mid X\in L'\setminus L\}\cup\{\delta_X^*\mid X\in L''\setminus L'\} $$
は $T$ の定義による拡大である。$L''$ 構造 $N$ について、$N$ が $T''$ のモデルであることと $U$ のモデルであることを比べる。どちらの場合も $N|_{L'}$ は $T'$ のモデルである（$T'\subset T''$、$T'\subset U$）。$N|_{L'}$ が $T'$ のモデルなら $\chi_X$ と $\chi_X^*$ は $N$ で同値なので、$N\models\delta_X\iff N\models\delta_X^*$ である。よって $T''$ と $U$ のモデルは一致する。$\square$