型(モデル理論)

要点：型を実現する組をとれば、どの主張もそのモデルでの真偽の言い換えになる。

要点：有限部分集合の連言を $\theta$ とすると、$\exists\bar x\,\theta$ が $\operatorname{Th}(M_A)$ に属するかどうかの問題になる。

Hausdorff． $p\neq q$ なら $\varphi\in p\setminus q$ があり、完全性から $\lnot\varphi\in q$ である。$p\in[\varphi]$、$q\in[\lnot\varphi]$ で、この 2 つの開集合は交わらない。開かつ閉な集合で 2 点が分けられたので、コンパクト性を示せば Stone双対性 の定理「Stone 空間の同値な条件」により 1 が従う。
コンパクト． 開基の元による被覆に有限部分被覆があることを示せば十分である。$\{[\varphi_i]\}_{i\in I}$ が $S_n(T)$ を覆い、有限部分被覆をもたないとする。$\Sigma:=\{\lnot\varphi_i\mid i\in I\}$ とおく。有限集合 $F\subset I$ について $\bigcup_{i\in F}[\varphi_i]\neq S_n(T)$ なので、そこに入らない $q\in S_n(T)$ があり、完全性から $\lnot\varphi_i\in q$（$i\in F$）である。prop-type-basic の 2 で $q$ を実現する組を考えると、$T\cup\{\lnot\varphi_i(\bar c)\mid i\in F\}$ は充足可能である。したがってコンパクト性定理により $\Sigma$ は $T$ の型であり、prop-type-basic の 3 により $\Sigma\subset p$ となる $p\in S_n(T)$ がある。$p$ はどの $\varphi_i$ も含まないので、どの $[\varphi_i]$ にも入らず、被覆であることに反する。
2． $[\varphi]$ が開かつ閉であることは上で見た。逆に $K$ を開かつ閉な集合とする。$K$ はコンパクト空間の閉集合なのでコンパクトであり、開集合なので開基の元の和である。有限個の $[\varphi_1],\dots,[\varphi_m]$ で覆われるので $K=[\varphi_1\lor\cdots\lor\varphi_m]$ である（$K=\emptyset$ なら $K=[\varphi\land\lnot\varphi]$）。
3． $T\models\forall\bar x\,(\varphi\to\psi)$ なら、prop-type-basic の 4 により $[\varphi]\subset[\psi]$ である。そうでなければ、あるモデル $M\models T$ と $\bar a\in M^n$ で $M\models\varphi(\bar a)\land\lnot\psi(\bar a)$ となるものがあり、$\operatorname{tp}^M(\bar a)\in[\varphi]\setminus[\psi]$ である。$\square$

thm-type-stone の 2・3 により、類と $S_n(T)$ の開かつ閉な集合は 1 対 1 に対応する。$S_n(T)$ が $k$ 点の有限集合なら、Hausdorff 空間の有限集合として離散なので、すべての部分集合が開かつ閉であり、類は $2^k$ 個である。逆に類が $m$ 個なら、型 $p$ は「どの類の論理式を含むか」で決まるので（$\varphi\in p$ と $T$ のもとで同値な $\psi$ について $\psi\in p$）、$S_n(T)$ は $2^m$ 個以下である。$\square$

1 ⇒ 2． $\varphi$ が $p$ を孤立させるとする。$\lnot\varphi\in p$ なら $T\models\forall\bar x\,(\varphi\to\lnot\varphi)$、すなわち $T\models\lnot\exists\bar x\,\varphi$ となり、$T\cup\{\exists\bar x\,\varphi\}$ の充足可能性に反する。よって $\varphi\in p$ である。$q\in[\varphi]$ なら、prop-type-basic の 4 により $p\subset q$ であり、$p$ の完全性から $q=p$ である（$\psi\in q\setminus p$ なら $\lnot\psi\in p\subset q$）。
2 ⇒ 1． $\varphi\in p$ で $[\varphi]=\{p\}$ とする。$p$ を実現する組があるので $T\cup\{\exists\bar x\,\varphi\}$ は充足可能である。$\psi\in p$ について $[\varphi]=\{p\}\subset[\psi]$ なので、thm-type-stone の 3 により $T\models\forall\bar x\,(\varphi\to\psi)$ である。
2 ⇔ 3． $\{p\}$ が開集合であることは、$p$ を含む開基の元 $[\varphi]$ で $[\varphi]\subset\{p\}$ となるものがあることと同値である。$\square$

$\varphi$ が $p$ を孤立させるとする。$T\cup\{\exists\bar x\,\varphi\}$ は充足可能なので $T\not\models\lnot\exists\bar x\,\varphi$ であり、$T$ が完全なので $T\models\exists\bar x\,\varphi$ である。$M\models T$ について $M\models\varphi(\bar a)$ となる $\bar a$ をとると、$\psi\in p$ ごとに $T\models\forall\bar x\,(\varphi\to\psi)$ から $M\models\psi(\bar a)$ である。$\square$

並び方 $\sigma$ に対し、それを表す原子論理式とその否定の連言を $\chi_\sigma(\bar x)$ とする。$\sigma$ は全順序として矛盾しないので、$(\mathbb Q,<)$ に $\sigma$ のとおりに並ぶ組があり、$\mathrm{DLO}\cup\{\exists\bar x\,\chi_\sigma\}$ は充足可能である。言語 $\{<\}$ の原子論理式は $x_i< x_j$ と $x_i=x_j$ だけなので、量化記号のない論理式 $\psi(\bar x)$ の真偽は並び方で決まり、$\psi$ が $\sigma$ のもとで真なら $\mathrm{DLO}\models\forall\bar x\,(\chi_\sigma\to\psi)$ である。量化記号消去 の定理「DLO の量化記号消去」により、どの $\varphi(\bar x)$ も量化記号のない論理式と $\mathrm{DLO}$ のもとで同値なので、$\chi_\sigma$ は 1 つの型 $p_\sigma$ を孤立させ、$[\chi_\sigma]=\{p_\sigma\}$ である（prop-type-isolated-point）。どの型も、どれか 1 つの $\chi_\sigma$ を含むので、型は $p_\sigma$ で尽きる。3 変数の並び方は、3 つとも相異なるもの 6 通り、ちょうど 2 つが等しいもの 6 通り、3 つとも等しいもの 1 通りの 13 通りである。$\square$

要点：量化記号消去により、パラメータ付きの論理式の真偽は $x$ と有限個の有理数の大小だけで決まる。

要点：完全性は Łoś–Vaught の判定法から、孤立しないことは名前のない元に新しい名前を付け替えることから従う。