決定可能性

決定可能性とは

数理論理学において、決定可能性（decidability）とは、ある論理式の集合のメンバーシップを実効的に決定できる性質を指します。つまり、与えられた論理式がその集合に属するかどうかを、計算可能な方法で判断できるということです。

形式体系、例えば命題論理は、論理的に妥当な論理式（定理）の集合のメンバーシップを実効的に決定できる場合に決定可能であると言えます。同様に、特定の論理体系における理論（論理的帰結で閉じている論理式の集合）は、任意の論理式がその理論に含まれるかどうかを決定する実効的な方法が存在する場合、決定可能であるとされます。もしそのような方法が存在しなければ、その理論は決定不能です。

計算可能性との関係

決定可能な集合、理論、論理体系の定義には、「実効的方法」や「計算可能関数」という概念が用いられます。これらの概念は一般にチャーチ＝チューリングのテーゼによって定義されます。具体的には、ある論理体系や理論が決定不能であることを証明する場合、計算可能性の形式定義を用いて、ある集合が決定可能ではないことを示し、チャーチのテーゼを適用することで、その理論や論理体系が実効的な方法では決定できないことを結論づけます。

論理体系の決定可能性

論理体系は、証明可能性を定める統語論的要素と、論理的妥当性を定める意味論的要素を併せ持ちます。ある体系で証明可能な論理式は、その体系の定理と呼ばれます。一階述語論理では、ゲーデルの完全性定理により、証明可能性と論理的妥当性が同値であることが示されますが、線形論理など他の体系では必ずしもそうではありません。

論理体系が決定可能であるとは、任意の論理式がその体系の定理であるかどうかを決定する実効的な方法が存在することを意味します。例えば、命題論理は真理値表を用いることで、任意の論理式の妥当性を決定できるため、決定可能です。

しかし、一般的に一階述語論理は決定可能ではありません。特に、等式と2つ以上の引数を持つ述語がシグネチャ（非論理記号の一覧）に含まれる場合、論理的妥当性の集合は決定不能となります。二階述語論理や型理論も同様に決定不能です。

ただし、等式を持つ単項述語計算の妥当性は決定可能です。この体系は、関数記号を含まず、関係記号が等式以外はすべて引数が1つ以下であるという制限を加えた一階述語論理です。

論理体系によっては、定理の集合だけでは十分に表現できない場合（例えば、3値論理には定理が存在しない）もあります。その場合、論理式の妥当性ではなく、シークエントの妥当性や、帰結関係といったより一般的な概念を決定する実効的方法を問うことで、決定可能性を定義します。

理論の決定可能性

理論とは、論理式の集合であり、論理的帰結の下で閉じているものを指します。理論の決定可能性は、与えられた論理式がその理論の一部であるかどうかを決定する実効的な手続きが存在するかどうかを問います。理論が、公理の集合からの論理的帰結の集合として定義されている場合、この問題は自然に発生します。

決定可能な一階の理論の例としては、実閉体の理論やプレスブルガー算術があります。一方、決定不能な理論の例としては、群の理論やロビンソン算術が挙げられます。

理論の決定可能性に関する基本的な結論として、矛盾を含む理論は決定可能であるという事実があります。なぜなら、その理論のシグネチャにある論理式はすべてその理論の論理的帰結になり得るため、理論の一部となるからです。また、完全で帰納的可算な一階の理論は決定可能です。

決定可能な理論を拡張した場合、必ずしも決定可能とは限りません。例えば、命題論理には決定不能な理論も存在しますが、最小の理論である妥当性の集合は決定可能です。

無矛盾の理論で、そのすべての無矛盾な拡張が決定不能である場合、その理論は本質的に決定不能であるとされます。ロビンソン算術は本質的に決定不能であることが知られており、ロビンソン算術を含むまたは翻訳可能なすべての無矛盾な理論も（本質的に）決定不能です。

決定可能な理論の例

以下に決定可能な理論の例を挙げます。

等式のみを持つ一階の論理的妥当性の集合
等式と1つの単項関数を持つ一階の論理的妥当性の集合
等式と加法のみを持つ一階の理論（プレスブルガー算術）
ブール代数の一階の理論
任意の標数の代数的閉体の一階の理論
実閉体の一階の理論
ユークリッド幾何学の一階の理論
双曲幾何学の一階の理論
集合論の決定可能な部分言語

決定可能性を証明する手法には、量化子除去、モデル完全性、Vaught's testなどがあります。

決定不能な理論の例

以下に決定不能な理論の例を挙げます。

一階のシグネチャに等式と以下のいずれかを含む理論での論理的妥当性の集合
2つ以上の引数をとる関係記号
2つの単項関数記号
2引数以上の1つの関数記号
自然数の加法、乗法、等式を持つ一階の理論
有理数の加法、乗法、等式を持つ一階の理論
群の一階の理論
半群の理論
環の理論
体の理論
ペアノ算術（強く決定不能）

理論の決定不能性を証明する際には、変換可能性（interpretability）が用いられます。決定不能な理論Tが無矛盾な理論Sに変換可能である場合、Sも同様に決定不能であることが示されます。これは、計算可能性理論における多対一還元の概念と密接に関連しています。

半決定可能性

決定可能性よりも弱い属性として、半決定可能性（semidecidability）という概念があります。理論が半決定可能であるとは、与えられた論理式が理論に含まれる場合には正しい答えを返す実効的な方法が存在するが、理論に含まれない論理式に対しては答えられない可能性がある状態を指します。

論理体系が半決定可能であるとは、すべての定理を生成できる実効的な方法が存在することを意味します。半決定可能な論理体系は、ある論理式が定理でないことをチェックする実効的な方法を持たない可能性がある点で、決定可能な論理体系と異なります。

決定可能なすべての理論や論理体系は半決定可能でもありますが、逆は成り立ちません。理論が決定可能であることと、その理論とその補理論が共に半決定可能であることは同値です。例えば、一階論理の論理的妥当性の集合は半決定可能ですが、決定可能ではありません。これは、任意の論理式がその集合に属さないことを決定する実効的な方法が存在しないためです。

完全性との関係

決定可能性と完全性は異なる概念です。例えば、代数的閉体の理論は決定可能ですが完全ではありません。一方、加法と乗法を持つ言語における非負整数に関するすべての真の一階の文の集合は完全ですが、決定不能です。

参考文献

Barwise, Jon (1982年), “Introduction to first-order logic”, in Barwise, Jon, Handbook of Mathematical Logic
Chagrov, Alexander; Zakharyaschev, Michael (1997年), Modal logic
Davis, Martin (1958年), Computability and Unsolvability
Keisler, H. J. (1982年), “Fundamentals of model theory”, in Barwise, Jon, Handbook of Mathematical Logic

もう一度検索