§E16.25本質的決定不能性と Church の定理

最終更新

一階述語論理の完全性定理は、意味論的帰結と形式的導出が一致することを述べる。しかし、完全性定理は、文が妥当であるか否かを判定するアルゴリズムの存在を主張しない。本記事では Robinson 算術QQの本質的決定不能性を証明し、QQの定理判定問題を一階述語論理の妥当性判定問題へ還元する。還元の向きと入力全体に対する写像を明示することにより、妥当性、証明可能性、充足可能性、充足不能性が決定不能であることを順に導く。

1 決定問題の規約

文字列の有限アルファベットと、LAL_Aの項・論理式・文に対する有効な符号化を一つ固定する。正しい文のコードであるか否かは決定可能であり、正しい文のコードから否定のコードを計算する操作も全域計算可能である。

定義 1.1. 有限文字列xxに対して、次の四言語を定める。

VALA={⌜φ⌝∣φ は妥当な LA 文},PRVA={⌜φ⌝∣φ は LA 文かつ ⊢φ},SATA={⌜φ⌝∣φ は充足可能な LA 文},UNSATA={⌜φ⌝∣φ は充足不能な LA 文}.\begin{aligned} \mathsf{VAL}_A &=\{\ulcorner\varphi\urcorner\mid \varphi\text{ は妥当な }L_A\text{ 文}\},\\ \mathsf{PRV}_A &=\{\ulcorner\varphi\urcorner\mid \varphi\text{ は }L_A\text{ 文かつ }\vdash\varphi\},\\ \mathsf{SAT}_A &=\{\ulcorner\varphi\urcorner\mid \varphi\text{ は充足可能な }L_A\text{ 文}\},\\ \mathsf{UNSAT}_A &=\{\ulcorner\varphi\urcorner\mid \varphi\text{ は充足不能な }L_A\text{ 文}\}. \end{aligned}

正しいLAL_A文を表さない文字列は、四言語のいずれにも属さないと定める。理論TTの定理集合は

Thm⁡(T)={⌜φ⌝∣φ は LA 文かつ T⊢φ}\operatorname{Thm}(T) =\{\ulcorner\varphi\urcorner\mid \varphi\text{ は }L_A\text{ 文かつ }T\vdash\varphi\}

とする。

注意 1.2 (many-one 還元の局所再掲). many-one 還元の定義は§E15.6 定義 1.1で与えられている。本記事で用いる記号を明確にするため、定義の条件を局所的に再掲する。文字列の集合A,BA,Bに対して、A≤mBA\le_m Bであるとは、全域計算可能関数ffが存在して、すべての文字列xxについて

x∈A⟺f(x)∈Bx\in A\quad\Longleftrightarrow\quad f(x)\in B

が成り立つことをいう。

この定義では、AAに属する入力だけでなく、すべての入力に対してf(x)f(x)を定める必要がある。したがって、以下の還元では非論理式コードに対する出力も指定する。

2 Robinson 算術 Q の本質的決定不能性

定義 2.1. 計算可能に列挙することができる理論SSが本質的に決定不能であるとは、SSを含む任意の無矛盾かつ計算可能に列挙することができる理論TTに対して、Thm⁡(T)\operatorname{Thm}(T)が決定不能であることをいう。

定理 2.2 (Q の本質的決定不能性).TTを、Q⊆TQ\subseteq Tを満たす無矛盾かつ計算可能に列挙することができるLAL_A理論とする。このとき、Thm⁡(T)\operatorname{Thm}(T)は決定不能である。したがって、QQは本質的に決定不能である。

証明.Thm⁡(T)\operatorname{Thm}(T)が決定可能であると仮定する。LAL_Aのすべての文を重複を許して計算可能に

σ0,σ1,σ2,…\sigma_0,\sigma_1,\sigma_2,\ldots

と列挙する。有限集合Δn\Delta_nを帰納的に構成し、Tn=T∪ΔnT_n=T\cup\Delta_nが無矛盾であるように保つ。初期値をΔ0=∅\Delta_0=\varnothingとする。

Δn\Delta_nの文の連言をδn\delta_nと書く。Δn\Delta_nが空である場合には、δn\delta_nを論理的に妥当な固定文とする。有限回の演繹定理により、Tn∪{σn}T_n\cup\{\sigma_n\}が矛盾することと

T⊢δn→(σn→⊥)T\vdash\delta_n\to(\sigma_n\to\bot)

とは同値である。右辺の式はnnから有効に構成されるため、仮定したThm⁡(T)\operatorname{Thm}(T)の決定手続きを用いて、Tn∪{σn}T_n\cup\{\sigma_n\}の無矛盾性を決定することができる。

Tn∪{σn}T_n\cup\{\sigma_n\}が無矛盾ならば

Δn+1=Δn∪{σn}\Delta_{n+1}=\Delta_n\cup\{\sigma_n\}

とする。矛盾するならば

Δn+1=Δn∪{¬σn}\Delta_{n+1}=\Delta_n\cup\{\neg\sigma_n\}

とする。後者の場合にもTn+1T_{n+1}は無矛盾である。実際、Tn∪{¬σn}T_n\cup\{\neg\sigma_n\}も矛盾すると仮定すると、演繹定理からTn⊢¬σnT_n\vdash\neg\sigma_nとTn⊢¬¬σnT_n\vdash\neg\neg\sigma_nが得られる。古典論理ではTn⊢σnT_n\vdash\sigma_nも得られるため、TnT_nの無矛盾性に反する。

構成した理論を

U=T∪⋃n∈NΔnU=T\cup\bigcup_{n\in\mathbb N}\Delta_n

とする。各段階の選択は全域の決定手続きによって有効に実行されるため、UUは計算可能に列挙することができる。UUの有限導出で使用される追加公理は、ある一つのΔn\Delta_nにすべて含まれる。各TnT_nは無矛盾であるから、UUも無矛盾である。また、各LAL_A文σ\sigmaは列挙のある段階に現れ、その段階でσ\sigmaまたは¬σ\neg\sigmaがUUに加えられる。したがって、UUは構文論的に完全である。

一方、Q⊆T⊆UQ\subseteq T\subseteq Uであり、UUは無矛盾かつ計算可能に列挙することができる。§E16.23 定理 4.2をUUに適用すると、U⊬RUU\nvdash R_UかつU⊬¬RUU\nvdash\neg R_Uを満たす Rosser 文RUR_Uが存在する。これはUUの構文論的完全性に反する。ゆえに、Thm⁡(T)\operatorname{Thm}(T)は決定不能である。▨

§E16.15 定理 2.2により標準モデルがQQのモデルであるため、QQは無矛盾である。また、QQの公理は有限個なので、QQは計算可能に列挙することができる。したがって、定理をT=QT=Qに適用すると、Thm⁡(Q)\operatorname{Thm}(Q)は決定不能である。

3 Q の定理集合から妥当性への全域還元

§E16.15 定義 2.1で定めたQQの七つの公理は文である。それらの連言を

q=Q1∧Q2∧⋯∧Q7q=Q_1\land Q_2\land\cdots\land Q_7

と書く。また、⊥\botを固定した充足不能なLAL_A文とする。

定理 3.1. 次の関係が成り立つ。

  1. Thm⁡(Q)≤mVALA\operatorname{Thm}(Q)\le_m\mathsf{VAL}_Aである。
  2. VALA=PRVA\mathsf{VAL}_A=\mathsf{PRV}_Aである。
  3. VALA≤mUNSATA\mathsf{VAL}_A\le_m\mathsf{UNSAT}_Aである。
  4. VALA\mathsf{VAL}_A、PRVA\mathsf{PRV}_A、SATA\mathsf{SAT}_A、UNSATA\mathsf{UNSAT}_Aはいずれも決定不能である。

証明. 最初に、全域計算可能関数fQf_Qを次のように定める。

fQ(x)={⌜q→φ⌝,x=⌜φ⌝ が正しい LA 文のコードである場合,⌜⊥⌝,x が正しい LA 文のコードでない場合.f_Q(x)= \begin{cases} \ulcorner q\to\varphi\urcorner, &x=\ulcorner\varphi\urcorner\text{ が正しい }L_A\text{ 文のコードである場合},\\ \ulcorner\bot\urcorner, &x\text{ が正しい }L_A\text{ 文のコードでない場合}. \end{cases}

構文検査と式の結合は計算可能なので、fQf_Qは全域計算可能である。正しい文φ\varphiについて、有限回の演繹定理と命題論理による連言の変形から

Q⊢φ⟺⊢q→φQ\vdash\varphi \quad\Longleftrightarrow\quad \vdash q\to\varphi

が成り立つ。一階述語論理の健全性と、§E16.12 定理 5.2を空理論に適用すると、さらに

⊢q→φ⟺⊨q→φ\vdash q\to\varphi \quad\Longleftrightarrow\quad \models q\to\varphi

が成り立つ。したがって、正しい文のコードxxについて

x∈Thm⁡(Q)⟺fQ(x)∈VALAx\in\operatorname{Thm}(Q) \quad\Longleftrightarrow\quad f_Q(x)\in\mathsf{VAL}_A

を得る。xxが正しい文のコードでない場合には、定義によりx∉Thm⁡(Q)x\notin\operatorname{Thm}(Q)であり、fQ(x)=⌜⊥⌝∉VALAf_Q(x)=\ulcorner\bot\urcorner\notin\mathsf{VAL}_Aである。ゆえに同値はすべての文字列xxについて成り立ち、Thm⁡(Q)≤mVALA\operatorname{Thm}(Q)\le_m\mathsf{VAL}_Aである。

次に、正しいLAL_A文φ\varphiに対して、健全性と完全性定理を空理論に適用すると

⊨φ⟺⊢φ\models\varphi\quad\Longleftrightarrow\quad\vdash\varphi

を得る。非論理式コードはいずれの言語にも含めないという規約も両辺で同じである。したがって、VALA=PRVA\mathsf{VAL}_A=\mathsf{PRV}_Aである。完全性定理は、第一にThm⁡(Q)≤mVALA\operatorname{Thm}(Q)\le_m\mathsf{VAL}_Aの証明でQ⊢φ⟺⊨q→φQ\vdash\varphi\Longleftrightarrow\models q\to\varphiを得る箇所、第二にVALA=PRVA\mathsf{VAL}_A=\mathsf{PRV}_Aを得る箇所の双方で用いている。完全性定理から決定手続きの存在を導いているのではない。

続いて、全域計算可能関数ggを次のように定める。

g(x)={⌜¬φ⌝,x=⌜φ⌝ が正しい LA 文のコードである場合,⌜∀v (v=v)⌝,x が正しい LA 文のコードでない場合.g(x)= \begin{cases} \ulcorner\neg\varphi\urcorner, &x=\ulcorner\varphi\urcorner\text{ が正しい }L_A\text{ 文のコードである場合},\\ \ulcorner\forall v\,(v=v)\urcorner, &x\text{ が正しい }L_A\text{ 文のコードでない場合}. \end{cases}

正しい文φ\varphiについて、φ\varphiがすべてのLAL_A構造で真であることと、¬φ\neg\varphiを満たすLAL_A構造が存在しないこととは同値である。したがって、

⌜φ⌝∈VALA⟺g(⌜φ⌝)∈UNSATA\ulcorner\varphi\urcorner\in\mathsf{VAL}_A \quad\Longleftrightarrow\quad g(\ulcorner\varphi\urcorner)\in\mathsf{UNSAT}_A

が成り立つ。非論理式コードxxについては、x∉VALAx\notin\mathsf{VAL}_Aであり、g(x)=⌜∀v (v=v)⌝g(x)=\ulcorner\forall v\,(v=v)\urcornerは充足可能なのでg(x)∉UNSATAg(x)\notin\mathsf{UNSAT}_Aである。ゆえに、VALA≤mUNSATA\mathsf{VAL}_A\le_m\mathsf{UNSAT}_Aである。

§E15.6 命題 1.3の対偶により、Thm⁡(Q)\operatorname{Thm}(Q)が決定不能でThm⁡(Q)≤mVALA\operatorname{Thm}(Q)\le_m\mathsf{VAL}_Aであることから、VALA\mathsf{VAL}_Aは決定不能である。集合としてVALA=PRVA\mathsf{VAL}_A=\mathsf{PRV}_Aなので、PRVA\mathsf{PRV}_Aも決定不能である。同じ移送命題の対偶とVALA≤mUNSATA\mathsf{VAL}_A\le_m\mathsf{UNSAT}_Aにより、UNSATA\mathsf{UNSAT}_Aも決定不能である。

最後に、SATA\mathsf{SAT}_Aが決定可能であると仮定する。まず、その決定手続きからUNSATA\mathsf{UNSAT}_Aの決定手続きを構成する。入力yyが正しいLAL_A文のコードでなければ拒否し、正しい文のコードであれば、SATA\mathsf{SAT}_Aの決定結果を反転する。この手続きは、非論理式コードがUNSATA\mathsf{UNSAT}_Aに属さないという規約を守り、UNSATA\mathsf{UNSAT}_Aを決定する。

次に、UNSATA\mathsf{UNSAT}_Aの任意の決定手続きからThm⁡(Q)\operatorname{Thm}(Q)の決定手続きを構成する。入力xxに対してg(fQ(x))g(f_Q(x))を計算し、その文字列がUNSATA\mathsf{UNSAT}_Aに属するか否かを決定すればよい。二つの還元の同値から

x∈Thm⁡(Q)⟺g(fQ(x))∈UNSATAx\in\operatorname{Thm}(Q) \quad\Longleftrightarrow\quad g(f_Q(x))\in\mathsf{UNSAT}_A

が成り立つ。したがって、仮定したSATA\mathsf{SAT}_Aの決定手続きからThm⁡(Q)\operatorname{Thm}(Q)の決定手続きが得られ、QQの本質的決定不能性に反する。この二段階は、§E15.6 命題 1.3が述べる決定可能性の移送を、合成した全域還元g∘fQg\circ f_Qについて具体化したものである。ゆえに、SATA\mathsf{SAT}_Aも決定不能である。▨

注意 3.2 (完全性定理を用いる範囲). 完全性定理が与えるのは、各文φ\varphiについて⊨φ\models\varphiと⊢φ\vdash\varphiが同値であるという主張である。妥当な文の証明を計算可能に列挙することができても、列挙の途中で証明が現れない文が非妥当であると有限時間内に結論する方法は得られない。したがって、意味論と構文論の一致と、決定可能性とは異なる性質である。

4 演習

問題 4.1.

  1. fQf_Qを正しい文のコードだけに定める方法では、many-one 還元の証明として不十分である理由を述べよ。
  2. Q⊢φQ\vdash\varphiと⊨q→φ\models q\to\varphiの同値において、完全性定理を用いる向きを特定せよ。
  3. SATA\mathsf{SAT}_Aの決定手続きからThm⁡(Q)\operatorname{Thm}(Q)の決定手続きを得る二段階を述べよ。
解答 (確認問題の解答).
  1. many-one 還元の写像は、対象集合に属する入力だけでなく、すべての有限文字列に対して値をもつ全域計算可能関数でなければならない。非論理式コードにも出力を定め、所属の同値を保つ必要がある。
  2. 演繹定理からQ⊢φQ\vdash\varphiと⊢q→φ\vdash q\to\varphiの同値を得た後、⊨q→φ\models q\to\varphiから⊢q→φ\vdash q\to\varphiを得る向きで完全性を用いる。逆向きは健全性による。
  3. 第一段階では、構文検査の後、正しい文に限ってSATA\mathsf{SAT}_Aの決定結果を反転し、UNSATA\mathsf{UNSAT}_Aの決定手続きを得る。第二段階では、入力xxをg(fQ(x))g(f_Q(x))に写し、得られたUNSATA\mathsf{UNSAT}_Aの決定手続きを適用してx∈Thm⁡(Q)x\in\operatorname{Thm}(Q)を決定する。

▨

参考文献

  1. Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001.一階述語論理の完全性、および算術理論の不完全性と決定不能性の扱いを参考にした。
  2. George S. Boolos, John P. Burgess, and Richard C. Jeffrey, Computability and Logic, 5th ed., Cambridge University Press, 2007.計算可能性、many-one 還元、Church の定理、および本質的決定不能性の関係を参考にした。

前提記事