Loading article…
論理学において、真偽判定問題は、正しい答えを導き出すための有効な方法が存在する場合に決定可能である。論理体系は、論理的に妥当な式（または定理）の集合への所属を効果的に決定できる場合に決定可能である。ゼロ階論理（命題論理）は決定可能であるが、一階論理および高階論理は決定不可能である。固定された論理体系における理論（論理的帰結のもとで閉じている文の集合）は、任意の式がその理論に含まれるかどうかを判断するための有効な方法が存在する場合に決定可能である。多くの重要な問題は決定不可能であり、つまり、それらの問題に対して所属を決定するための有効な方法（すべての場合において有限時間（ただし非常に長い時間になる可能性もある）後に正しい答えを返す方法）は存在しないことが証明されている。
論理体系には、証明可能性の概念などを規定する構文的要素と、論理的妥当性の概念を規定する意味的要素の両方が含まれる。体系の論理的に妥当な式は、特にゲーデルの完全性定理によって意味的帰結と構文的帰結の等価性が確立される一階述語論理においては、体系の定理と呼ばれることがある。線形論理などの他の分野では、構文的帰結（証明可能性）関係を用いて体系の定理を定義することができる。
論理体系が決定可能であるとは、任意の論理式がその論理体系の定理であるかどうかを判定する有効な方法が存在する場合をいう。例えば、命題論理は決定可能である。なぜなら、真理値表を用いることで、任意の命題式が論理的に妥当であるかどうかを判定できるからである。
一般的に、一階述語論理は決定不可能である。特に、等号と少なくとも１つ以上の他の述語記号（ ２つ以上の引数を持つ）を含む任意のシグネチャにおける論理的妥当性の集合は決定不可能である。 [ 1 ]二階述語論理や型理論など、一階述語論理を拡張する論理体系も決定不可能である。
ただし、同一性を持つ単項述語論理の妥当性は判定可能である。このシステムは、関数記号を持たず、等号以外の述語記号が常に1つ以上の引数を取らないシグネチャに限定された一階述語論理である。
論理体系の中には、定理の集合だけでは十分に表現できないものがあります。（例えば、クリーネの論理には定理が全くありません。）このような場合、論理体系の決定可能性に関する別の定義がよく用いられます。これは、式の妥当性だけでなく、より一般的な何かを決定するための効果的な方法を求めるものです。例えば、シーケントの妥当性、あるいは論理の帰結関係{(Г, A ) | Г ⊧ A } などが挙げられます。
理論とは、論理的帰結に関して閉じていると仮定されることが多い、一連の式の集合である。理論の決定可能性とは、理論のシグネチャに含まれる任意の式が与えられたときに、その式が理論の要素であるか否かを判定する有効な手続きが存在するかどうかに関わる問題である。理論が固定された公理の集合の論理的帰結の集合として定義される場合、決定可能性の問題は自然に生じる。
理論の決定可能性については、いくつかの基本的な結果があります。矛盾のない（パラコンシステントでない）理論はすべて決定可能です。なぜなら、その理論のシグネチャに含まれるすべての式は、その理論の論理的帰結であり、したがってその理論の要素となるからです。計算可能かつ列挙可能な完全な 一階述語論理はすべて決定可能です。決定可能な理論の拡張は、決定可能ではない場合があります。例えば、命題論理には決定不可能な理論が存在しますが、妥当性の集合（最小の理論）は決定可能です。
すべての無矛盾拡張が決定不能であるという性質を持つ無矛盾理論は、本質的に決定不能であると言われる。実際、すべての無矛盾拡張は本質的に決定不能である。体論は決定不能ではあるが、本質的に決定不能ではない。ロビンソン算術は本質的に決定不能であることが知られており、したがって、ロビンソン算術を含む、あるいは解釈するすべての無矛盾理論もまた（本質的に）決定不能である。
決定可能な一階理論の例としては、実閉体理論やプレスバーガー算術などがあり、群論やロビンソン算術は決定不可能な理論の例である。
決定可能な理論には以下のようなものがある（Monk 1976、p. 234）：[ 2 ]
決定可能性を確立するために使用される方法には、量化子除去、モデルの完全性、およびŁoś–Vaughtテストなどがあります。
決定不可能な理論には以下のようなものがある：[ 2 ]
解釈可能性法は、理論の決定不能性を確立するためによく用いられる。本質的に決定不能な理論Tが、一貫性のある理論Sにおいて解釈可能であれば、Sもまた本質的に決定不能である。これは、計算可能性理論における多対一還元という概念と密接に関連している。
理論または論理体系の決定可能性よりも弱い性質として、半決定可能性がある。理論が半決定可能であるとは、任意の式が与えられたときに、その式が理論に含まれる場合は肯定的な結果が得られ、含まれない場合は全く得られないか否定的な結果が得られるような、明確に定義された方法が存在する場合をいう。言い換えれば、論理体系が半決定可能であるとは、各定理が最終的に生成されるような定理の系列を生成する明確な方法が存在する場合をいう。これは決定可能性とは異なる。なぜなら、半決定可能な体系では、式が定理ではないことを検証する有効な手順が存在しない可能性があるからである。
決定可能な理論や論理体系はすべて半決定可能ですが、一般にその逆は成り立ちません。理論が決定可能であるのは、その理論と補集合の両方が半決定可能である場合に限ります。例えば、一階述語論理の論理的妥当性の集合V は半決定可能ですが、決定可能ではありません。これは、任意の論理式AがVに含まれないかどうかを判定する有効な方法がないためです。同様に、計算可能な列挙可能な一階述語論理の公理の集合の論理的帰結の集合は半決定可能です。上記で挙げた決定不可能な一階述語論理の例の多くは、この形式です。
決定可能性と完全性を混同してはならない。例えば、代数的に閉じた体の理論は決定可能ではあるが不完全であるのに対し、+と×を含む言語における自然数に関するすべての真の1階述語論理の命題の集合は完全ではあるが決定不可能である。残念ながら、用語の曖昧さから、「決定不可能な命題」という用語は、独立した命題の同義語として使われることがある。
決定可能集合の概念と同様に、決定可能な理論または論理体系の定義は、有効な方法または計算可能な関数のいずれかで与えることができます。これらは一般的に、チャーチのテーゼに従って同等であると考えられています。実際、論理体系または理論が決定不可能であることの証明は、計算可能性の形式的な定義を使用して適切な集合が決定可能集合ではないことを示し、次にチャーチのテーゼを援用して、その理論または論理体系が有効な方法では決定不可能であることを示します（Enderton 2001、pp. 206以降）。
ゲームの中には、判定可能性に基づいて分類されているものがある。
{{citation}}ISBN /日付の不一致（ヘルプ）