Trakhtenbrotの定理

計算を $C_0,\dots,C_N$、$C_n=(q_n,\tau_n,h_n)$ とし、$C_N$ を停止様相とする。ヘッドは 1 ステップで高々 1 マス動くので $\lvert h_n\rvert\le n$ である。台集合を $U:=\{-N,\dots,N+x\}\subset\mathbb{Z}$ とし、$<$ を通常の大小、$\mathsf o:=0$、
$$ Q_q^{\mathfrak F}:=\{(h_n,n)\mid 0\le n\le N,\ q_n=q\},\qquad S_c^{\mathfrak F}:=\{(i,n)\in U\times\{0,\dots,N\}\mid\tau_n(i)=c\} $$
とおいて $L_M$ 構造 $\mathfrak F$ を定める。$\lvert h_n\rvert\le N$ なので $Q_q^{\mathfrak F}\subset U\times U$ である。$U$ は整数の区間なので $\mathrm{Ord}$ が成り立ち、$\mathrm{Suc}(u,v)$ は $v=u+1$ と同値である。
$I_x$：$v_i:=i$（$0\le i\le x$）とすればよい。$x\le N+x$ なので $v_i\in U$ であり、$C_0=(q_0,\tau_x,0)$ から $Q_{q_0}(0,0)$、$i< x$ での $S_1(i,0)$、$w< 0$ または $w\ge x$ での $S_\sqcup(w,0)$ が成り立つ。
$T_{q,a}$：$\delta(q,a)=(q',b,D)$ とし、$(u,t)\in Q_q^{\mathfrak F}\cap S_a^{\mathfrak F}$ とする。$Q_q^{\mathfrak F}$ の定義から、ある $n\le N$ について $(u,t)=(h_n,n)$、$q_n=q$ であり、$S_a^{\mathfrak F}$ の定義から $\tau_n(h_n)=a$ である。$\delta(q_n,\tau_n(h_n))$ が定義されるので $C_n$ は停止様相でなく、$n< N$ で、$C_{n+1}=(q',\tau_{n+1},h_n+d)$ である。$t':=n+1\in U$ が求める元であることを確かめる。

$<,\mathsf o,Q_q,S_a$ の $\mathcal A$ での解釈も同じ記号で書く。$\mathrm{Ord}$ により $<$ は台集合 $A$ 上の狭義の全順序である。
段 1（直後の元の一意性）． $\mathrm{Suc}(a,b)$ と $\mathrm{Suc}(a,b')$ が成り立てば $b=b'$ である。実際 $b\ne b'$ なら全順序性から $b< b'$ としてよく、$a< b< b'$ が $\mathrm{Suc}(a,b')$ に反する。同様に $\mathrm{Suc}(a,b)$ と $\mathrm{Suc}(a',b)$ から $a=a'$ が従う。
段 2（マスを表す元）． $e_0:=\mathsf o$ とし、$i\ge0$ について $e_i$ が定まり、$\mathrm{Suc}(e_i,b)$ となる $b$ があればそれを $e_{i+1}$ とする。$i\le0$ について $e_i$ が定まり、$\mathrm{Suc}(b,e_i)$ となる $b$ があればそれを $e_{i-1}$ とする（段 1 により一意）。$e_i$ が定まる $i$ の全体 $J$ は $0$ を含む $\mathbb{Z}$ の区間で、$i,i+1\in J$ なら $\mathrm{Suc}(e_i,e_{i+1})$ である。推移律から、$i< j$ がともに $J$ に属すれば $e_i< e_j$ であり、とくに $e_i\ne e_j$ である。段 1 と合わせると、$i\in J$ について、$\mathrm{Suc}(e_i,u')$ となる $u'$ があれば $i+1\in J$ かつ $u'=e_{i+1}$、$\mathrm{Suc}(u',e_i)$ となる $u'$ があれば $i-1\in J$ かつ $u'=e_{i-1}$ である。
段 3（帰納法）． 計算を $C_0,C_1,\dots$、$C_n=(q_n,\tau_n,h_n)$ とする。$M$ は停止しないので、すべての $n$ について $C_n$ がある。$A$ の元の列 $t_0,t_1,\dots$ で、$t_0=\mathsf o$、$\mathrm{Suc}(t_n,t_{n+1})$ であり、各 $n$ について次の $(\mathrm P_n)$ を満たすものを、帰納的に作る。
$$ (\mathrm P_n)\qquad h_n\in J,\quad \mathcal A\models Q_{q_n}(e_{h_n},t_n),\quad\text{すべての }i\in J\text{ について }\mathcal A\models S_{\tau_n(i)}(e_i,t_n). $$

停止するなら有限充足可能であることは lem-tr-halts-finite である。停止しないなら、lem-tr-model-infinite により $\sigma_{M,x}$ のモデルはどれも無限なので、$\sigma_{M,x}$ は有限充足可能でない。$\square$

停止問題 の記事の例「停止を判定できない 1 台の機械」により、番号 $e_0$ の機械 $M_0:=M_{e_0}$ で、$M_0$ が入力 $x$ で停止することと $x\in K$ が同値になるものがある（$K$ は自己停止集合）。$L_0:=L_{M_0}$ とおく。$L_0$ は定数記号 $\mathsf o$ と 2 項関係記号 $<,Q_q,S_a$（$q\in Q$、$a\in\Gamma$）からなり、有限である。$L_0$ の有限充足可能な文の番号の集合を $\mathrm{FS}_0$ とする。
$g(x):=\ulcorner\sigma_{M_0,x}\urcorner$ とおく。$\sigma_{M_0,x}$ のうち $x$ によって変わるのは $I_x$ だけで、$I_x$ は決まった形の部分を $x$ に応じた個数だけ並べた文なので、$g$ は記号列をつなぐ操作の繰り返しで計算でき、全域的な計算可能関数である。thm-tr-reduction により、すべての $x$ について
$$ x\in K\iff M_0\text{ は入力 }x\text{ で停止する}\iff g(x)\in\mathrm{FS}_0 $$
である。$\mathrm{FS}_0$ が決定可能なら、$\chi_K=\chi_{\mathrm{FS}_0}\circ g$ は計算可能な関数の合成なので計算可能になり、$K$ が決定可能でないこと（停止問題 の定理「停止問題の決定不能性」）に反する。
後半を示す。$L_0$ の文 $\sigma$ が $L$ の文として有限充足可能であることと、$L_0$ の文として有限充足可能であることは同値である。有限な $L$ 構造 $\mathcal A$ では $\mathcal A\models\sigma\iff\mathcal A|_{L_0}\models\sigma$ であり（構造(モデル) の定義「簡約と拡張」の後の段落）、$\mathcal A|_{L_0}$ も有限である。逆にどの有限な $L_0$ 構造も、$L\setminus L_0$ の記号を同じ台集合の上で任意に解釈して（関数記号は定値写像にするなど）有限な $L$ 構造に拡張できる。番号を移す計算可能な写像を $h$、$L$ の有限充足可能な文の番号の集合を $\mathrm{FS}_L$、$L_0$ の文の番号の集合を $\mathrm{Sent}_0$（決定可能）とし、$h$ を $\mathrm{Sent}_0$ の外では値 $0$ をとる全域的な計算可能関数に延ばしておくと、$\chi_{\mathrm{FS}_0}=\chi_{\mathrm{Sent}_0}\cdot(\chi_{\mathrm{FS}_L}\circ h)$ である。$\mathrm{FS}_L$ が決定可能なら $\mathrm{FS}_0$ も決定可能になり、前半に反する。$\square$

同型な構造は同じ文を満たし（一階述語論理 の定理「同型補題」）、$n$ 元の構造は台集合を $\{1,\dots,n\}$ に取り替えた同型な構造をもつ。よって文 $\sigma$ が有限充足可能であることは、ある $n\ge1$ について台集合 $\{1,\dots,n\}$ の上に $\sigma$ のモデルがあることと同値である。
$L$ は有限なので、台集合 $\{1,\dots,n\}$ の上の $L$ 構造は有限個しかなく、各記号の解釈を有限の表として順に書き出せる。各構造で $\sigma$ が真かどうかは、量化記号を $n$ 個の元についての有限の連言・選言として読めば計算できる（決定可能な理論 の定理「有限構造の理論は決定可能」の証明の手順）。よって「$\sigma$ は文の番号で、台集合 $\{1,\dots,n\}$ の上に $\sigma$ のモデルがある」という $(\ulcorner\sigma\urcorner,n)$ の関係は決定可能であり、有限充足可能な文の番号の集合はその射影である。帰納的可算集合 の定理「帰納的可算集合の言い換え」の 4 により、これは半決定可能である。$\square$

$L_0$ の文の番号の集合を $\mathrm{Sent}_0$、有限妥当な文と有限充足可能でない文の番号の集合を $\mathrm{FV}_0$、$\mathrm{NF}_0$ とする。$\mathrm{Sent}_0$ は決定可能で、否定を作る写像 $\nu(\ulcorner\sigma\urcorner):=\ulcorner\lnot\sigma\urcorner$ は計算可能である（$\mathrm{Sent}_0$ の外では値 $0$ をとるとしておく）。
2：$\mathrm{NF}_0$ が半決定可能なら、$\mathbb{N}\setminus\mathrm{FS}_0=(\mathbb{N}\setminus\mathrm{Sent}_0)\cup\mathrm{NF}_0$ は半決定可能な集合の和なので半決定可能である（帰納的可算集合 の命題「帰納的可算集合の閉包性」）。prop-tr-semidecidable により $\mathrm{FS}_0$ も半決定可能なので、停止問題 の定理「決定可能性と半決定可能性」により $\mathrm{FS}_0$ は決定可能になり、thm-tr-main に反する。
1：$\sigma$ が有限充足可能でないことは $\lnot\sigma$ が有限妥当であることと同値なので、$\mathrm{NF}_0=\mathrm{Sent}_0\cap\nu^{-1}(\mathrm{FV}_0)$ である。$\mathrm{FV}_0$ が半決定可能なら、逆像と決定可能な集合との共通部分も半決定可能なので（同じ命題）、2 に反する。
3：そのような証明体系があれば、$\mathrm{FV}_0$ は証明できる文の番号の集合に一致して半決定可能になり、1 に反する。$\square$