Churchの定理(一階論理の決定不能性)
概要
Churchの定理(一階論理の決定不能性)（Church's theorem）とは、一階述語論理の文が妥当（すべての構造で真）であるかどうかを判定する機械的な手順は存在しないという定理であり、Hilbert の決定問題に否定的に答える。Church と Turing がほぼ同時に独立に示したので Church–Turing の定理ともよばれる。Turing 機械と入力から、機械が停止するときちょうど妥当になる文を作ると、停止問題の決定不能性が妥当性の判定へ移り、有限個の記号からなるある言語で妥当な文の全体が決定可能でないことが従う。完全性定理により妥当な文の全体は半決定可能なので、充足可能な文の全体は半決定可能でもない。
前提知識: 一階述語論理, Turing機械, 停止問題, Gödelの完全性定理
一階述語論理の文が 妥当、すなわちすべての構造で真であるかどうかを、機械的な手順で必ず判定できるだろうか。この問いは歴史的に単に 決定問題（Entscheidungsproblem）とよばれてきた。答えは否定的である。Church と Turing がほぼ同時に独立に示したこの結果を Churchの定理（Church's theorem）または Church–Turingの定理 という（OLT26 §32.1、p. 496）。
Gödelの完全性定理 により、妥当な文は証明をもち、証明を順に数え上げればいつか見つかる。したがって妥当な文の全体は半決定可能である。Church の定理は、その逆側、すなわち「妥当でない」ことを確かめる一般的な手順はないことを述べている。
この記事では、Turing 機械 $M$ と入力 $x$ から、「$M$ が入力 $x$ で停止する」ときちょうど妥当になる一階の文 $\theta_{M,x}$ を作り、停止問題 の決定不能性を一階論理の妥当性の判定へ移す。この方法で、有限個の記号からなる言語 $L_0$ で妥当な文の全体が決定可能でないことを完全に証明する。系として、充足可能な文の全体は決定可能でないだけでなく半決定可能でもないことを示し、決定可能になる場合（命題論理、1 項関係記号だけの言語）との違いを反例の表で比べる。
記法と前提
$\mathbb{N}=\{0,1,2,\dots\}$、$\mathbb{Z}$ は整数全体とする。Turing 機械 $M=(Q,\Gamma,\sqcup,q_0,\delta)$、様相 $(q,\tau,h)$、次の様相、停止様相、入力 $x\in\mathbb{N}$ の初期様相 $(q_0,\tau_x,0)$ は Turing機械 の記事の定義「Turing 機械」「様相と計算」「Turing 機械が計算する関数」に従う。テープのマスは $\mathbb{Z}$ で番号づけられ、$\tau_x$ はマス $0,\dots,x-1$ に $1$ を書き、ほかのマスを空白 $\sqcup$ としたテープの内容である。ヘッドの向き $\mathrm{L},\mathrm{R},\mathrm{N}$ に応じて $d=-1,1,0$ だけヘッドが動き、$\delta(q,\tau(h))$ が定義されない様相が停止様相である。
決定可能・半決定可能、機械の番号 $M_e$、停止集合 $H$ と自己停止集合 $K$ は 停止問題 の記事の定義「決定可能と半決定可能」「停止問題」による。一階言語、構造、充足関係 $\mathcal M\models\varphi$、妥当な文は 一階述語論理 の記事の定義「構造」「充足関係」「モデル・妥当性・論理的帰結」による。とくに構造の台集合は空でなく、等号 $=$ はつねに論理記号として使える。文 $\sigma$ が 充足可能 であるとは、$\sigma$ を真にする構造があることをいう。$\sigma$ が妥当であることと $\lnot\sigma$ が充足可能でないことは同値である。
言語 $L$ が可算のとき、記号と論理式に Gödel 数 $\ulcorner\varphi\urcorner$ を付けておく（Gödel数化）。番号は 決定可能な理論 の記事の節「設定」と同じく、「番号が文を表すか」の判定、否定や含意を作る操作、記号列をつなげる操作が番号の上で計算できるように付ける。文の集合が決定可能（半決定可能）であるとは、番号の集合がそうであることをいう。
定義
Turing 機械 $M=(Q,\Gamma,\sqcup,q_0,\delta)$ の計算を一階の文で書き表すための言語を定める。
$M=(Q,\Gamma,\sqcup,q_0,\delta)$ を Turing 機械とする。一階言語 $L_M$ を、次の記号からなる言語とする。
- 定数記号 $0$、1 項関数記号 $\mathsf s$（後者）と $\mathsf p$（前者）、2 項関係記号 $<$。
- 状態 $q\in Q$ ごとの 2 項関係記号 $Q_q$。$Q_q(u,t)$ は「時刻 $t$ に状態 $q$ でマス $u$ を読んでいる」と読む。
- テープ記号 $a\in\Gamma$ ごとの 2 項関係記号 $S_a$。$S_a(u,t)$ は「時刻 $t$ にマス $u$ に記号 $a$ が書かれている」と読む。
$m\in\mathbb{Z}$ に対し、数項 $\overline m$ を、$\overline0:=0$、$m\ge0$ のとき $\overline{m+1}:=\mathsf s(\overline m)$、$m\le0$ のとき $\overline{m-1}:=\mathsf p(\overline m)$ で定める。
$L_M$ は有限個の記号からなる。マスの番号と時刻の両方を、同じ台集合の元で表す。
$M$ と入力 $x\in\mathbb{N}$ について、次の $L_M$ の文を定める。
- 数の公理 $A_1:=\forall u\,(u< \mathsf s(u))$、$A_2:=\forall u\,\forall v\,\forall w\,((u< v\land v< w)\to u< w)$、$A_3:=\forall u\,(\mathsf s(\mathsf p(u))=u\land\mathsf p(\mathsf s(u))=u)$。
- 初期様相 $I_x:=Q_{q_0}(0,0)\land\bigwedge_{i=0}^{x}S_{\tau_x(i)}(\overline i,0)\land\forall w\,\bigl((w< 0\lor\overline x< w)\to S_\sqcup(w,0)\bigr)$。
- 書き換えのない部分 $\varphi(u,t):=\bigwedge_{c\in\Gamma}\forall w\,\bigl(((w< u\lor u< w)\land S_c(w,t))\to S_c(w,\mathsf s(t))\bigr)$。
- 遷移 $\delta(q,a)=(q',b,D)$ が定義される組 $(q,a)\in Q\times\Gamma$ ごとに
$$ T_{q,a}:=\forall u\,\forall t\,\Bigl(\bigl(Q_q(u,t)\land S_a(u,t)\bigr)\to\bigl(Q_{q'}(\mu_D(u),\mathsf s(t))\land S_b(u,\mathsf s(t))\land\varphi(u,t)\bigr)\Bigr). $$
ここで $\mu_{\mathrm L}(u):=\mathsf p(u)$、$\mu_{\mathrm R}(u):=\mathsf s(u)$、$\mu_{\mathrm N}(u):=u$ とする。 - $\alpha_{M,x}$ を $A_1,A_2,A_3,I_x$ とすべての $T_{q,a}$ の連言とする。
- 停止 $X:=\{(q,a)\in Q\times\Gamma\mid\delta(q,a)\text{ は定義されない}\}$ とし、$\eta_M:=\exists u\,\exists t\,\bigvee_{(q,a)\in X}\bigl(Q_q(u,t)\land S_a(u,t)\bigr)$ とおく。$X=\emptyset$ のときは $\eta_M:=\exists u\,\lnot(u=u)$ とする。
- $\theta_{M,x}:=\alpha_{M,x}\to\eta_M$ とおく。
$Q\times\Gamma$ は有限集合なので、連言と選言は有限個の文の連言と選言である。入力 $x$ は $I_x$ にだけ現れる。$I_x$ の 2 つ目の連言で $i=x$ のマスは空白であり（$\tau_x(x)=\sqcup$）、3 つ目の連言はそれより外のマスがすべて空白であることを述べる。$\alpha_{M,x}$ は「時刻 $0$ に初期様相にあり、各時刻に遷移関数に従って 1 ステップ進む」こと、$\eta_M$ は「ある時刻に停止様相にある」ことを述べている。
- 遷移関数 $\delta$ がどこでも定義されない機械 $M$ では、$X=Q\times\Gamma$ で、$\alpha_{M,x}$ は $A_1,A_2,A_3,I_x$ の連言である。$I_x$ の連言 $Q_{q_0}(0,0)$ と $S_{\tau_x(0)}(\overline0,0)$ から $Q_{q_0}(0,0)\land S_{\tau_x(0)}(0,0)$ が従い、$(q_0,\tau_x(0))\in X$ なので $\eta_M$ が従う。よって $\theta_{M,x}$ は妥当である。実際 $M$ はどの入力でも $0$ ステップで停止する。
- 状態が $q_0$ だけで、すべての $a\in\Gamma$ について $\delta(q_0,a)=(q_0,a,\mathrm R)$ とする機械 $M$ は、右へ進み続けて停止しない。$X=\emptyset$ なので $\eta_M=\exists u\,\lnot(u=u)$ はどの構造でも偽であり、$\theta_{M,x}$ が妥当であることは $\alpha_{M,x}$ がモデルをもたないことと同じになる。後の lem-ch-model の構造 $\mathfrak N_{M,x}$ が $\alpha_{M,x}$ のモデルなので、$\theta_{M,x}$ は妥当でない。
計算を文に移す
数項は、数の公理を満たす構造の中で整数の順序をそのまま写す。
$\mathcal A$ を $A_1,A_2,A_3$ を満たす $L_M$ 構造とし、数項 $\overline m$ の値を $\overline m^{\mathcal A}$ と書く。このとき、すべての $m,k\in\mathbb{Z}$ について次が成り立つ。
- $\mathsf s^{\mathcal A}(\overline m^{\mathcal A})=\overline{m+1}^{\mathcal A}$、$\mathsf p^{\mathcal A}(\overline m^{\mathcal A})=\overline{m-1}^{\mathcal A}$。
- $m< k$ なら $\overline m^{\mathcal A}<^{\mathcal A}\overline k^{\mathcal A}$。
1：$m\ge0$ のとき前半は数項の定義そのものである。$m< 0$ のとき $\overline m=\mathsf p(\overline{m+1})$ なので、$A_3$ の $\mathsf s(\mathsf p(u))=u$ から $\mathsf s^{\mathcal A}(\overline m^{\mathcal A})=\overline{m+1}^{\mathcal A}$ である。後半も同様で、$m\le0$ のときは定義そのもの、$m>0$ のときは $\overline m=\mathsf s(\overline{m-1})$ と $A_3$ の $\mathsf p(\mathsf s(u))=u$ による。
2：1 と $A_1$ から、すべての $m$ について $\overline m^{\mathcal A}<^{\mathcal A}\mathsf s^{\mathcal A}(\overline m^{\mathcal A})=\overline{m+1}^{\mathcal A}$ である。$m< k$ なら、$\overline m^{\mathcal A}<^{\mathcal A}\overline{m+1}^{\mathcal A}<^{\mathcal A}\cdots<^{\mathcal A}\overline k^{\mathcal A}$ を $A_2$ でつなげばよい。$\square$
$A_1,A_2$ には $<$ の非反射性が入っていないので、$\overline m^{\mathcal A}$ どうしが相異なるとは限らない。書き換えのない部分 $\varphi$ を $w\neq u$ ではなく $w< u\lor u< w$ で書いたのは、この 2 で足りるようにするためである。
$M$ が入力 $x$ の初期様相から停止するなら、$\theta_{M,x}$ は妥当である。
$M$ の入力 $x$ からの計算を $C_0,C_1,\dots,C_N$ とし、$C_N$ を停止様相、$C_n=(q_n,\tau_n,h_n)$ とする。$\mathcal A$ を任意の $L_M$ 構造とする。$\mathcal A\not\models\alpha_{M,x}$ なら $\mathcal A\models\theta_{M,x}$ なので、$\mathcal A\models\alpha_{M,x}$ とし、$\mathcal A\models\eta_M$ を示す。$0\le n\le N$ についての次の主張 $(\mathrm P_n)$ を帰納法で示す。
$$
(\mathrm P_n)\qquad\mathcal A\models Q_{q_n}(\overline{h_n},\overline n),\qquad\text{すべての }i\in\mathbb{Z}\text{ について }\mathcal A\models S_{\tau_n(i)}(\overline i,\overline n).
$$
詳しい証明を開く
$n=0$． $q_0$、$h_0=0$、$\tau_0=\tau_x$ である。$I_x$ の連言から $Q_{q_0}(0,0)$ と、$0\le i\le x$ での $S_{\tau_x(i)}(\overline i,0)$ が成り立つ。$i< 0$ なら lem-ch-numerals の 2 から $\overline i^{\mathcal A}<^{\mathcal A}0^{\mathcal A}$、$i>x$ なら $\overline x^{\mathcal A}<^{\mathcal A}\overline i^{\mathcal A}$ なので、$I_x$ の 3 つ目の連言から $S_\sqcup(\overline i,0)$ が成り立ち、このとき $\tau_x(i)=\sqcup$ である。
$n$ から $n+1$ へ（$n< N$）． $C_n$ は停止様相でないので、$a:=\tau_n(h_n)$ について $\delta(q_n,a)=(q',b,D)$ が定義され、$C_{n+1}=(q',\tau',h_n+d)$ である（$\tau'(h_n)=b$、$i\ne h_n$ では $\tau'(i)=\tau_n(i)$）。$\alpha_{M,x}$ の連言 $T_{q_n,a}$ の $u,t$ に $\overline{h_n}^{\mathcal A},\overline n^{\mathcal A}$ を入れると、$(\mathrm P_n)$ から前件 $Q_{q_n}(\overline{h_n},\overline n)\land S_a(\overline{h_n},\overline n)$ が成り立つので、次の 3 つが成り立つ。
(i) $Q_{q'}(\mu_D(\overline{h_n}),\mathsf s(\overline n))$。lem-ch-numerals の 1 により、$\mu_D(\overline{h_n})$ の値は $\overline{h_n+d}^{\mathcal A}$、$\mathsf s(\overline n)$ の値は $\overline{n+1}^{\mathcal A}$ なので、これは $Q_{q_{n+1}}(\overline{h_{n+1}},\overline{n+1})$ である。
(ii) $S_b(\overline{h_n},\overline{n+1})$。これは $i=h_n$ での $S_{\tau_{n+1}(i)}(\overline i,\overline{n+1})$ である。
(iii) $\varphi(\overline{h_n},\overline n)$。$i\ne h_n$ なら $i< h_n$ か $h_n< i$ なので、lem-ch-numerals の 2 により $\overline i^{\mathcal A}<^{\mathcal A}\overline{h_n}^{\mathcal A}$ か $\overline{h_n}^{\mathcal A}<^{\mathcal A}\overline i^{\mathcal A}$ である。$(\mathrm P_n)$ の $S_{\tau_n(i)}(\overline i,\overline n)$ と $\varphi$ の $c=\tau_n(i)$ の連言から $S_{\tau_n(i)}(\overline i,\overline{n+1})$ を得る。$\tau_{n+1}(i)=\tau_n(i)$ なので、これが求める式である。
以上で $(\mathrm P_{n+1})$ が示された。
結論． $(\mathrm P_N)$ から $\mathcal A\models Q_{q_N}(\overline{h_N},\overline N)\land S_{a_N}(\overline{h_N},\overline N)$（$a_N:=\tau_N(h_N)$）である。$C_N$ は停止様相なので $(q_N,a_N)\in X$ であり、$\eta_M$ の選言の 1 つが $u,t$ を $\overline{h_N}^{\mathcal A},\overline N^{\mathcal A}$ として成り立つ。よって $\mathcal A\models\eta_M$ である。$\mathcal A$ は任意だったので $\theta_{M,x}$ は妥当である。$\square$
逆向きには、計算そのものを構造にする。
$M$ と入力 $x$ について、$L_M$ 構造 $\mathfrak N_{M,x}$ を次で定める。台集合は $\mathbb{Z}$、$0$ は $0$、$\mathsf s$ は $m\mapsto m+1$、$\mathsf p$ は $m\mapsto m-1$、$<$ は通常の大小とする。入力 $x$ からの計算を $C_0,C_1,\dots$（停止すれば有限列）、$C_n=(q_n,\tau_n,h_n)$ とし、
$$
Q_q^{\mathfrak N}:=\{(h_n,n)\mid C_n\text{ が存在し }q_n=q\},\qquad S_c^{\mathfrak N}:=\{(i,n)\mid C_n\text{ が存在し }\tau_n(i)=c\}
$$
とおく。このとき $\mathfrak N_{M,x}\models\alpha_{M,x}$ である。さらに、$M$ が入力 $x$ で停止しないなら $\mathfrak N_{M,x}\not\models\eta_M$ である。
$A_1,A_2,A_3$ は $\mathbb{Z}$ で成り立つ。$C_0=(q_0,\tau_x,0)$ なので $I_x$ が成り立つ（$w< 0$ または $w>x$ のマス $w$ は $\tau_x(w)=\sqcup$）。
詳しい証明を開く
$T_{q,a}$ を確かめる。$\delta(q,a)=(q',b,D)$ とし、$(m,n)\in Q_q^{\mathfrak N}$ かつ $(m,n)\in S_a^{\mathfrak N}$ とする。$Q_q^{\mathfrak N}$ の定義から $C_n$ が存在して $m=h_n$、$q_n=q$ であり、$\tau_n(h_n)=a$ である。$\delta(q_n,\tau_n(h_n))$ が定義されるので $C_n$ は停止様相でなく、$C_{n+1}=(q',\tau',h_n+d)$ が存在する。よって $(h_n+d,n+1)\in Q_{q'}^{\mathfrak N}$、$(h_n,n+1)\in S_b^{\mathfrak N}$ であり、$w\ne h_n$ では $\tau'(w)=\tau_n(w)$ なので $\varphi(h_n,n)$ も成り立つ。
$M$ が停止しないとし、$(m,n)\in Q_q^{\mathfrak N}\cap S_a^{\mathfrak N}$ とすると、上と同じく $m=h_n$、$q=q_n$、$a=\tau_n(h_n)$ である。$C_n$ は停止様相でないので $(q,a)\notin X$ である。よって $\eta_M$ の選言はどの $(m,n)$ でも成り立たず（$X=\emptyset$ のときは $\eta_M$ はもともと偽）、$\mathfrak N_{M,x}\not\models\eta_M$ である。$\square$
2 つの補題を合わせると、次が得られる。
すべての Turing 機械 $M$ と入力 $x\in\mathbb{N}$ について、$\theta_{M,x}$ が妥当であることと、$M$ が入力 $x$ で停止することは同値である。
停止するなら妥当であることは lem-ch-halts-valid である。停止しないなら、lem-ch-model により $\mathfrak N_{M,x}\models\alpha_{M,x}$ かつ $\mathfrak N_{M,x}\not\models\eta_M$ なので、$\mathfrak N_{M,x}\not\models\theta_{M,x}$ であり、$\theta_{M,x}$ は妥当でない。$\square$
Church の定理
thm-ch-reduction の言語 $L_M$ は機械 $M$ ごとに違う。1 台の機械で停止問題の難しさがすでに現れることを使うと、言語を 1 つに固定できる。
有限個の記号からなる一階言語 $L_0$ で、$L_0$ の妥当な文の全体が決定可能でないものが存在する。さらに、$L_0$ の記号をすべて含む可算な言語 $L$ で、$L_0$ の文の番号を $L$ の文としての番号へ移す写像が計算可能であるものについて、$L$ の妥当な文の全体も決定可能でない。
停止問題 の記事の例「停止を判定できない 1 台の機械」により、番号 $e_0$ の機械 $M_0:=M_{e_0}$ で、$M_0$ が入力 $x$ で停止することと $x\in K$ が同値になるものがある。$L_0:=L_{M_0}$ とおき、$L_0$ の妥当な文の番号の集合を $\mathrm{Val}_0$ とする。
$g(x):=\ulcorner\theta_{M_0,x}\urcorner$ とおく。$\theta_{M_0,x}$ のうち $x$ によって変わるのは $I_x$ だけで、$I_x$ は決まった形の連言を $x+1$ 個並べた文なので、$g$ は記号列をつなげる操作の繰り返しで計算でき、全域的な計算可能関数である（同じ組み立てを機械の番号ごとに行う手順は OLT26 Theorem 32.16 の証明にある、p. 511）。thm-ch-reduction により、すべての $x$ について
$$
x\in K\iff M_0\text{ は入力 }x\text{ で停止する}\iff g(x)\in\mathrm{Val}_0
$$
である。$\mathrm{Val}_0$ が決定可能なら、$\chi_K=\chi_{\mathrm{Val}_0}\circ g$ は計算可能な関数の合成なので計算可能になり、$K$ が決定可能でないこと（停止問題 の定理「停止問題の決定不能性」）に反する。
後半を示す。$L_0$ の文 $\sigma$ が $L$ の文として妥当であることと、$L_0$ の文として妥当であることは同値である。実際、$L$ 構造 $\mathcal A$ では $\mathcal A\models\sigma\iff\mathcal A|_{L_0}\models\sigma$ であり（構造(モデル) の定義「簡約と拡張」の後の段落）、逆にどの $L_0$ 構造も、$L\setminus L_0$ の記号を任意に解釈して $L$ 構造に拡張できる（台集合は空でないので解釈は存在する）。番号を移す計算可能な写像を $h$、$L$ の妥当な文の番号の集合を $\mathrm{Val}_L$ とする。$L_0$ の文の番号の集合を $\mathrm{Sent}_0$（決定可能）とし、$h$ を $\mathrm{Sent}_0$ の外では値 $0$ をとる全域的な計算可能関数に延ばしておくと、$\chi_{\mathrm{Val}_0}=\chi_{\mathrm{Sent}_0}\cdot(\chi_{\mathrm{Val}_L}\circ h)$ である。$\mathrm{Val}_L$ が決定可能なら $\mathrm{Val}_0$ も決定可能になり、前半に反する。$\square$
証明の要は、「機械が停止するか」という問いを、「計算の規則を述べた文から停止を述べた文が論理的に従うか」という問いに書き換えたことである。前者が決定できないので、後者も決定できない。
妥当な文の全体は、決定可能でなくても半決定可能である。
可算な言語 $L$ の妥当な文の全体は半決定可能である。
Gödelの完全性定理 により、$\sigma$ が妥当であることは $\sigma$ が論理的公理だけから証明できることと同値である。証明は文の有限列であり、与えられた有限列が証明かどうかは機械的に検査できるので、有限列を番号の順に検査し、$\sigma$ で終わる証明が見つかったら停止する手順は、$\sigma$ が妥当なときちょうど停止する（OLT26 Theorem 32.18、p. 512。証明の検査が計算可能であることはこの記事では証明しない）。$\square$
この 2 つから、妥当でない側と充足可能な側について次が従う。
thm-ch-main の言語 $L_0$ について、次が成り立つ。
- 妥当でない $L_0$ の文の全体は半決定可能でない。
- 充足可能な $L_0$ の文の全体は、決定可能でなく、半決定可能でもない。
- 充足可能でない $L_0$ の文の全体は半決定可能であるが、決定可能でない。
$L_0$ の文の番号の集合を $\mathrm{Sent}$、妥当な文、妥当でない文、充足可能な文の番号の集合をそれぞれ $\mathrm{Val}_0$、$\mathrm{NV}$、$\mathrm{Sat}$ とする。$\mathrm{Sent}$ は決定可能である。
詳しい証明を開く
1：$\mathrm{NV}$ が半決定可能なら、$\mathbb{N}\setminus\mathrm{Val}_0=(\mathbb{N}\setminus\mathrm{Sent})\cup\mathrm{NV}$ は半決定可能な集合の和なので半決定可能である（帰納的可算集合 の命題「帰納的可算集合の閉包性」）。prop-ch-semidecidable により $\mathrm{Val}_0$ も半決定可能なので、停止問題 の定理「決定可能性と半決定可能性」により $\mathrm{Val}_0$ は決定可能になり、thm-ch-main に反する。
2：否定を作る写像 $\nu(\ulcorner\sigma\urcorner):=\ulcorner\lnot\sigma\urcorner$ は計算可能である。$\sigma$ が妥当でないことは、$\lnot\sigma$ を真にする構造があること、すなわち $\lnot\sigma$ が充足可能であることと同値なので、$\mathrm{NV}=\mathrm{Sent}\cap\nu^{-1}(\mathrm{Sat})$ である（$\nu$ は $\mathrm{Sent}$ の外では任意の計算可能な値をとるとしておく）。$\mathrm{Sat}$ が半決定可能なら、逆像と決定可能な集合との共通部分も半決定可能なので（同じ命題）、$\mathrm{NV}$ が半決定可能になり 1 に反する。決定可能な集合は半決定可能なので、$\mathrm{Sat}$ は決定可能でもない。
3：$\sigma$ が充足可能でないことは $\lnot\sigma$ が妥当であることと同値なので、充足可能でない文の番号の集合は $\mathrm{Sent}\cap\nu^{-1}(\mathrm{Val}_0)$ であり、prop-ch-semidecidable と同じ命題により半決定可能である。決定可能なら、$\mathrm{Sat}=\mathrm{Sent}\setminus(\text{その集合})$ が決定可能になり 2 に反する。$\square$
妥当性と充足不能性は「証明が見つかれば確かめられる」側で、妥当でないことと充足可能性は「反例となる構造が見つかれば確かめられる」はずの側である。しかし構造は一般に無限で、反例の構造を有限の手順で探し当てることはできない。1 はこのことを正確に述べている。
直感
停止問題 で停止しない側を判定できないのは、どれだけ待っても「まだ止まらない」と「永久に止まらない」を区別できないからであった。thm-ch-reduction はこの非対称性をそのまま論理に写す。機械が停止するなら、停止までの有限個の様相を 1 つずつたどる議論（lem-ch-halts-valid の帰納法）が $\theta_{M,x}$ の証明の骨組みになる。停止しないなら、反例は計算の全体を写した無限の構造 $\mathfrak N_{M,x}$ である。有限の証明は探せるが、無限の反例は一般に探せない。
反例：条件を外すと成り立たない
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 量化記号を含む一階の文を扱う | 命題論理の論理式（命題変数と結合子だけ） | 妥当性の決定不能性 |
| 言語が 1 項関係記号以外の記号（2 項関係記号・関数記号・定数記号）を含む | 1 項関係記号だけからなる有限な言語 | 妥当性の決定不能性 |
| 構造の大きさを制限しない | 有限構造だけで真か（有限妥当性）を問う | 妥当な文の全体の半決定可能性 |
thm-ch-main の言語 $L_0$ は、2 項関係記号 $<,Q_q,S_a$、関数記号 $\mathsf s,\mathsf p$、定数記号 $0$ を含み、すべての構造を相手にしている。各行では、そのうち 1 つだけを外している。
1 行目：命題論理の論理式 $\varphi$ の真理値は $\varphi$ に現れる有限個の命題変数の値だけで決まる（命題論理 の補題「現れる変数だけで値が決まる」）。現れる変数が $n$ 個なら付値は本質的に $2^n$ 通りしかないので、すべてを調べれば $\varphi$ が恒真式かどうかが判定できる。
2 行目：1 項関係記号だけからなる有限な言語では、文が充足可能なら記号の個数と量化記号の深さで決まる個数以下の元のモデルをもち、妥当な文の全体は決定可能である（決定可能な理論 の定理「単項述語論理の決定可能性」）。$L_0$ から 1 項関係記号以外の記号（2 項関係記号・関数記号・定数記号）を除くと、この場合に入る。
3 行目：以下、文は、番号 $e$ の機械 $M_e$（$e\in\mathbb{N}$）の言語 $L_{M_e}$ の記号をすべて含む 1 つの可算な言語 $L_\infty$ の文とし、$L_\infty$ の記号と文には「記法と前提」の約束で番号を付ける。文 $\sigma$ が有限構造で充足可能であるかどうかを判定する Turing 機械は存在しない（Trakhtenbrot の定理、OLT26 Theorem 32.21、p. 514。この記事では証明しない）。一方、有限構造で充足可能な文の全体は半決定可能である。$n=1,2,\dots$ について、台集合 $\{1,\dots,n\}$ の上で $\sigma$ に現れる記号を解釈する有限個の構造を順に作り、それぞれで $\sigma$ が真かを計算すればよい（有限構造での真偽の計算は 決定可能な理論 の定理「有限構造の理論は決定可能」の証明の手順による）。有限構造で充足可能な文の全体は、半決定可能で決定可能でないので、その補集合（文の番号のうち）は半決定可能でない（停止問題 の定理「決定可能性と半決定可能性」）。$\sigma$ がすべての有限構造で真であることは $\lnot\sigma$ が有限構造で充足可能でないことと同値である。有限構造すべてで真な文の全体が半決定可能なら、否定を作る写像による逆像として「有限構造で充足可能でない文」の全体が半決定可能になって矛盾するので（cor-ch-satisfiable の証明の 2 と同じ議論）、有限構造すべてで真な文の全体は半決定可能でない。prop-ch-semidecidable の半決定可能性は、構造を有限に制限すると成り立たなくなる。
3 行目の結果から、有限構造すべてで真な文をちょうど導く健全で完全な証明体系は存在しない。完全性定理が使えるのは、構造の大きさを制限しないときである。
補足
- 言語の大きさ． 言語を 2 項関係記号 1 つにまで小さくしても、妥当な文の全体は決定可能でない（OLT26 Corollary 36.16、p. 579。この記事では証明しない）。一方、決定可能な理論 の定理「単項述語論理の決定可能性」により、1 項関係記号だけなら決定可能である。関係記号だけからなる言語では、決定可能と決定不能の境目は 2 項の関係記号が現れるかどうかにある。関数記号を許すと事情が変わり、1 項関数記号を 1 つ加えても決定可能のままだが、1 項関数記号が 2 つあれば 2 項関係記号がなくても決定可能でない（OLT26 p. 579。この記事では証明しない）。
- 算術を経由する証明． Robinson算術 Q は有限個の公理をもち決定可能でない理論なので、Q の公理の連言を $\sigma_Q$ とすると、算術の言語の文 $\psi$ について「$\sigma_Q\to\psi$ が妥当か」は決定できない。この議論で、算術の言語の妥当な文の全体が決定可能でないことが示される（決定可能な理論 の系「算術の言語の妥当な文」）。この記事の証明は、算術を経由せずに停止問題から直接示している。
- Church–Turing のテーゼ． この記事の定理は、Turing 機械で計算できる手順についての定理である。「妥当性を判定する機械的な手順はどんな形でも存在しない」と読むには、Church–Turingのテーゼ を認める必要がある。
関連項目
- 前提: 一階述語論理, Turing機械, 停止問題
- 比較: Gödelの完全性定理, 決定可能な理論, 命題論理
- 発展: Gödelの不完全性定理, 計算可能性理論, 有限モデル理論, Hilbertの第10問題
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
