決定可能性

決定可能（けっていかのう、英: decidable）は、数理論理学または現代論理学において、論理式の集合のメンバーシップの決定をする実効的（effectiveな）方法が存在することを指す。決定可能性（けっていかのうせい、英: decidability）は、そのような属性を指す。命題論理のような形式体系は、論理的に妥当な論理式（または定理）の集合のメンバーシップを実効的に決定できるなら、決定可能である。ある決まった論理体系における理論（論理的帰結で閉じている論理式の集合）は、任意の論理式がその理論に含まれるか否かを決定する実効的方法があれば、決定可能である。そうでなければ、決定不能である。

計算可能性との関係

決定可能集合の概念と同様、決定可能な理論や論理体系の定義は、「実効的方法 (effective method)」や「計算可能関数 (computable function)」によって与えられる。これらは一般にチャーチ＝チューリングのテーゼと等しいと見なされている。実際、論理体系や理論が決定不能であるという証明は、計算可能性の形式定義を使い、ある適当な集合が決定可能集合ではないことを示し、チャーチのテーゼを使って、その理論や論理体系が実効的方法では決定可能でないことを示す^[1]。

論理体系の決定可能性

論理体系には、（証明可能性の概念を定める）統語論的要素と（論理的妥当性の概念を定める）意味論的要素が共に備わっている。ある体系で証明可能な論理式をその体系の定理と呼ぶ。一階述語論理ではゲーデルの完全性定理により証明可能性と論理的妥当性の同値性が示されているため、定理とは妥当な論理式のことでもあるが、線形論理などの他の体系では一般にそうとは限らない。

論理体系が決定可能であるとは、任意の論理式がその論理体系の定理か否かを決定する実効的方法があることを意味する。例えば、命題論理は任意の論理式が論理的に妥当か否かを真理値表を使って決定できるため、決定可能である。

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

ただし、等式を持つ単項述語計算の妥当性は決定可能である。この体系は、シグネチャに関数シンボルを含まず、関係シンボルは等式以外は引数が1つ以下になるよう一階述語論理を制限したものである。

論理体系によっては、定理の集合だけでは十分に表現できないものもある（例えば、3値論理には全く定理がない）。そのような場合、論理体系の決定可能性の別の定義を使うことが多い。それは、論理式の妥当性よりももっと一般的な何かの決定の実効的方法を問うものである。例えば、シークエントの妥当性、あるいはその論理における帰結関係 {(Г, A) | Г ⊧ A} などである。

理論の決定可能性

理論は論理式の集合であり、論理的帰結の下で閉じているとする。理論の決定可能性を問うということは、その理論のシグネチャに含まれる任意の論理式を与えられたとき、その論理式がその理論の一部かどうかを決定する実効的手続きが存在するかどうかを問うことである。理論が公理の決まった集合からの論理的帰結の集合として定義されているとき、この問題は自然に生じる。決定可能な一階の理論の例として、実閉体の理論やプレスブルガー算術があり、決定不能な理論の例として、群の理論やロビンソン算術がある。

理論の決定可能性について、いくつかの基本的結論がある。矛盾を含む理論は決定可能である。その理論のシグネチャにある論理式はどれでもその理論の論理的帰結になりうるため、理論の一部となりうるからである。完全で帰納的可算な一階の理論は決定可能である。決定可能な理論を拡張したものは決定可能でない場合がある。例えば、命題論理には決定不能な理論もあるが、最小の理論である妥当性の集合は決定可能である。

無矛盾の理論で、全ての無矛盾な拡張が決定不能であるとき、本質的に決定不能であるという。実際、全ての矛盾のない拡張は本質的に決定不能である。体の理論は決定不能だが、本質的に決定不能ではない。ロビンソン算術は本質的に決定不能であることが知られており、ロビンソン算術を内包するか翻訳した全ての無矛盾な理論も（本質的に）決定不能である。

決定可能な理論の例

決定可能な理論を以下に挙げる^[2]。

シグネチャに等式しかない一階の論理的妥当性の集合。Leopold Löwenheim が1915年に立証。
シグネチャに等式と1つの単項関数しかない一階の論理的妥当性の集合。1959年、Ehrenfeucht が立証。
シグネチャに等式と加法しかない一階の理論。プレスブルガー算術とも呼ぶ。その完全性は1929年、Mojżesz Presburger が立証。
ブール代数の一階の理論。1949年、アルフレト・タルスキが立証。
任意の標数の代数的閉体の一階の理論。1949年、タルスキが立証。
実閉体の一階の理論。1949年、タルスキが立証。
ユークリッド幾何学の一階の理論。1949年、タルスキが立証。
双曲幾何学の一階の理論。1959年、Schwabhäuser が立証。
1980年代から今日にかけて、集合論の決定可能な部分言語が研究されている^[3]。

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

決定不能な理論の例

決定不能な理論を以下に挙げる^[2]

一階のシグネチャに等式と下記のいずれかを含む理論での論理的妥当性の集合。1953年、Boris Trakhtenbrot が立証。
- 2つ以上の引数をとる関係シンボル
- 2つの単項関数シンボル
- 2引数以上の1つの関数シンボル
自然数の加法・乗法・等式のある一階の理論。1949年、タルスキと Andrzej Mostowski が立証。
有理数の加法・乗法・等式のある一階の理論。1949年、ジュリア・ロビンソンが立証。
群の一階の理論。1961年、Mal'cev が立証。Mal'cev は半群の理論と環の理論も決定不能であることを立証した。ロビンソンは1949年、体の理論が決定不能であることを立証した。
ペアノ算術は強く決定不能である。（ゲーデルの不完全性定理参照）

理論の決定不能性を立証する手法として、変換可能性 (interpretability) を利用することが多い。決定不能な理論 T が無矛盾な理論 S に変換できるとき、S も同様に決定不能であるとする考え方である。これは、計算可能性理論の多対一還元の概念と密接に関連している。

半決定可能性

理論や論理体系について決定可能性よりも弱い属性として半決定可能性 (semidecidability) がある。理論が半決定可能であるとは、任意の論理式を与えられたとき、その論理式がその理論に含まれる場合は正しい答を出せる実効的方法があるが、その理論に含まれない論理式の場合は答を出せない可能性があることを言う。論理体系が半決定可能であるとは、全ての定理を最終的に生成できるような定理（だけ）を生成する実効的方法が存在することを言う。このような半決定可能な論理体系が決定可能な論理体系と異なるのは、ある論理式が定理でないことをチェックする実効的方法を持たない可能性がある点である。

全ての決定可能な理論や論理体系は半決定可能でもあるが、その逆は真ではない。ある理論が決定可能であることと、その理論とその補理論が共に半決定可能であることは同値である。例えば、一階論理の論理的妥当性の集合 V は半決定可能だが、決定可能ではない。この場合の理由は、任意の論理式 A について、A が V に属さないことを決定する実効的方法がないためである。同様に、一階の公理の任意の帰納的可算集合の論理的帰結の集合は半決定可能である。上の節で挙げた決定不能な一階の理論の多くもこのタイプである。

完全性との関係

決定可能性は完全性とは異なる。例えば代数的閉体の理論は決定可能だが完全ではなく、加法と乗法のある言語における非負整数に関する全ての真の一階の文の集合は完全だが決定不能である。

脚注

^ Enderton, Herbert (2001年), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3
^ ^a ^b Monk, J. Donald (1976年), Mathematical Logic, Berlin, New York: Springer-Verlag
^ Cantone, D., E. G. Omodeo and A. Policriti, "Set Theory for Computing. From Decision Procedures to Logic Programming with Sets," Monographs in Computer Science, Springer, 2001.

参考文献

Barwise, Jon (1982年), “Introduction to first-order logic”, in Barwise, Jon, Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1
Chagrov, Alexander; Zakharyaschev, Michael (1997年), Modal logic, Oxford Logic Guides, 35, The Clarendon Press Oxford University Press, ISBN 978-0-19-853779-3
Davis, Martin (1958年), Computability and Unsolvability, McGraw-Hill Book Company, Inc, New York
Keisler, H. J. (1982年), “Fundamentals of model theory”, in Barwise, Jon, Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1

[1] Enderton, Herbert (2001年), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3

[Monk1976-2] Monk, J. Donald (1976年), Mathematical Logic, Berlin, New York: Springer-Verlag

[3] Cantone, D., E. G. Omodeo and A. Policriti, "Set Theory for Computing. From Decision Procedures to Logic Programming with Sets," Monographs in Computer Science, Springer, 2001.

[1]

[2]

[3]