論理体系の決定可能性
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/08/01 10:10 UTC 版)
論理体系には、(主に論理式の観念を決定する)統語論的要素と(論理的妥当性の観念を決定する)意味論的要素が共に備わっている。ある体系で論理的に妥当な論理式をその体系の定理などと呼ぶ。一階述語論理では、ゲーデルの完全性定理が意味論的帰結と統語論的帰結が同値であることを立証している。線形論理などの他の設定では、統語論的帰結(立証性)関係はその体系の定理を定義するのに使われる可能性がある。 論理体系が決定可能であるとは、任意の論理式がその論理体系の定理か否かを決定する実効的方法があることを意味する。例えば、命題論理は任意の論理式が論理的に妥当か否かを真理値表を使って決定できるため、決定可能である。 一階述語論理は一般に決定可能ではない。特に、シグネチャ(非論理記号の一覧)に等式と2つ以上の引数を持つ述語が少なくとも1つ含まれている場合、論理的妥当性の集合は決定可能ではない。一階述語論理を拡張した二階述語論理や型理論も同様に決定不能である。 ただし、等式を持つ単項述語計算の妥当性は決定可能である。この体系は、シグネチャに関数シンボルを含まず、関係シンボルは等式以外は引数が1つ以下になるよう一階述語論理を制限したものである。 論理体系によっては、定理の集合だけでは十分に表現できないものもある(例えば、3値論理には全く定理がない)。そのような場合、論理体系の決定可能性の別の定義を使うことが多い。それは、論理式の妥当性よりももっと一般的な何かの決定の実効的方法を問うものである。例えば、シークエントの妥当性、あるいはその論理における帰結関係 {(Г, A) | Г ⊧ A} などである。
※この「論理体系の決定可能性」の解説は、「決定可能性」の解説の一部です。
「論理体系の決定可能性」を含む「決定可能性」の記事については、「決定可能性」の概要を参照ください。
- 論理体系の決定可能性のページへのリンク