1 定義
決定不能性とは、ある問題に対して、すべての入力に対し正否を必ず正しく返す一般手続きが存在しない性質をいう。対象は数学的命題、プログラム、形式言語、論理式など多岐にわたり、有限の規則だけでは一律に判定できない場合に用いられる。
この概念は、単に「難しい」こととは異なる。計算資源を増やしても解ける見込みがある問題は、通常は困難ではあっても決定不能とは呼ばれない。むしろ、どれほど巧妙なアルゴリズムを考えても、原理的に完全な判定法が存在しない点に核心がある。
1.1 決定問題との関係
決定不能性は、決定問題の枠組みの中で定式化される。決定問題は、入力に対して「はい」か「いいえ」を返す形式の問いであり、理論計算機科学ではこの形に整理して解析することが多い。
ある決定問題が決定不能であるとは、その問題全体を解く単一のアルゴリズムが存在しないことを意味する。個々の入力については解答できる場合でも、一般の場合を網羅する方法がないなら、決定不能とみなされる。
1.2 判定可能性との違い
判定可能性は、ある問題に対して有限時間で必ず正しい答えを返す手続きがあるかどうかを示す。決定不能性は、その逆の性質として理解できる。
ただし、判定不能であっても、半決定可能である場合がある。これは、正例についてはいつか答えが得られるが、負例では停止しないことがありうる性質で、完全な判定とは区別される。
1.3 決定不能と未解決の違い
未解決問題は、現在の知識では結論が出ていない問いを指す。一方、決定不能な問題は、理論的にその性質が証明されており、どの方法を採っても一般解法は存在しない。
この違いは重要である。未解決性は将来の進展で覆る可能性があるが、決定不能性はその体系の内部で限界として確立される。
2 歴史
決定不能性の考え方は、20世紀前半の数理論理学と計算理論の進展の中で明確になった。形式的な推論を厳密に記述し、その限界を調べる過程で、一般的な解法を持たない問題があることが次第に示された。
当初の関心は、数学全体を完全で矛盾のない体系として基礎づけられるかという問いに向けられていた。その探究の中で、証明の機械化可能性や、演算手続きの限界が中心的なテーマとなった。
2.1 形式論理学における背景
19世紀末から20世紀初頭にかけて、数学を公理化し、推論を厳密化する試みが進んだ。これにより、証明は記述可能な対象となり、どの命題が導出できるかを形式的に問えるようになった。
この時期には、数学の基礎をめぐる研究が活発化し、論理的整合性や完備性が主要な課題となった。そうした流れが、後の決定不能性の発見につながる土台を作った。
2.2 計算可能性理論の成立
計算とは何かを定義する必要が生じ、関数や問題を機械的手続きで扱えるかどうかが研究された。これが計算可能性理論の出発点である。
この理論は、形式的な定義を通じて、どの問題が原理的に計算できるかを分類する枠組みを提供した。決定不能性は、この分類の中で最も重要な否定的結果の一つとして現れた。
2.2.1 チューリング機械の導入
チューリングは、計算を単純な記号操作の連鎖としてモデル化した。チューリング機械は、現在の計算可能性の標準的な抽象モデルの一つである。
このモデルの利点は、直観的でありながら厳密に定式化できる点にある。停止性や出力の存在を議論するうえで、機械の振る舞いを形式的に追跡できるようになった。
2.2.2 証明論との関連
証明論では、証明そのものを記号列として扱う。そこでは、ある命題が証明可能かどうかを、形式体系の規則に従って調べる。
計算可能性理論との接点は、証明の探索が計算手続きとして表現できる点にある。これにより、証明可能性の問題が、計算の限界と直結することが明らかになった。
2.3 主要な発見
決定不能性を示す代表的成果として、停止性問題の不可解性、論理式の満たしうるかどうかの判定不能性、そして形式体系の証明可能性の限界が挙げられる。
これらの発見は、数学的体系が万能ではないことを示しただけでなく、アルゴリズム的手法に本質的な境界があることを明確にした。
3 理論的基礎
決定不能性を理解するには、形式体系、計算可能性、自己言及という三つの柱が重要である。これらは互いに関連しながら、一般的な判定法が存在しない理由を説明する。
理論的基礎の検討では、対象をどのように記述するかが鍵になる。公理や推論規則、アルゴリズムの定義、そして記号列が自分自身を参照する構造が、核心的な役割を果たす。
3.1 形式体系
形式体系は、記号、規則、公理から成る演繹の枠組みである。そこでの命題は、明示的な規則に従って構成され、意味論よりも構文論が重視される。
この枠組みでは、何が正しいかではなく、何が導出されるかが問われる。決定不能性は、この導出可能性を一括して判定できない場合に現れる。
3.1.1 公理
公理は、体系の出発点となる基本命題である。証明は、これらを土台に推論を積み重ねて組み立てられる。
公理が有限個でも無限個でも、体系の性質は大きく変わる。特定の公理集合に対して、導出可能性が一般には判定できないことがある。
3.1.2 推論規則
推論規則は、既知の命題から新しい命題を得るための形式的な操作である。規則が明確であれば、証明の各段階は機械的に確認できる。
しかし、規則が機械的に適用できることと、任意の命題について導出可能性を決められることは同じではない。後者のほうがはるかに強い条件である。
3.2 計算可能性
計算可能性は、ある入力から出力を得る手続きがアルゴリズムとして実現できるかを扱う。決定不能性は、この枠組みの否定的境界を示す。
計算可能であることは、実際に計算できるだけでなく、理論上のモデルに還元できることを意味する。その一方で、還元不能な問題は一般の手順では扱えない。
3.2.1 アルゴリズム
アルゴリズムは、有限の手順で構成される問題解決法である。入力の種類が限られていれば容易に記述できるが、一般形では限界が現れる。
決定不能性の議論では、どのようなアルゴリズムを許してもよいかを厳密に定める必要がある。そのため、計算モデルの選択が重要になる。
3.2.2 帰納的可算性
帰納的可算集合は、肯定例を列挙できる集合である。証明を順に出力するような手続きは、この性質に対応する。
この概念は、決定可能性より弱いが、問題の構造を理解するうえで有用である。決定不能でも、帰納的可算な対象は多く、証明探索や列挙に関係する。
3.3 自己言及
自己言及は、ある記述が自分自身に関する情報を含む構造を指す。決定不能性の多くは、この種の構成と深く結びついている。
自己言及が生じると、体系は自分の限界について語ることになり、そこに論理的な緊張が生まれる。この緊張が、対角線論法や再帰定理の背景にある。
3.3.1 対角線論法
対角線論法は、全体を列挙したと仮定しても、その列挙に含まれない対象を構成する方法である。古典的には無限集合の大きさの比較で用いられたが、計算理論にも応用される。
決定不能性の証明では、あらゆる判定器候補に対して、それを破る入力を組み立てる形で利用される。これにより、完全な判定法の存在を否定できる。
3.3.2 再帰定理
再帰定理は、プログラムが自分自身の記述を参照する状況を保証する結果である。これによって、自己コピーや自己検査を含む構成が可能になる。
この定理は、自己参照を厳密に扱うための基本的道具である。証明不能性や判定不能性の構成では、しばしばその技法が用いられる。
4 代表的な決定不能問題
決定不能性を示す典型例は、計算理論と論理学の双方に見られる。これらの問題は、形式的に明確でありながら、一般解法が存在しないことが証明されている。
代表例を通じて、決定不能性が抽象的な概念ではなく、具体的な対象に現れることが分かる。
4.1 停止性問題
停止性問題は、与えられたプログラムと入力に対して、計算が有限時間で終了するかを判定する問題である。計算機科学における最も有名な決定不能問題の一つである。
この問題が解けないことは、任意のプログラムの将来の挙動を一般に完全予測できないことを意味する。実用上も理論上も、きわめて大きな含意を持つ。
4.1.1 問題の定式化
標準的には、プログラムと入力の組を受け取り、その実行が停止するかどうかを答える決定問題として表す。モデルとしてはチューリング機械がよく用いられる。
この定式化は、個々の事例では判定できても、全体を覆う単一手続きの有無を問う点に特徴がある。
4.1.2 証明の概略
証明は、停止性を判定する機械があると仮定し、その仮定から矛盾を導く形で行われる。典型的には、判定器を入力に取る反転的なプログラムを構成する。
そのプログラムに自分自身を与えると、停止する場合としない場合の両方で矛盾が生じる。したがって、一般の判定器は存在しない。
4.2 チューリング機械の等価性判定
二つのチューリング機械が同じ言語を受理するか、あるいは同じ関数を計算するかを判定する問題は、一般には決定不能である。機械の振る舞いを完全に比較する手続きは存在しない。
この種の問題は、見かけ上は構造比較であっても、内部で無限の挙動が絡むため判定が難しくなる。停止性問題からの帰着で示されることが多い。
4.3 論理式の充足可能性
論理式に変数への真偽値割り当てを与えて真にできるかを問う充足可能性問題は、論理学と計算機科学の接点にある。命題論理では判定可能だが、より豊かな体系では判定不能になることがある。
特に、述語論理の一般的な充足可能性や妥当性の問題は、広い意味での決定不能性を示す代表例である。論理の表現力が高まるほど、一般判定は困難になる。
4.4 ペアノ算術の証明可能性
ペアノ算術のような算術体系では、ある命題が証明できるかどうかを一般に判定する手続きは存在しない。証明を列挙することはできても、任意の文について結論を出す万能法はない。
この事実は、算術の内部に十分な表現力があることと関連する。数の性質を記述できる体系ほど、自身の限界を免れにくい。
4.5 形式言語に関する判定不能問題
文法やオートマトンに関する多くの性質は決定可能だが、より一般の形式言語では判定不能な問題が現れる。たとえば、ある言語が特定の性質を持つかどうかを一括して判断することは難しい。
言語理論では、対象クラスの広がりに応じて、判定可能性と決定不能性の境界が明瞭になる。これは、抽象言語の研究が計算理論と密接につながる理由でもある。
5 証明方法
決定不能性の証明には、いくつかの標準的技法がある。どの方法も、ある問題を別の既知の問題へ結びつけ、一般解法の不存在を示す方向に働く。
これらの技法は互いに独立ではなく、しばしば組み合わせて用いられる。実際の証明では、帰着、対角化、自己参照が重なり合うことが多い。
5.1 帰着による証明
帰着は、ある問題を別の問題に変換することで、後者が解ければ前者も解けるという関係を作る方法である。既知の決定不能問題からの変換により、新しい対象の困難さを示せる。
この手法の利点は、個別の問題を一から解析しなくてもよい点にある。構造を保つ変換があれば、性質の移送が可能になる。
5.1.1 停止性問題からの帰着
停止性問題は、決定不能性の出発点としてしばしば使われる。ある問題が停止性を判定できれば、その問題も判定不能であると結論づけられる。
この方法では、入力をプログラム化し、停止の有無が元の問いの真偽を反映するように設計する。変換が有効なら、元の問題の不可解性がそのまま受け継がれる。
5.1.2 既知の決定不能問題からの帰着
停止性問題以外にも、充足可能性や証明可能性など、既に決定不能と分かっている問題が基準として用いられる。新しい問題をこれらへ落とし込めれば、不可判定性が示される。
この技法は、決定不能性の分類を体系的に広げるうえで重要である。多くの定理は、この連鎖的な比較によって確立されてきた。
5.2 対角線論法
対角線論法では、あらゆる候補手続きの一覧を想定し、それぞれの弱点を突く対象を作る。これにより、列挙が完全ではありえないことを示す。
計算理論では、機械が出す答えの並びを横断的に操作し、どの機械とも一致しない入力を設計する。これが一般判定法の不存在を導く。
5.3 自己参照構成
自己参照構成は、対象が自分自身に関する情報を含むように設計する技法である。証明やプログラムが自分の記述を取り込むことで、特殊な挙動を引き起こせる。
この方法は、停止性問題の対角的証明や、不完全性定理の構成と親和的である。再帰定理と合わせて用いられることが多い。
5.4 還元の技法
還元は、問題間の比較を通じて性質を伝播させる広い概念である。計算複雑性だけでなく、決定不能性の証明でも中心的役割を果たす。
適切な還元が見つかれば、難しさの源泉を別のよく理解された問題に移すことができる。これにより、未知の対象の限界が明らかになる。
6 関連する定理
決定不能性は、いくつかの基本定理によって支えられている。これらは計算、証明、真理の各概念に関する深い制約を示す。
各定理は異なる視点を与えるが、共通して形式体系の万能性を否定する点で一致している。
6.1 チャーチ・チューリングのテーゼ
チャーチ・チューリングのテーゼは、直観的に計算可能なものはチューリング機械で計算可能だとする主張である。これは定理というより、計算概念の同一視に関する基本的な立場である。
この考え方が受け入れられることで、チューリング機械上での決定不能性が、一般の機械的計算の限界として理解される。
6.2 ゲーデルの不完全性定理
不完全性定理は、十分に強い無矛盾な形式体系には、証明も反証もできない命題が存在することを示す。これにより、算術を含む体系の限界が明確になった。
決定不能性との関係は深い。証明可能性の一般判定ができないことや、自己言及文の構成が、この定理と密接に結びついている。
6.3 ライスの定理
ライスの定理は、チューリング機械が計算する部分関数の非自明な意味論的性質はすべて決定不能であると述べる。これは、プログラムの挙動に関する多くの性質が一括判定できないことを示す。
この定理は、個々のソースコードではなく、その意味に依存する性質が広く解けないことを明らかにする。プログラム解析の基本的限界を与える結果である。
6.4 タルスキの真理不能性定理
タルスキの定理は、十分に豊かな形式言語の内部で、その言語自身の真理概念を完全に定義することはできないとする。真理の全体を同一体系内に取り込むことに制限がある。
この結果は、自己言及と対角化の強力さを示す。形式化された真理の扱いには、必ず外部の観点が必要になる。
7 決定不能性の種類
決定不能性にはいくつかの区別がある。問題がどの意味で「解けない」のかを精密に述べることで、誤解を避けられる。
分類は、絶対的な不可能性、オラクルに相対的な不可能性、証明体系内での限界、そして計算量上の困難さとの対比を含む。
7.1 絶対的決定不能性
絶対的決定不能性は、標準的な計算モデルの範囲で一般判定法が存在しない性質をいう。通常、停止性問題のような古典的結果がこれに当たる。
この意味での不可能性は、特定のプログラミング言語や実装に依存しない。問題の本質に由来する限界である。
7.2 相対的決定不能性
相対的決定不能性は、あるオラクルや補助手続きが与えられたとしてもなお解けないことを指す。基準を強化しても残る不可解性である。
この概念は、計算階層や相対化の議論で重要になる。どの程度の追加情報があっても越えられない壁を示す。
7.3 証明論的決定不能性
証明論的決定不能性は、ある命題が特定の公理系から導出できるかどうかを、その体系の内部では一般に判定できないことをいう。証明探索の限界として理解される。
これは、真偽の問題というより、導出可能性の問題である。形式的証明と計算手続きの接点に位置づけられる。
7.4 計算量的困難性との比較
計算量的困難性は、理論上は解けるが実行資源が大きすぎる問題を扱う。これに対し、決定不能性は資源を増やしても一般解法が存在しない点で異なる。
両者はしばしば混同されるが、区別は明確である。前者は実用上の制約、後者は原理的制約を表す。
8 応用と影響
決定不能性の理論は、純粋数学にとどまらず、計算機科学の多くの分野に影響を与えた。限界を知ることは、何が可能かを設計するうえでも重要である。
現代の解析手法や検証技術は、決定不能性を前提に、完全性ではなく近似や部分的保証を目指すことが多い。
8.1 数学基礎論への影響
数学基礎論では、形式体系の能力と限界が中心課題となる。決定不能性は、数学の全命題を一つの手順で完全に扱う構想に制約を与えた。
その結果、より限定された公理系や、相互に補完し合う複数の枠組みを用いる発想が重視されるようになった。
8.2 計算機科学への影響
計算機科学では、アルゴリズム設計、プログラミング言語理論、複雑なシステムの分析において、決定不能性が基本的な背景となる。理論の上限を知ることで、適切な仕様設定が可能になる。
この知識は、実装可能性の見積もりや、自動化の期待値を調整するうえでも役立つ。
8.3 形式検証への影響
形式検証は、ソフトウェアやハードウェアの性質を数学的に証明する技術である。決定不能性のため、すべての性質を完全に自動検証することはできない。
そのため、検証器は特定クラスに限定したり、人間の補助を前提にしたりする。実際のツールは、この限界に合わせて設計される。
8.4 プログラム解析への影響
プログラム解析では、停止、到達可能性、変数の値の範囲などを調べる。多くの解析問題は、一般には決定不能か、少なくとも厳しい制約を受ける。
この事実により、実用的な解析は近似、保守的推定、あるいは特定言語への制限を取り入れることが多い。
9 哲学的含意
決定不能性は、数学と機械の限界に関する哲学的議論にも影響を与えた。形式化できるものの範囲や、理解と計算の関係が問われるようになった。
このテーマは、認識論や数学の存在論とも関わるが、まずは理論的な制約として理解されることが多い。
9.1 数学における限界
決定不能性は、数学がすべてを一様に決着できるわけではないことを示す。証明可能性と真理は一致しない場合がある。
このことは、数学的真理の広がりと、公理的推論の境界を区別する必要があることを示唆する。
9.2 機械による推論の限界
機械は規則に従う以上、規則そのものが抱える限界も引き受ける。したがって、完全な自動推論には原理的制約がある。
この制約は、知能の機械化を否定するものではないが、無制限な自動化への期待を修正する。
9.3 形式主義との関係
形式主義は、数学を記号操作として理解する立場である。決定不能性は、この立場においても、形式化だけでは全てを尽くせないことを示す。
そのため、形式主義は強力な方法論でありながら、万能の解釈ではないことが明らかになる。
10 主要な研究者
決定不能性の理論は、複数の研究者の独立した貢献によって形成された。彼らの成果は、計算、証明、論理の関係を再定義した。
それぞれの業績は互いに補完的であり、今日の理論の基礎をなしている。
10.1 アラン・チューリング
アラン・チューリングは、計算の形式モデルとしてチューリング機械を提案し、停止性問題の決定不能性を示した。彼の業績は、計算可能性理論の中心を成す。
また、機械的計算の概念を明確にしたことで、以後の理論研究に強い影響を与えた。
10.2 クルト・ゲーデル
クルト・ゲーデルは、不完全性定理を通じて、形式体系の限界を示した。自己言及と算術化の技法は、後の決定不能性研究にも大きな示唆を与えた。
彼の成果は、数学的真理が証明可能性より広いことを明らかにした点で重要である。
10.3 アロンゾ・チャーチ
アロンゾ・チャーチは、ラムダ計算を用いて計算可能性を解析し、一般的な決定不能性の理解に寄与した。彼の研究は、関数計算の形式的側面を洗練させた。
また、チャーチ・チューリングのテーゼの形成にも深く関わっている。
10.4 スティーヴン・コール・クリーネ
スティーヴン・コール・クリーネは、再帰理論の発展に重要な役割を果たした。帰納的可算性や再帰定理の整備を通じて、計算理論の基盤を強化した。
彼の仕事は、決定不能性を単発の結果ではなく、体系的な理論として理解するのに貢献した。