二階述語論理
二階述語論理(にかいじゅつごろんり、英: second-order predicate logic)あるいは単に二階論理(にかいろんり、英: second-order logic)は、一階述語論理を拡張した論理体系であり、一階述語論理自体も命題論理を拡張したものである。二階述語論理もさらに高階述語論理や型理論に拡張される。
一階述語論理と同様に議論領域(ドメイン)の考え方を使う。ドメインとは、量化可能な個々の元の集合である。一階述語論理では、そのドメインの個々の元が変項の値となり、量化される。例えば、一階の論理式 ∀x (x ≠ x + 1) では、変項 x は任意の個体を表す。二階述語論理は個体の集合を変項の値とし、量化することができる。例えば、二階の論理式 ∀S ∀x (x ∈ S ∨ x ∉ S) は、個体の全ての集合 S と全ての個体 x について、x が S に属するか、あるいは属さないかのどちらかであるということを主張している。最も一般化された二階述語論理は関数の量化をする変項も含んでいる(詳しくは後述)。
二階述語論理の文法から、どの式が論理式かが示される。一階述語論理の文法に加えて、二階述語論理では変項に様々な「種(sort)」または「型(type)」がある。
個体の集合を値とする変項。S をこの種の変項とし、一階の項 t があるとき、式 t ∈ S は原子論理式である(S(t) あるいは St とも書かれる)。個体群の集合はドメインの単項関係と見ることもできる。
任意の自然数 k について、個体の全ての k-項関係を値とする変項。R をそのようなk-項関係の変項とし、一階の項 t1,..., tk があるとき、式 R(t1,...,tk) は原子論理式である。
任意の自然数 k について、ドメインの k 個の元を引数として1つの元を値とする関数を値とする変項。f をそのようなk引数の関数シンボルとし、一階の項 t1,...,tk があるとき、式 f(t1,...,tk) は一階の項である。
これらの変項の種について、全称記号や存在記号を使った論理式を構築可能である。
二階述語論理の「文(sentence)」は、いかなる種の自由変項も持たない論理式をいう。
上記のうちドメインの部分集合だけを変項として追加したものを「単項二階述語論理(monadic second-order logic)」と呼ぶ。上記の全種の変項を追加した二階述語論理を「完全二階述語論理(full second-order logic)」と呼んで、単項版と区別することがある。
一階述語論理と同様、二階述語論理でも非論理記号を含むことがある。ただし、論理式を構成する全ての項は一階の項(一階の変項で置換可能)か二階の項(適切な種の二階の変項で置換可能)でなければならない。