決定可能性と決定不能性：機械的に判定できる問題とは - 記号論理学
決定可能性（decidability）は、問題を機械的に解けるかどうかを問う概念です。記号論理学と計算理論が交わる重要なテーマであり、チューリングやチャーチの先駆的研究に基づいています。
決定可能性の定義
理論 T が決定可能（decidable）であるとは、任意の文 φ について、φ が T の定理かどうかを判定するアルゴリズムが存在することです。
アルゴリズムとは、有限時間で必ず停止し、正しい答え（YES または NO）を返す手続きです。
機械的な判定手続きが存在する。入力に対して必ず有限時間で答えが出る。
そのような手続きが存在しない。一般には解けない問題。
決定不能の例：述語論理の妥当性
チャーチとチューリングは1936年に、一階述語論理の妥当性問題が決定不能であることを証明しました。
与えられた論理式 φ がトートロジー（すべての解釈で真）かどうかを判定する一般的なアルゴリズムは存在しません。
決定可能。真理値表で機械的に判定できる。
決定不能。一般的な判定アルゴリズムは存在しない。
セミ決定可能性
述語論理は決定不能ですが、セミ決定可能（semi-decidable）です。
妥当な式については、有限時間で「YES」と答えられます（完全性定理より証明が見つかる）。しかし、妥当でない式については、探索が永遠に続く可能性があり、「NO」と確定できないことがあります。
妥当な式
証明を探索
有限時間で発見（YES）
妥当でない式の場合、反例を見つけられるかもしれませんが、保証はありません。
決定可能な断片
述語論理全体は決定不能ですが、いくつかの断片は決定可能です。
単項述語論理：述語がすべて1項（単項）の場合、妥当性は決定可能です。
いくつかの冠頭標準形の断片：量化子のパターンが限定された式のクラスで、決定可能なものがあります。
単項述語論理、∀∃ 形式の式など。限定されたクラス。
2項述語と2つの量化子があれば、もう決定不能に十分。
停止問題との関係
決定不能性の最も有名な例は、チューリングの停止問題です。
「プログラム P を入力 x で実行すると停止するか」を判定する一般的なアルゴリズムは存在しません。この結果は対角線論法で証明されます。
述語論理の決定不能性は、停止問題の決定不能性に帰着させて証明できます。論理式の妥当性判定ができれば、停止問題も解けることになり、矛盾します。
帰納的可算と帰納的
決定可能性に関連する概念として、帰納的可算性があります。
集合 S が帰納的可算（recursively enumerable）であるとは、S の要素を列挙するアルゴリズムが存在することです。S と補集合 S̄ が両方とも帰納的可算なら、S は帰納的（recursive）、つまり決定可能です。
YES も NO も有限時間で判定できる。
YES は判定できるが、NO は確定しないことがある。
述語論理の妥当な式の集合は、帰納的可算だが帰納的ではありません。
実用的な含意
決定不能性は理論的な限界ですが、実用的には多くの問題が解けます。
自動定理証明器は、多くの場合に有用な結果を出します。決定不能性は「最悪の場合」の限界であり、実際に遭遇する問題の多くは扱えます。
また、決定可能な断片（命題論理、特定の述語論理の断片など）だけで十分な応用も多くあります。
次回からは、発展的なトピックとして様相論理を紹介します。
