決定可能性
理論や論理体系について決定可能性よりも弱い属性として半決定可能性 (semidecidability) がある。理論が半決定可能であるとは、任意の論理式を与えられたとき、その論理式がその理論に含まれる場合は正しい答を出せる実効的方法があるが、その理論に含まれない論理式の場合は答を出せない可能性があることを言う。論理体系が半決定可能であるとは、全ての定理を最終的に生成できるような定理(だけ)を生成する実効的方法が存在することを言う。このような半決定可能な論理体系が決定可能な論理体系と異なるのは、ある論理式が定理でないことをチェックする実効的方法を持たない可能性がある点である。
全ての決定可能な理論や論理体系は半決定可能でもあるが、その逆は真ではない。ある理論が決定可能であることと、その理論とその補理論が共に半決定可能であることは同値である。例えば、一階論理の論理的妥当性の集合 V は半決定可能だが、決定可能ではない。この場合の理由は、任意の論理式 A について、A が V に属さないことを決定する実効的方法がないためである。同様に、一階の公理の任意の帰納的可算集合の論理的帰結の集合は半決定可能である。上の節で挙げた決定不能な一階の理論の多くもこのタイプである。
論理体系には、(証明可能性の概念を定める)統語論的要素と(論理的妥当性の概念を定める)意味論的要素が共に備わっている。ある体系で証明可能な論理式をその体系の定理と呼ぶ。一階述語論理ではゲーデルの完全性定理により証明可能性と論理的妥当性の同値性が示されているため、定理とは妥当な論理式のことでもあるが、線形論理などの他の体系では一般にそうとは限らない。
論理体系が決定可能であるとは、任意の論理式がその論理体系の定理か否かを決定する実効的方法があることを意味する。例えば、命題論理は任意の論理式が論理的に妥当か否かを真理値表を使って決定できるため、決定可能である。
一階述語論理は一般に決定可能ではない。特に、シグネチャ(非論理記号の一覧)に等式と2つ以上の引数を持つ述語が少なくとも1つ含まれている場合、論理的妥当性の集合は決定可能ではない。一階述語論理を拡張した二階述語論理や型理論も同様に決定不能である。
ただし、等式を持つ単項述語計算の妥当性は決定可能である。この体系は、シグネチャに関数シンボルを含まず、関係シンボルは等式以外は引数が1つ以下になるよう一階述語論理を制限したものである。
論理体系によっては、定理の集合だけでは十分に表現できないものもある(例えば、3値論理には全く定理がない)。そのような場合、論理体系の決定可能性の別の定義を使うことが多い。それは、論理式の妥当性よりももっと一般的な何かの決定の実効的方法を問うものである。例えば、シークエントの妥当性、あるいはその論理における帰結関係 {(Г, A) | Г ⊧ A} などである。