省略型定理
概要
省略型定理（omitting types theorem）とは、可算な一階言語の充足可能な理論 $T$ と、$T$ のもとで孤立していない、つまり 1 つの論理式から導かれない論理式の集合（型）の可算族について、それらをどれも実現しない高々可算な $T$ のモデルがあるという定理である。言語の可算性と型の族の可算性は外せない。可算言語の完全な理論では、すべてのモデルで実現される型と孤立した型が一致し、孤立していない完全型があれば同型でない可算なモデルが 2 つある。可算なモデルを作り分ける基本の道具で、可算範疇的な理論の特徴づけ（Ryll-Nardzewski の定理）に使われる。
前提知識: 型(モデル理論), コンパクト性定理(一階論理), 初等部分モデル, 完全な理論
コンパクト性定理を使うと、ある型を実現するモデルはいつでも作れる。逆に、型を 実現しない（省略する）モデルを作るのは難しい。完全な理論で、1 つの論理式から導かれる型（孤立した型）は、どのモデルでも実現されてしまうからである（型(モデル理論) の命題「孤立した型はすべてのモデルで実現される」）。省略型定理（omitting types theorem）は、言語が可算なら、この障害が唯一のものであることを述べる。すなわち、孤立していない型は、可算個まとめて、可算なモデルで省略できる。
この記事では、省略型定理を述べて完全に証明する。証明は、新しい定数記号を可算個加え、文を 1 つずつ決めながら、証人を加える段と、型を省略させる段を交互に行う構成である。帰結として、可算言語の完全な理論では「すべてのモデルで実現される型」と「孤立した型」が一致すること、孤立していない完全型があれば同型でない可算なモデルが 2 つあることを示す。言語の可算性や型の個数の条件が外せないことも例で確かめる。
主張
以下、$L$ は一階言語、$T$ は $L$ の文の集合とする。型・実現・省略・孤立の意味は 型(モデル理論) の定義「型」「実現と省略」「孤立した型」のとおりである。とくに、$L$ の論理式 $\varphi(\bar x)$ が $T$ のもとで論理式の集合 $p(\bar x)$ を孤立させるとは、$T\cup\{\exists\bar x\,\varphi\}$ が充足可能で、$p$ のすべての元 $\psi$ について $T\models\forall\bar x\,(\varphi\to\psi)$ となることであった。
$L$ を可算な一階言語、$T$ を充足可能な $L$ の理論とする。各 $i\in\mathbb N$ について、$p_i(x_1,\dots,x_{n_i})$（$n_i\ge1$）を $L$ の論理式の集合で、$T$ のもとで孤立していないものとする。このとき、$T$ の高々可算なモデルで、すべての $p_i$ を省略するものがある。
証明は後の節「証明」で与える。$p_i$ は $T$ の型でなくてもよい（$T$ と同時に充足可能でない集合は、どのモデルでも省略される）。型が有限個のときや 1 つのときは、同じ型を繰り返して並べればよい。可算言語の完全な理論と 1 変数の型の場合の主張は、対偶の形で HS24 §3.4 にある。
$L$ が可算で $T$ が完全な理論のとき、$L$ の論理式の集合 $p(\bar x)$ について次は同値である。
- $T$ のどのモデルも $p$ を実現する。
- $T$ の高々可算なモデルはどれも $p$ を実現する。
- $p$ は $T$ のもとで孤立している。
1 ⇒ 2 は明らかである。2 ⇒ 3 は thm-ott-main の対偶である（$p_i:=p$ とする）。3 ⇒ 1 は 型(モデル理論) の命題「孤立した型はすべてのモデルで実現される」である。$\square$
$L$ が可算、$T$ が無限のモデルをもつ完全な理論で、孤立していない完全型 $p\in S_n(T)$ があるとする。このとき、$p$ を実現する可算無限なモデルと、$p$ を省略する可算無限なモデルがあり、両者は同型でない。
$T$ は無限のモデルをもち完全なので、各 $k$ について「少なくとも $k$ 個の元がある」という文を $T$ のすべてのモデルが満たす。よって $T$ のモデルはすべて無限である。thm-ott-main により $p$ を省略する高々可算なモデル $M$ があり、$M$ は可算無限である。一方、$p$ はあるモデル $N\models T$ の組 $\bar a$ で実現される（型(モデル理論) の命題「型の基本性質」）。初等部分モデル の定理「下向き Löwenheim–Skolem の定理」により、$\bar a$ の成分を含む可算な初等部分モデル $N_0\preccurlyeq N$ があり、$\operatorname{tp}^{N_0}(\bar a)=\operatorname{tp}^N(\bar a)=p$ なので $N_0$ は $p$ を実現する。$N_0$ も $T$ のモデルなので可算無限である。同型写像 $h\colon N_0\to M$ があれば $\operatorname{tp}^M(h(\bar a))=\operatorname{tp}^{N_0}(\bar a)=p$ となり、$M$ が $p$ を省略することに反する。$\square$
証明
$L$ に含まれない相異なる定数記号の可算集合 $C=\{d_0,d_1,d_2,\dots\}$ をとり、$L':=L\cup C$ とおく。$L'$ も可算である。$L'$ 構造 $N$ と、$C$ の元の組 $\bar e=(e_1,\dots,e_n)$ について、$\bar e^N:=(e_1^N,\dots,e_n^N)$ と書く。$L$ の論理式の真偽は、それに現れない記号の解釈によらない。とくに $T$ の文や $p_i$ の論理式の真偽は、$C$ の解釈を変えても変わらない。
証明の中心は、型を省略させる 1 歩である。ここで孤立していないという仮定を使う。
$p(x_1,\dots,x_n)$ を $T$ のもとで孤立していない $L$ の論理式の集合、$\Theta$ を $L'$ の文の有限集合で $T\cup\Theta$ が充足可能なもの、$\bar e=(e_1,\dots,e_n)$ を $C$ の元の組（同じ元が繰り返し現れてもよい）とする。このとき、ある $\varphi\in p$ について $T\cup\Theta\cup\{\lnot\varphi(\bar e)\}$ は充足可能である。
$\Theta$ の文と $\bar e$ に現れる $C$ の元を、重複なく $d'_1,\dots,d'_m$ と並べる。$\Theta$ の文の連言（$\Theta=\emptyset$ なら恒真な文）の $d'_l$ を新しい変数 $z_l$ に替えた $L$ の論理式を $\theta(z_1,\dots,z_m)$ とし、$e_j=d'_{s(j)}$ となる $s(j)$ をとる。
$$
\psi(\bar x):=\exists z_1\cdots\exists z_m\Bigl(\theta(\bar z)\land\bigwedge_{j=1}^nx_j=z_{s(j)}\Bigr)
$$
とおく。$T\cup\Theta$ のモデル $N$ では、$z_l:=(d'_l)^N$、$x_j:=e_j^N$ が $\psi$ の中身を満たすので、$T\cup\{\exists\bar x\,\psi\}$ は充足可能である。$p$ は孤立していないので、$\psi$ は $p$ を孤立させず、ある $\varphi\in p$ について $T\not\models\forall\bar x\,(\psi\to\varphi)$ である。すなわち、あるモデル $M\models T$ と $\bar a\in M^n$ で $M\models\psi(\bar a)\land\lnot\varphi(\bar a)$ となるものがある。$\psi(\bar a)$ の証人 $\bar b\in M^m$ をとると、$M\models\theta(\bar b)$ かつ $a_j=b_{s(j)}$ である。$M$ を $L'$ 構造に広げ、$d'_l$ を $b_l$ と解釈する（$C$ のほかの元は任意の元と解釈する）。この $L'$ 構造は $T$ のモデルで、$\Theta$ の文をすべて満たし、$e_j$ を $b_{s(j)}=a_j$ と解釈しているので $\lnot\varphi(\bar e)$ も満たす。$\square$
段 1（列挙）． $L'$ は可算なので、$L'$ の文の全体を $\sigma_0,\sigma_1,\dots$ と並べられる。また $i\in\mathbb N$ と、$C$ の元の長さ $n_i$ の組 $\bar e$ の対 $(i,\bar e)$ の全体も可算なので、$(i_0,\bar e_0),(i_1,\bar e_1),\dots$ と並べる。
段 2（有限集合の列）． $L'$ の文の有限集合 $\Theta_0\subset\Theta_1\subset\cdots$ で、各 $T\cup\Theta_k$ が充足可能なものを次のように作る。$\Theta_0:=\emptyset$ とする。$\Theta_k$ ができたとき、次の 3 つの操作で $\Theta_{k+1}$ を作る。
- (a) $T\cup\Theta_k\cup\{\sigma_k\}$ が充足可能なら $\Theta':=\Theta_k\cup\{\sigma_k\}$、そうでなければ $\Theta':=\Theta_k\cup\{\lnot\sigma_k\}$ とする。後者の場合、$T\cup\Theta_k$ のモデルは $\sigma_k$ を満たさないので $\lnot\sigma_k$ を満たし、$T\cup\Theta'$ は充足可能である。
- (b) $\sigma_k\in\Theta'$ で、$\sigma_k$ が $\exists y\,\chi(y)$ の形なら、$T\cup\Theta'$ に現れない $d\in C$ をとり（$\Theta'$ は有限で $T$ に $C$ の元は現れない）、$\Theta'':=\Theta'\cup\{\chi(d)\}$ とする。そうでなければ $\Theta'':=\Theta'$ とする。$T\cup\Theta'$ のモデル $N$ では $\exists y\,\chi(y)$ が真なので、その証人 $b$ をとり $d$ の解釈だけを $b$ に替えると、$d$ は $T\cup\Theta'$ に現れないので $T\cup\Theta''$ のモデルになる。
- (c) lem-ott-step を $p:=p_{i_k}$、$\Theta:=\Theta''$、$\bar e:=\bar e_k$ に当てはめて $\varphi\in p_{i_k}$ をとり、$\Theta_{k+1}:=\Theta''\cup\{\lnot\varphi(\bar e_k)\}$ とする。
段 3（全体のモデル）． $T^\ast:=T\cup\bigcup_k\Theta_k$ の有限部分集合はある $T\cup\Theta_k$ に含まれるので充足可能であり、コンパクト性定理（コンパクト性定理(一階論理) の定理「一階論理のコンパクト性定理」）により $T^\ast$ はモデル $N$ をもつ。$N$ は次の性質をもつ：$L'$ の文 $\exists y\,\chi(y)$ が $N$ で真なら、ある $d\in C$ について $N\models\chi(d)$ である。実際、この文を $\sigma_k$ とすると、$N\models\Theta_{k+1}$ なので $\lnot\sigma_k\notin\Theta'$ であり、(a) で $\sigma_k$ が加えられ、(b) で $\chi(d)$ が加えられている。
段 4（名前のついた元の部分モデル）． $M_0:=\{d^N\mid d\in C\}\subset N$ とおく。$L$ の定数記号 $c$ について文 $\exists y\,(y=c)$ は真なので、段 3 により $c^N\in M_0$ である。$L$ の $m$ 項関数記号 $f$ と $d_{j_1},\dots,d_{j_m}\in C$ について、文 $\exists y\,(y=f(d_{j_1},\dots,d_{j_m}))$ から同様に $f^N(d_{j_1}^N,\dots,d_{j_m}^N)\in M_0$ である。よって $M_0$ は $N$ の $L'$ 部分構造の台集合になる（初等部分モデル の定義「部分構造」）。さらに、$L'$ の論理式 $\varphi(y,\bar x)$ と $\bar a\in M_0$ について、$\bar a=\bar e^N$ となる $C$ の元の組 $\bar e$ をとれば、$N\models\exists y\,\varphi(y,\bar a)$ は文 $\exists y\,\varphi(y,\bar e)$ が真であることなので、段 3 によりある $d\in C$ で $N\models\varphi(d^N,\bar a)$ となる。初等部分モデル の定理「Tarski–Vaught の判定法」により $M_0\preccurlyeq N$ である。$M_0$ の $L$ への簡約を $M$ とすると、$T$ の文は $N$ で真なので $M$ で真であり、$M\models T$、$\lvert M\rvert\le\lvert C\rvert=\aleph_0$ である。
段 5（省略）． $i\in\mathbb N$ と $\bar a\in M^{n_i}$ をとり、$\bar a=\bar e^N$ となる組 $\bar e$ を選ぶ。$(i,\bar e)=(i_k,\bar e_k)$ となる $k$ があり、(c) によりある $\varphi\in p_i$ について $\lnot\varphi(\bar e)\in\Theta_{k+1}$ である。よって $N\models\lnot\varphi(\bar a)$ で、$M_0\preccurlyeq N$ と $\varphi$ が $L$ の論理式であることから $M\models\lnot\varphi(\bar a)$ である。$\bar a$ は $p_i$ を実現しないので、$M$ はすべての $p_i$ を省略する。$\square$
段 4 で作ったモデル $M$ は、すべての元が $C$ のどれかの記号の値になっている。段 2 の (a)・(b) だけを行えば、この方法はコンパクト性定理から高々可算なモデルを作る方法になる。(c) を挟むことで、各組 $\bar e$ に「$p_i$ のどれかの論理式を満たさない」という約束を前もって書き込んでいる。
例と応用
$L$ を可算な言語、$\{c_k\mid k\in\mathbb N\}\subset L$ を定数記号、$T$ を充足可能な $L$ の理論とする。$T\cup\{\exists x\,\varphi(x)\}$ を充足可能にする $L$ の論理式 $\varphi(x)$ ごとに、ある $k$ について $T\cup\{\varphi(c_k)\}$ が充足可能であるとする。このとき、すべての元がある $c_k$ の値であるような $T$ のモデルがある。
$p(x):=\{x\neq c_k\mid k\in\mathbb N\}$ とおく。$\varphi$ が $p$ を孤立させるなら、すべての $k$ について $T\models\forall x\,(\varphi\to x\neq c_k)$、すなわち $T\cup\{\varphi(c_k)\}$ は充足可能でなく、仮定に反する。よって $p$ は孤立せず、thm-ott-main により $p$ を省略するモデルがある。そのモデルの元 $a$ は $p$ を実現しないので、ある $k$ について $a=c_k$ である。$\square$
仮定は「$T$ と矛盾しない性質は、名前のついたある元がもちうる」という条件である。結論のモデルでは、どの元も定数記号で名指しできる。
標数 $0$ の代数閉体の理論 $\mathrm{ACF}_0$ は完全で、$\mathbb Q$ 上超越的な元の型 $p(x)\in S_1(\mathrm{ACF}_0)$（$p$ は 0 でない整数係数多項式 $g$ についての $g(x)\neq0$ をすべて含む）は孤立していない（この型がただ 1 つであることは 安定性理論 の例「標数 0 の代数閉体」で $A=\emptyset$ とした場合にあたる）。実際、$\mathbb Q$ の代数閉包 $\overline{\mathbb Q}$ は $p$ を省略するので、型(モデル理論) の命題「孤立した型はすべてのモデルで実現される」により孤立していない。cor-ott-two-models の 2 つのモデルは、たとえば $\overline{\mathbb Q}$ と $\overline{\mathbb Q(t)}$（$t$ は超越元）である。
$\mathrm{ACF}_0$ の完全性は 量化記号消去 の系「代数閉体の理論の帰結」にある。この例のように、あるモデルが型を省略することが分かれば、孤立していないことが計算なしに従う。逆向きに、孤立しないことから省略するモデルの存在を導くのが thm-ott-main である。
thm-ott-main の「高々可算なモデル」を「濃度 $\kappa$ のモデル」（$\kappa$ は非可算）に替えることはできない。型(モデル理論) の例「名前のついた元の外にある元の型」の理論 $T_c$ と型 $p=\{x\neq c_k\mid k\in\mathbb N\}$ では、$p$ は孤立していないが、非可算なモデルでは名前のついた元が可算個しかないので、名前のない元が $p$ を実現する。
反例：条件を外すと成り立たない
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 言語が可算 | $L=\{c_\alpha\mid\alpha<\omega_1\}\cup\{d_k\mid k\in\mathbb N\}$、$T=\{c_\alpha\neq c_\beta\mid\alpha\neq\beta\}$、$p=\{x\neq d_k\mid k\in\mathbb N\}$ | $p$ を省略するモデルがあること |
| 型が孤立していない | $T_c$ と $p=\{x=c_0\}$ | $p$ を省略するモデルがあること |
| 型が可算個 | 1 項関係記号 $P_0,P_1,\dots$ の理論 $T_P$ と、$\sigma\in\{0,1\}^{\mathbb N}$ ごとの型 $p_\sigma$ の全体 | すべての型を同時に省略するモデルがあること |
1 行目：$T$ のモデルには相異なる元 $c_\alpha$ が $\aleph_1$ 個あり、$d_k$ の値は可算個なので、ある $c_\alpha$ はどの $d_k$ とも異なり $p$ を実現する。$p$ が孤立しないこと：$T\cup\{\exists x\,\varphi\}$ が充足可能な $\varphi(x)$ について、モデル $M$ と $M\models\varphi(a)$ をとり、$\varphi$ に現れない $d_m$ の解釈を $a$ に替える。$T$ は $d_k$ に触れないので $T$ のモデルのままで、$\varphi(a)$ も保たれ、$a=d_m$ となる。よって $T\not\models\forall x\,(\varphi\to x\neq d_m)$ である。
2 行目：$T_c$ は rem-ott-countable の理論で、言語は可算である。$x=c_0$ は $p$ を孤立させ、$T_c$ の各モデルで $c_0$ の値が $p$ を実現する。
3 行目：言語 $\{P_i\mid i\in\mathbb N\}$ で、互いに交わらない有限集合 $I,J\subset\mathbb N$ と $m\ge1$ ごとに「$\bigwedge_{i\in I}P_i(x)\land\bigwedge_{j\in J}\lnot P_j(x)$ を満たす元が $m$ 個以上ある」という文を並べた理論を $T_P$ とする。$\{0,1\}^{\mathbb N}\times\mathbb N$ で $P_i(\tau,l)$ を $\tau(i)=1$ と定めた構造がモデルなので $T_P$ は充足可能で、言語は可算である。$P_i^1:=P_i$、$P_i^0:=\lnot P_i$ として $p_\sigma(x):=\{P_i^{\sigma(i)}(x)\mid i\in\mathbb N\}$ とおく。どのモデルのどの元 $a$ も、$\sigma(i)=1\iff P_i(a)$ で定まる $p_\sigma$ を実現するので、すべての $p_\sigma$ を省略するモデルはない。各 $p_\sigma$ は孤立していない：$\varphi(x)$ で $T_P\cup\{\exists x\,\varphi\}$ が充足可能なものについて、$M\models T_P$、$M\models\varphi(a)$ をとり、$\varphi$ に現れない $P_i$ を選ぶ。$a$ が $P_i$ に属するかどうかだけを入れ替えた構造 $M'$ も、各パターンを満たす元が無限個のままなので $T_P$ のモデルで、$M'\models\varphi(a)$ である。$M$ と $M'$ の一方では $P_i^{\sigma(i)}(a)$ が偽なので、$T_P\not\models\forall x\,(\varphi\to P_i^{\sigma(i)}(x))$ である。型の個数 $2^{\aleph_0}$ は可算でない。
関連項目
- 前提: 型(モデル理論), コンパクト性定理(一階論理), 初等部分モデル, 完全な理論
- 比較: Löwenheim–Skolemの定理, Gödelの完全性定理
- 直後に読む: Ryll-Nardzewskiの定理
- 発展: Morleyの範疇性定理, 安定性理論
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
