計算可能性理論および計算複雑性理論において、決定不能問題とは、常に正しいイエスかノーの答えに導くアルゴリズムを構築することが不可能であることが証明されている決定問題のことである。停止問題はその一例である。任意のプログラムが実行時に最終的に停止するかどうかを正しく判定するアルゴリズムは存在しないことが証明されている。[ 1 ]
決定問題とは、ある無限集合の入力に対して「はい」または「いいえ」の答えを必要とする質問です。[ 2 ]これらの入力は数値(例えば、「入力は素数ですか?」という決定問題)または形式言語の文字列などの他の種類の値です。
決定問題の形式的表現は、自然数のサブセットです。自然数に関する決定問題の場合、その集合は、決定問題が「はい」と答える数で構成されます。例えば、「入力は偶数か?」という決定問題は、偶数の集合として形式化されます。入力が文字列やより複雑な値で構成される決定問題は、特定のゲーデル数化によって、決定問題の基準を満たす入力に対応する数の集合として形式化されます。
決定問題Aは、 Aの形式化された集合が再帰的集合である場合、決定可能または実質的に解決可能であると呼ばれる。そうでない場合、Aは決定不可能と呼ばれる。問題A が再帰的に列挙可能な集合である場合、その問題は部分的に決定可能、半決定可能、解決可能、または証明可能であると呼ばれる。[注 1 ]
計算可能性理論において、停止問題は決定問題であり、以下のように定式化できる。
アラン・チューリングは1936年に、チューリングマシン上で実行可能な、あらゆるプログラムと入力の組み合わせに対して停止問題を解決する汎用アルゴリズムは存在し得ないことを証明した。したがって、停止問題はチューリングマシンにとって決定不能である。
ゲーデルの不完全性定理によって提起される概念は、停止問題によって提起される概念と非常によく似ており、証明もかなり似ています。実際、第一不完全性定理の弱い形式は、停止問題の決定不能性から容易に導かれる帰結です。この弱い形式は、完全かつ健全な自然数の有効な公理化は不可能であると主張する点で、不完全性定理の標準的な記述とは異なります。「健全」の部分が弱化の理由です。つまり、問題となっている公理系は、自然数に関する真の命題のみを証明する必要があるということです。健全性は一貫性を意味するため、この弱い形式は強い形式の系と見なすことができます。ゲーデルの第一不完全性定理の標準的な記述は、命題の真偽値には全く関心がなく、数学的証明によってそれを見つけることが可能かどうかという問題のみに関心があることに注意することが重要です。
定理の弱い形式は、停止問題の決定不能性から次のように証明できます。[ 3 ]自然数に関するすべての真の1階論理ステートメントの健全(したがって一貫性のある)かつ完全な有効公理化があると仮定します。すると、これらのステートメントをすべて列挙するアルゴリズムを構築できます。これは、自然数nが与えられたときに、自然数に関する真の1階論理ステートメントを計算するアルゴリズムN ( n ) が存在し、すべての真のステートメントに対して、 N ( n ) がそのステートメントを生成するようなnが少なくとも 1 つ存在することを意味します。ここで、表現aを持つアルゴリズムが入力iで停止するかどうかを決定したいとします。このステートメントは、 H ( a , i )のような1階論理ステートメントで表現できることがわかっています。公理化が完全であることから、 N ( n ) = H ( a , i )となるnが存在するか、 N ( n ′ ) = ¬H ( a , i )となるn ′が存在するかのいずれかであることがわかります。したがって、H ( a , i )またはその否定が見つかるまですべてのnについて反復すると、必ず停止し、さらに、その結果得られる答えは(健全性により)真となります。これは、停止問題を判定するアルゴリズムが得られることを意味します。このようなアルゴリズムは存在しないことがわかっているので、自然数に関するすべての真の一階述語論理の命題について、健全かつ完全な有効な公理化が存在するという仮定は偽でなければなりません。
決定不能な問題は、論理、抽象機械、位相幾何学など、さまざまなトピックに関連しています。決定不能な問題は数えきれないほど存在するため、[注2 ]無限長のリストであっても、必然的に不完全です。
現代において「決定不能」という言葉には2つの異なる意味がある。1つ目はゲーデルの定理に関連して用いられる意味で、特定の演繹体系において証明も反駁もできない命題を指す。2つ目は計算可能性理論に関連して用いられる意味で、命題ではなく決定問題に適用される。決定問題とは、それぞれが「はい」か「いいえ」の答えを必要とする、可算無限個の質問の集合である。このような問題は、問題集合内のすべての質問に正しく答える計算可能な関数が存在しない場合、決定不能であると言われる。この2つの意味の関連性は、決定問題が(再帰理論的な意味で)決定不能である場合、問題内のすべての質問Aに対して「 Aに対する答えははい」または「 Aに対する答えはいいえ」のいずれかを証明する、一貫性のある有効な形式体系が存在しないということである。
「 undecidable」という単語には2つの意味があるため、 「証明も反証もできない」という意味では、「undecidable」の代わりに「 independent」という用語が使われることがある。しかし、「independent」の使い方も曖昧である。単に「証明できない」という意味で使われることもあり、独立した命題が反証可能かどうかは未解決のまま残される。
ある特定の演繹体系における命題の決定不能性は、それ自体では、その命題の真偽値が明確に定義されているか、あるいは他の手段で決定できるかという問題には答えない。決定不能性とは、検討対象の特定の演繹体系ではその命題の真偽を証明できないことを意味するにすぎない。真偽値が決して分からない、あるいは明確に定義されていない、いわゆる「絶対的に決定不能な」命題が存在するかどうかは、様々な哲学学派の間で議論の的となっている。
用語の2番目の意味で決定不能であると疑われた最初の問題の一つは、 1911年にマックス・デーンが最初に提起した群の単語問題で、2つの単語が同値であるかどうかを判定するアルゴリズムが存在しない有限表示群が存在するかどうかを問うものです。これは1955年にセルゲイ・ノビコフによって証明されました。[ 4 ]
ゲーデルとポール・コーエンの共同研究により、決定不能な命題(第一の意味で)の具体的な例が2つ示された。連続体仮説はZFC (集合論の標準的な公理化)では証明も反証もできず、選択公理はZF (選択公理を除くZFCのすべての公理)では証明も反証もできない。これらの結果は不完全性定理を必要としない。ゲーデルは1940年に、これらの命題のいずれもZFまたはZFC集合論では反証できないことを証明した。1960年代にコーエンは、いずれもZFからは証明できず、連続体仮説はZFCからは証明できないことを証明した。
1900年に次の世紀の数学者への挑戦として提起されたヒルベルトの第10問題は、1970年にユーリ・マティヤセヴィチによって決定不能であることが証明された。ヒルベルトの挑戦は、ディオファントス方程式のすべての解を見つけるアルゴリズムを求めるものであった。ディオファントス方程式はフェルマーの最終定理のより一般的な場合であり、整数係数を持つ任意の数の変数の多項式の整数根を求めるものである。方程式は1つしかないが変数はn個あるため、複素平面上には無限に多くの解が存在し(そして簡単に見つけることができる)、しかし、解が変数の整数値に制限されると、この問題は解決不可能になる。マティヤセヴィチは、ディオファントス方程式を再帰的に列挙可能な集合にマッピングし、ゲーデルの不完全性定理を適用することによって、この問題が解決不可能であることを示した。[ 5 ]
1936年、アラン・チューリングは、停止問題(チューリングマシンが与えられたプログラムで停止するかどうかという問題)が、この用語の2番目の意味において決定不能であることを証明した。この結果は後にライスの定理によって一般化された。
1973年、サハロン・シェラは、群論におけるホワイトヘッド問題が、標準集合論では、その用語の最初の意味で決定不能であることを示した。 [ 6 ]
1977年、パリスとハリントンは、ラムゼーの定理の一種であるパリス・ハリントン原理が、ペアノ公理によって与えられる算術の公理化においては決定不能であるが、より大きな2階算術体系においては真であることが証明できることを証明した。
コンピュータ科学に応用されているクラスカルの木の定理は、ペアノ公理系では決定不能であるが、集合論では証明可能である。実際、クラスカルの木の定理(またはその有限形式)は、述語主義と呼ばれる数学哲学に基づいて受け入れられる原理を体系化した、はるかに強力な体系においても決定不能である。
グッドスタインの定理は、カービーとパリスがペアノ算術では決定不能であることを示した、ラムゼーの自然数理論に関する定理である。
グレゴリー・チャイティンは、アルゴリズム情報理論において決定不能な命題を生み出し、その枠組みの中で別の不完全性定理を証明した。チャイティンの定理は、十分な算術演算を表現できる理論には上限cが存在し、その理論において特定の数がcより大きいコルモゴロフ複雑性を持つことは証明できないと述べている。ゲーデルの定理が嘘つきのパラドックスに関連しているのに対し、チャイティンの結果はベリーのパラドックスに関連している。
2007年、研究者のカーツとサイモンは、1970年代のJHコンウェイによる先行研究に基づいて、コラッツ問題の自然な一般化は決定不能であることを証明した。[ 7 ]
2019年、ベン・デイビッドらは学習モデル(EMXと名付けられた)の例を構築し、EMXにおける学習可能性が標準集合論では決定不能な関数のファミリーを示した。[ 8 ] [ 9 ]