決定可能な理論

段 1（意味の上の演繹定理）． 文 $\varphi$ について、$T\cup\{\sigma\}\models\varphi\iff T\models\sigma\to\varphi$ である。実際、$T\cup\{\sigma\}\models\varphi$ とし、$\mathcal M$ を $T$ のモデルとする。$\mathcal M\models\sigma$ なら $\mathcal M$ は $T\cup\{\sigma\}$ のモデルなので $\mathcal M\models\varphi$ であり、どちらの場合も $\mathcal M\models\sigma\to\varphi$ である。逆に $T\models\sigma\to\varphi$ とし、$\mathcal M$ を $T\cup\{\sigma\}$ のモデルとすると、$\mathcal M\models\sigma\to\varphi$ と $\mathcal M\models\sigma$ から $\mathcal M\models\varphi$ である。
段 2（番号の上の計算）． 文の番号の集合を $\mathrm{Sent}$ とする。関数 $g\colon\mathbb{N}\to\mathbb{N}$ を、$n=\ulcorner\varphi\urcorner\in\mathrm{Sent}$ なら $g(n):=\ulcorner\sigma\to\varphi\urcorner$、$n\notin\mathrm{Sent}$ なら $g(n):=n$ と定める。$\mathrm{Sent}$ が決定可能で、含意を作る操作が番号の上で計算できるので、$g$ は計算可能な全域関数である。段 1 により、すべての $n$ について
$$ n\in\operatorname{Cn}(T\cup\{\sigma\})\iff g(n)\in\operatorname{Cn}(T) $$
である（$n\notin\mathrm{Sent}$ のときは両辺とも偽）。$\operatorname{Cn}(T\cup\{\sigma\})$ の特性関数は、$\operatorname{Cn}(T)$ の特性関数と $g$ の合成なので計算可能である（計算可能な関数が合成で閉じていることは、停止問題 の記事の (A) で述べられている μ再帰関数との一致による）。$\square$

Robinson の算術 Q は 8 個の文 $Q_1,\dots,Q_8$ を公理とする理論である（OLT26 Definition 33.5、p. 524）。Q は決定可能でない（同 Theorem 36.1、p. 573。この記事では証明しない）。$\sigma:=Q_1\land\cdots\land Q_8$ とおくと $\operatorname{Cn}(\{\sigma\})=\operatorname{Cn}(\{Q_1,\dots,Q_8\})$ なので、$\emptyset\cup\{\sigma\}$ は決定不能である。prop-dt-finite-extension の対偶により $\emptyset$、すなわち $L_A$ の妥当な文の全体は決定不能である。$\square$

構造の理論なので完全である。公理化可能なら、完全な理論 の記事の定理「決定可能な公理系をもつ完全な理論は決定可能」により決定可能になる。しかし真の算術は決定可能でない（OLT26 Corollary 36.6、p. 576。この記事では証明しない）。$\square$

$T\models\varphi\leftrightarrow\varphi^\ast$ なので、$T$ のどのモデルでも $\varphi$ と $\varphi^\ast$ の真偽は一致し、$T\models\varphi\iff T\models\varphi^\ast$ である。$\varphi$ が与えられたら $\varphi^\ast$ を計算し、量化記号のない文についての判定を当てはめればよい。2 つの計算可能な手順の合成なので計算可能である。$\square$

$M=\{a_1,\dots,a_m\}$ とする。$L$ は有限なので、$\mathcal M$ は有限の表で与えられる。各関係記号の解釈は $M^r$ の部分集合、各関数記号の解釈は $M^r\to M$ の写像、各定数記号の解釈は $M$ の元であり、どれも有限個のデータである。
論理式 $\varphi$ と、$\varphi$ の自由変数から $M$ への割り当て $s$ を入力として、$\mathcal M\models\varphi[s]$ の真偽を返す手順 $\operatorname{Sat}(\varphi,s)$ を、$\varphi$ の組み立てに沿って次のように定める。

• 項の値は、変数なら $s$ の値、定数記号なら表の元、$f(t_1,\dots,t_r)$ なら $t_i$ の値を先に計算して $f$ の表を引く。
• 原子論理式 $R(t_1,\dots,t_r)$、$t_1=t_2$ は、項の値を計算して $R$ の表を引くか、2 つの値を比べる。
• $\lnot\psi$、$\psi\land\chi$ などは、$\operatorname{Sat}(\psi,s)$、$\operatorname{Sat}(\chi,s)$ の値を真理値表で組み合わせる。
• $\exists x\,\psi$ は、$x$ に $a_1,\dots,a_m$ を順に割り当てて $\operatorname{Sat}(\psi,s[x\mapsto a_j])$ を $m$ 回計算し、どれかが真なら真とする。$\forall x\,\psi$ はすべてが真なら真とする。
  各段で呼び出す $\operatorname{Sat}$ は、より短い論理式についてのもので、呼び出しは有限回なので、論理式の長さに関する帰納法により手順は必ず止まる。返す値が $\mathcal M\models\varphi[s]$ の真偽と一致することは、各段が 一階述語論理 の記事の定義「項の値」「充足関係」の各項をそのままなぞっていることから、同じ帰納法で分かる（$M$ が有限なので、$\exists$ の定義の「ある元」は $m$ 個の元を調べ尽くすことで確かめられる）。
  番号 $n$ が与えられたら、$n\in\mathrm{Sent}$ かを判定し、文 $\sigma$ なら空の割り当てで $\operatorname{Sat}(\sigma,\emptyset)$ を計算すればよい。これで $\operatorname{Th}(\mathcal M)$ の特性関数を計算する手順が得られた。$\square$

$M$ は空でないので、ある色 $C_\gamma$ は空でなく、そこから $1$ 個以上の元が選ばれる。よって $M'$ は空でない。$\lvert M'\rvert\le2^kq$ は作り方から明らかである。主張を $\varphi$ の組み立てに関する帰納法で示す。論理式は $\lnot,\land,\exists$ から作られるとしてよい（$\forall x\,\psi$ は $\lnot\exists x\,\lnot\psi$ と同値で、量化記号の深さも変わらない）。
原子論理式． $P_i(x_j)$ と $x_i=x_j$ の真偽は、$\mathcal M'$ が部分構造なので $\mathcal M'$ と $\mathcal M$ で一致する。
結合子． $\lnot\psi$、$\psi\land\chi$ では、$\psi,\chi$ の量化記号の深さは $\varphi$ 以下なので、帰納法の仮定がそのまま使える。
存在量化． $\varphi=\exists y\,\psi$ とし、束縛変数を付け替えて $y$ は $x_1,\dots,x_l$ と異なるとする（一階述語論理 の記事の系「束縛変数の付け替え」）。$\psi$ の自由変数は $x_1,\dots,x_l,y$ の $l+1$ 個の中にあり、$\operatorname{qr}(\psi)+(l+1)=\operatorname{qr}(\varphi)+l\le q$ なので、$\psi$ には帰納法の仮定が使える。
$\mathcal M'\models\varphi[\bar a]$ なら、ある $b\in M'$ で $\mathcal M'\models\psi[\bar a,b]$ であり、帰納法の仮定で $\mathcal M\models\psi[\bar a,b]$、よって $\mathcal M\models\varphi[\bar a]$ である。
逆に $\mathcal M\models\psi[\bar a,b]$ となる $b\in M$ があるとする。$b\in M'$ なら帰納法の仮定で $\mathcal M'\models\psi[\bar a,b]$ である。$b\notin M'$ とする。このとき $b$ の色 $\gamma$ の集合 $C_\gamma$ は $q$ 個より多くの元をもち、$M'\cap C_\gamma$ はちょうど $q$ 個の元をもつ。$\operatorname{qr}(\varphi)\ge1$ なので $l\le q-1$ であり、$M'\cap C_\gamma$ の元で $a_1,\dots,a_l$ のどれとも異なる $b'$ がある。
$b$ と $b'$ を入れ替え、ほかの元を動かさない写像 $\tau\colon M\to M$ は全単射で、$b,b'$ が同じ色なので各 $P_i$ の解釈を保つ。すなわち $\tau$ は $\mathcal M$ の自己同型である。$b\notin M'$ なので $b\ne a_i$ であり、$b'\ne a_i$ なので、$\tau(a_i)=a_i$ である。一階述語論理 の記事の定理「同型補題」により
$$ \mathcal M\models\psi[\bar a,b]\iff\mathcal M\models\psi[\tau(\bar a),\tau(b)]=\psi[\bar a,b'] $$
であり、$b'\in M'$ なので帰納法の仮定で $\mathcal M'\models\psi[\bar a,b']$、よって $\mathcal M'\models\varphi[\bar a]$ である。$\square$

1：$\sigma$ に現れる関係記号を $P_1,\dots,P_k$ とし、$L_0:=\{P_1,\dots,P_k\}$ とする。$\mathcal M\models\sigma$ とすると、$\sigma$ の真偽は $L_0$ の記号の解釈だけで決まるので（構造(モデル) の記事の定義「簡約と拡張」の後の段落）、$L_0$ への簡約 $\mathcal M|_{L_0}$ も $\sigma$ を満たす。lem-dt-shrink により、$2^kq$ 個以下の元からなる $L_0$ 構造 $\mathcal M'$ で $\mathcal M'\models\sigma$ となるものがある。$L\setminus L_0$ の記号を空集合と解釈して $\mathcal M'$ を $L$ 構造に拡張すれば、それが求めるモデルである。
2：文 $\sigma$ が妥当であることは、$\lnot\sigma$ がモデルをもたないことと同値である。$\lnot\sigma$ に現れる記号と量化記号の深さは $\sigma$ と同じなので、1 により、$\lnot\sigma$ がモデルをもつのは、台集合が $\{1,\dots,j\}$（$1\le j\le2^kq$）で $P_1,\dots,P_k$ をその部分集合と解釈した $L_0$ 構造のどれかが $\lnot\sigma$ を満たすときに限る。そのような構造は有限個（$j$ ごとに $2^{jk}$ 個）であり、すべて書き出せる。各構造で $\lnot\sigma$ が真かどうかは、thm-dt-finite-structure の証明の手順 $\operatorname{Sat}$ で計算できる。$\sigma$ の番号から $k$、$q$、$P_1,\dots,P_k$ は計算できるので、これらを順に調べ、どれも $\lnot\sigma$ を満たさなければ $\sigma$ は妥当、どれかが満たせば妥当でないと答える手順が得られる。$\square$