§E19.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 還元の定義は§E18.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.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は無矛盾かつ計算可能に列挙することができる。§E19.23 定理 4.2をUUに適用すると、U⊬RUU\nvdash R_UかつU⊬¬RUU\nvdash\neg R_Uを満たす Rosser 文RUR_Uが存在する。これはUUの構文論的完全性に反する。ゆえに、Thm⁡(T)\operatorname{Thm}(T)は決定不能である。▨

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

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

§E19.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

が成り立つ。一階述語論理の健全性と、§E19.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である。

§E18.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の本質的決定不能性に反する。この二段階は、§E18.6 命題 1.3で述べられる決定可能性の移送を、合成した全域還元g∘fQg\circ f_Qについて具体化したものである。ゆえに、SATA\mathsf{SAT}_Aも決定不能である。▨

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

4 演習

問題 4.1.

  1. Ref⁡(Q)={⌜φ⌝∣φ は LA 文かつ Q⊢¬φ}\operatorname{Ref}(Q)=\{\ulcorner\varphi\urcorner\mid\varphi\text{ は }L_A\text{ 文かつ }Q\vdash\neg\varphi\}とする。すべての文字列で定義された全域計算可能関数を具体的に与えてThm⁡(Q)≤mRef⁡(Q)\operatorname{Thm}(Q)\le_m\operatorname{Ref}(Q)を示し、Ref⁡(Q)\operatorname{Ref}(Q)が決定不能であることを結論せよ。
  2. 全域計算可能関数hhで、妥当な任意のLAL_A文φ\varphiが、符号がh(⌜φ⌝)h(\ulcorner\varphi\urcorner)以下である空理論からの導出をもつようなものは存在しないことを示せ。
  3. UNSATA\mathsf{UNSAT}_Aの要素を列挙する手続きが存在することを示し、SATA\mathsf{SAT}_Aの要素を列挙する手続きは存在しないことを示せ。ここで集合を列挙する手続きとは、その集合の要素だけを、すべての要素が有限時間内に現れるように重複を許して出力し続ける手続きをいう。
解答 (確認問題の解答).

  1. 全域計算可能関数rrを、x=⌜φ⌝x=\ulcorner\varphi\urcornerが正しいLAL_A文のコードならばr(x)=⌜¬φ⌝r(x)=\ulcorner\neg\varphi\urcorner、そうでなければr(x)=⌜0=0⌝r(x)=\ulcorner0=0\urcornerと定める。構文検査と否定のコードの計算は全域計算可能であるから、rrは全域計算可能である。正しい文φ\varphiについて、古典命題論理の二重否定の導入と除去によりQ⊢φQ\vdash\varphiとQ⊢¬¬φQ\vdash\neg\neg\varphiは同値であるから、⌜φ⌝∈Thm⁡(Q)\ulcorner\varphi\urcorner\in\operatorname{Thm}(Q)とr(⌜φ⌝)∈Ref⁡(Q)r(\ulcorner\varphi\urcorner)\in\operatorname{Ref}(Q)は同値である。xxが正しい文のコードでない場合、x∉Thm⁡(Q)x\notin\operatorname{Thm}(Q)である。一方、Q⊢0=0Q\vdash0=0でありQQは無矛盾であるからQ⊬¬(0=0)Q\nvdash\neg(0=0)、すなわちr(x)∉Ref⁡(Q)r(x)\notin\operatorname{Ref}(Q)である。よってすべての文字列xxについて同値が成り立ち、Thm⁡(Q)≤mRef⁡(Q)\operatorname{Thm}(Q)\le_m\operatorname{Ref}(Q)である。非論理式コードの出力にRef⁡(Q)\operatorname{Ref}(Q)に属さない文のコードを選んだことで、この場合の同値が成り立つ。定理 2.2によりThm⁡(Q)\operatorname{Thm}(Q)は決定不能であるから、§E18.6 命題 1.3の対偶によりRef⁡(Q)\operatorname{Ref}(Q)は決定不能である。

  2. そのようなhhが存在すると仮定し、VALA\mathsf{VAL}_Aを決定する手続きを構成する。入力xxが正しいLAL_A文のコードでなければ拒否する。正しい文φ\varphiのコードならばh(x)h(x)を計算し、p≤h(x)p\leq h(x)を満たす各ppについて、ppが空理論からのφ\varphiの導出の符号であるかを判定し、一つでも導出の符号であれば受理し、そうでなければ拒否する。導出の符号であるかの判定は§E19.18 定理 5.2のDeriv⁡A\operatorname{Deriv}_Aを空の公理述語について用いれば原始再帰的であり、調べるppは有限個であるから、手続きは必ず停止する。φ\varphiが妥当ならば仮定により受理する。受理したならば⊢φ\vdash\varphiであり、健全性によりφ\varphiは妥当である。よって手続きはVALA\mathsf{VAL}_Aを決定し、定理 3.1 (4)に反する。

    したがって、§E19.12 定理 5.2により妥当な文はすべて導出をもつが、その導出の符号の大きさを文の符号の全域計算可能関数で上から抑えることはできない。

  3. 完全性定理と健全性により、正しい文φ\varphiが充足不能であることは¬φ\neg\varphiが妥当であること、すなわち⊢¬φ\vdash\neg\varphiと同値である。そこで、n=0,1,2,…n=0,1,2,\ldotsの順に、nnをpair⁡(e,p)\operatorname{pair}(e,p)と分解し、eeが正しい文φ\varphiのコードでありppが空理論からの¬φ\neg\varphiの導出の符号であるときにeeを出力する手続きを考える。各段の判定は有限回の操作で終わる。出力されるeeは⊢¬φ\vdash\neg\varphiを満たすのでUNSATA\mathsf{UNSAT}_Aに属し、UNSATA\mathsf{UNSAT}_Aの要素⌜φ⌝\ulcorner\varphi\urcornerには¬φ\neg\varphiの導出の符号ppがあるので、n=pair⁡(⌜φ⌝,p)n=\operatorname{pair}(\ulcorner\varphi\urcorner,p)の段で出力される。よってUNSATA\mathsf{UNSAT}_Aを列挙する手続きが存在する。

    SATA\mathsf{SAT}_Aを列挙する手続きが存在すると仮定する。入力xxが正しい文のコードでなければ拒否し、正しい文のコードならば、SATA\mathsf{SAT}_AとUNSATA\mathsf{UNSAT}_Aの列挙を交互に一段ずつ進め、xxが前者に現れたら拒否し、後者に現れたら受理する。正しい文はちょうど一方の集合に属するので、どちらかの列挙に有限時間内に現れ、手続きは停止してUNSATA\mathsf{UNSAT}_Aを正しく決定する。これは定理 3.1 (4)に反する。よってSATA\mathsf{SAT}_Aを列挙する手続きは存在しない。

▨

参考文献

  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 の定理、および本質的決定不能性の関係を参考にした。

前提記事