決定問題（Entscheidungsproblem）：論理学と計算における決定問題

形式的な定式化と範囲

非形式的にいえば、決定問題は、ある形式体系の記述とその体系内の論理式を入力として受け取り、つねに「真」（その式が証明可能または妥当である）か「偽」（そうではない）を出力するアルゴリズム、すなわち有効で機械的な方法を求めるものである。ヒルベルトのプログラムと同時代の研究者たちは、論理体系および算術に対するこのような決定法を探求した。この定式化は、形式言語、構文、ならびに計算またはアルゴリズムについての有効な概念に依存する。

歴史的展開

ダフィット・ヒルベルトらは1920年代に、明確なメタ数学的問題を提起した。1930年代には複数の論理学者による研究が、機械的に決定できる事柄の限界を明らかにした。アロンゾ・チャーチはラムダ計算と有効計算可能性の概念を用い、算術に適用される一階述語論理について一般的な決定手続きが存在しないことを示した。これとは独立に、アラン・チューリングは計算を捉えるための抽象的な機械モデルを導入し、機械の振る舞いに関する決定不能問題を定式化することによって、これと同値の否定的結果を証明した。

証明の中心的な考え方

両方の方法は、既知の決定不能な問題からの帰着を構成した。チャーチはラムダ定義可能関数の表現力を利用して論理的妥当性を符号化した。一方、チューリングは自身の機械に関する停止問題を定式化し、それにはアルゴリズムによる解法がないことを示した。有効計算可能な関数については両者の計算の形式的概念が一致するため、この二つの結果は両立する。さらに、自然数に関する文、すなわち算術についての決定不能性も、これらの構成から導かれる。

帰結と重要性

決定問題に対する否定的な解決は、長期にわたる重要な含意をもつ。

• 形式化には内在的な限界があることを示す。ある真の数学的文は、単一のアルゴリズムでは決定できない。
• 原理的に解決可能な問題を明確にしたことにより、計算可能性理論および計算量理論の発展に直接つながった。
• 形式体系、自動定理証明、ならびに決定可能な理論と決定不能な理論の分類に影響を与えた。

関連する区別と例

すべての形式体系が決定不能であるわけではない。制限された理論の中には決定手続きをもつものがあり、たとえばプレスバーガー算術は決定可能であるのに対し、ペアノ算術は決定不能である。決定問題が扱うのは、文全体の類に対する普遍的な解法の存在である。個別の断片や言語は、その表現力に応じて決定可能にも決定不能にもなりうる。歴史的な論文や技術的解説については、形式言語に関する資料、数理論理学の入門書、またはチューリングとチャーチに関する伝記や解説を参照できる。

簡潔な要約や現代的な扱いについては、停止問題、帰着、アルゴリズムによる決定可能性の境界を説明する概説書や信頼できるオンライン資料が有用である。こうした資料には、普遍的な決定アルゴリズムが存在しえない理由を示す例や証明の概略が含まれることが多い。ヒルベルトのプログラムと、この否定的解決が数学の形式的基礎に対する期待をどのように変えたかについての歴史的議論も参照されたい。