決定可能性（論理）

論理学では、正しい答えを導き出す有効な方法が存在する場合、真偽判定問題は決定可能です。ゼロ階論理（命題論理）は決定可能ですが、一階論理と高階論理は決定できません。論理体系は、論理的に有効な式（または定理）の集合への所属が効果的に決定できる場合、決定可能です。固定された論理体系における理論（論理的帰結の下で閉じられた文の集合）は、任意の式が理論に含まれているかどうかを判断する有効な方法がある場合、決定可能です。多くの重要な問題は決定不可能です。つまり、それらの問題に対して所属を決定する（すべてのケースにおいて有限の時間、場合によっては非常に長い時間の後に正しい答えを返す）有効な方法は存在し得ないことが証明されています。

各論理システムには、とりわけ証明可能性の概念を決定する統語的要素と、論理的妥当性の概念を決定する意味的要素の両方が付属しています。システムの論理的に妥当な式は、特にゲーデルの完全性定理によって意味的帰結と統語的帰結の同値性が確立される一階述語論理のコンテキストでは、システムの定理と呼ばれることがあります。線型論理などの他の設定では、統語的帰結（証明可能性）関係を使用してシステムの定理を定義する場合があります。

任意の式が論理システムの定理であるかどうかを判断するための効果的な方法がある場合、論理システムは決定可能です。たとえば、命題論理は、任意の命題式が論理的に有効であるかどうかを判断するために真理値表法を使用できるため、決定可能です。

一階述語論理は一般に決定可能ではない。特に、等号と2つ以上の引数を持つ少なくとも1つの他の述語を含むシグネチャの論理妥当性の集合は決定可能ではない。 ^{[1]一階述語論理を拡張した}二階述語論理や型理論などの論理システムも決定不可能である。

ただし、同一性を持つモナド述語計算の有効性は決定可能です。このシステムは、関数記号を持たず、等号以外の関係記号が 1 つ以上の引数を取らないシグネチャに制限された一階述語論理です。

一部の論理システムは、定理の集合だけでは適切に表現できません。(たとえば、クリーネの論理には定理がまったくありません。) このような場合、論理システムの決定可能性の代替定義がよく使用されます。この定義では、式の妥当性だけでなく、より一般的な何か、たとえば、シークエントの妥当性、または論理の結果関係{(Г, A ) | Г ⊧ A } を決定するための効果的な方法が求められます。

理論とは、論理的帰結の下で閉じていると想定される一連の式です。理論の決定可能性は、理論のシグネチャに任意の式が与えられた場合に、その式が理論のメンバーであるかどうかを決定する有効な手順があるかどうかに関係します。決定可能性の問題は、理論が固定された公理の集合の論理的帰結の集合として定義されている場合に自然に発生します。

理論の決定可能性に関する基本的な結果がいくつかあります。すべての (非矛盾のない) 矛盾した理論は決定可能です。なぜなら、理論のシグネチャ内のすべての式は理論の論理的帰結であり、したがって理論のメンバーとなるからです。すべての完全な 再帰的に列挙可能な一階の理論は決定可能です。決定可能な理論の拡張は決定可能ではない場合があります。たとえば、命題論理には決定不可能な理論がありますが、妥当性の集合 (最小の理論) は決定可能です。

すべての整合的な拡張が決定不可能であるという性質を持つ整合的な理論は、本質的に決定不可能であると言われています。実際、すべての整合的な拡張は本質的に決定不可能です。体の理論は決定不可能ですが、本質的に決定不可能ではありません。ロビンソン算術は本質的に決定不可能であることが知られており、したがってロビンソン算術を含むか解釈するすべての整合的な理論も（本質的に）決定不可能です。

決定可能な一階理論の例には、実閉体理論やプレスブルガー算術が含まれ、一方、群論やロビンソン算術は決定不可能な理論の例です。

決定可能な理論としては次のようなものがある（Monk 1976, p. 234）：^[2]

• 1915 年にレオポルド・レーヴェンハイムによって確立された、等式のみを含む署名における一階論理妥当性の集合。
• 1959 年に Ehrenfeucht によって確立された、等式と 1 つの単項関数を含む署名における一階論理妥当性の集合。
• 等式と加法を備えた符号における自然数の第一階理論。プレスブルガー算術とも呼ばれる。その完全性は1929 年にモイシェシュ・プレスブルガーによって確立された。
• 等式と乗算を含む署名内の自然数の第一階理論。スコーレム算術とも呼ばれます。
• 1940 年にアルフレッド・タルスキによって確立されたブール代数の第一階理論(1940 年に発見されたが、1949 年に発表された)。
• 1949 年にタルスキによって確立された、与えられた特性を持つ代数的に閉じた体の第一階の理論。
• 1949 年にタルスキによって確立された実閉順序体の一階理論(タルスキの指数関数問題も参照)。
• 1949年にタルスキによって確立されたユークリッド幾何学の第一階理論。
• 1955 年にシュミエルフによって確立されたアーベル群の第一階理論。
• 1959年にシュヴァーベザーによって確立された双曲幾何学の第一階理論。
• 1980 年代から今日まで研究されてきた集合論の特定の決定可能な部分言語。(Cantone et al.、2001)
• 木のモナド的第二階理論( S2Sを参照)。

決定可能性を確立するために使用される方法には、量指定子除去、モデルの完全性、およびŁoś-Vaughtテストが含まれます。

決定不可能な理論としては次のようなものがある（Monk 1976, p. 279）：^[2]

• 1953 年にTrakhtenbrotによって確立された、等式と、少なくとも 2 個の引数を持つ関係シンボル、または 2 個の単項関数シンボル、または少なくとも 2 個の引数を持つ 1 個の関数シンボルのいずれかを含む、任意の 1 階署名の論理妥当性の集合。
• 1949 年にタルスキとアンジェイ・モストフスキによって確立された、加算、乗算、等式を含む自然数の第一階理論。
• 1949 年にジュリア・ロビンソンによって確立された、加算、乗算、等式を含む有理数の第一階理論。
• 群の第一階理論は、1953年にアルフレッド・タルスキによって確立されました。 ^[3] 注目すべきことに、群の一般理論だけでなく、いくつかのより具体的な理論、例えば（1961年にマルチェフによって確立された）有限群の理論も決定不可能です。マルチェフはまた、半群の理論と環の理論が決定不可能であることを確立しました。ロビンソンは1949年に体の理論が決定不可能であることを確立しました。
• ロビンソン算術（およびペアノ算術などの一貫した拡張）は、1950 年にラファエル ロビンソンによって確立されたように、本質的に決定不可能です。
• 等式と2つの関数記号を持つ第一階理論^[4]

解釈可能性法は、理論の決定不能性を確立するためによく使用されます。本質的に決定不能な理論T が、一貫性のある理論Sで解釈可能である場合、Sも本質的に決定不能です。これは、計算可能性理論における多対一還元の概念と密接に関連しています。

決定可能性よりも弱い理論または論理システムの特性は、半決定可能性です。理論が半決定可能であるのは、任意の式が与えられたときに、その式が理論内にある場合はその結果が正として到達し、そうでなければ決して到達せず、そうでなければ負として到達するという明確に定義された方法がある場合です。論理システムが半決定可能であるのは、各定理が最終的に生成されるような一連の定理を生成する明確に定義された方法がある場合です。これは決定可能性とは異なります。半決定可能なシステムでは、式が定理でないことを確認するための効果的な手順がない場合があるからです。

すべての決定可能な理論または論理体系は半決定可能ですが、一般にその逆は真ではありません。理論が決定可能であるのは、理論とその補集合の両方が半決定可能である場合のみです。たとえば、一階述語論理の論理妥当性の集合Vは半決定可能ですが、決定可能ではありません。この場合、任意の式AについてAがVに含まれないかどうかを判断する効果的な方法がないためです。同様に、一階述語公理の再帰的に列挙可能な集合の論理的帰結の集合は半決定可能です。上記で示した決定不可能な一階述語理論の例の多くは、この形式です。

決定可能性を完全性と混同しないでください。たとえば、代数的に閉じた体の理論は決定可能ですが不完全です。一方、+ と × を含む言語における非負整数に関するすべての真の一階述語の集合は完全ですが決定不可能です。残念ながら、用語上の曖昧さとして、「決定不可能な述語」という用語は、独立述語の同義語として使用されることがあります。

決定可能集合の概念と同様に、決定可能な理論または論理システムの定義は、有効な方法または計算可能な関数のいずれかで与えることができます。これらは、チャーチのテーゼに従って一般的に同等であると見なされます。実際、論理システムまたは理論が決定不可能であることの証明では、計算可能性の正式な定義を使用して、適切な集合が決定可能集合ではないことを示し、次にチャーチのテーゼを使用して、理論または論理システムが有効な方法では決定できないことを示します (Enderton 2001、206 ページ以降)。

いくつかのゲームは、決定可能性に応じて分類されています。

• チェスは決定可能である。^{[5] [6]} 完全情報を持つ他のすべての有限の2人用ゲームでも同じことが言える。
• 無限チェス（ルールと駒に制限あり）におけるn詰めは決定可能である。^{[7] [8]}しかし、有限個の駒を持つポジションでは、有限のnに対してn 詰めではないが、強制的に勝つポジションが存在する。^[9]
• 有限の盤面（ただし時間は無制限）上で不完全な情報を扱うチームゲームの中には、決定不可能なものもあります。^[10]

• 結論問題
• 存在定量化

• バーワイズ、ジョン(1982)、「一階述語論理入門」、バーワイズ、ジョン (編)、『数理論理学ハンドブック』、『論理学と数学の基礎研究』、アムステルダム: 北ホラント、ISBN 978-0-444-86388-1
• Cantone, D.; Omodeo, EG; Policriti, A. (2013) [2001], コンピューティングのための集合理論。決定手順から集合による論理プログラミングまで、Monographs in Computer Science、Springer、ISBN 9781475734522
• チャグロフ、アレクサンダー、ザカリャシェフ、マイケル（1997）、様相論理、オックスフォード論理ガイド、第35巻、オックスフォード大学出版局、ISBN 978-0-19-853779-3、MR  1464942
• デイヴィス、マーティン(2013) [1958]、計算可能性と解決不能性、ドーバー、ISBN 9780486151069
• エンダートン、ハーバート（2001）、論理学への数学的入門（第2版）、アカデミックプレス、ISBN 978-0-12-238452-3
• Keisler, HJ (1982)、「モデル理論の基礎」、Barwise, Jon (編)、『数理論理学ハンドブック』 、論理学と数学の基礎研究、アムステルダム:北ホラント、ISBN 978-0-444-86388-1
• モンク、J.ドナルド（2012）[1976]、数学論理、シュプリンガー・フェアラーク、ISBN 9781468494525