一階述語論理

(サイエンス)

【いっかいじゅつごろんり】

命題論理に対し定数記号、変数記号、関数記号、述語記号などの表現を追加し、個体の量化を導入した論理体系。命題の意味内容を捨象した命題論理の体系に対して、述語論理は意味内容に立ち入った論理の体系であると考えられる。現代的な数学の枠組み（ZF、ZFC集合論）は一階述語論理で形式化されている。述語や関数の量化を導入した二階述語論理、さらに一般化された高階述語論理も存在する。

形式的定義

我々は先ず述語論理の体系で扱う記号の集まり(alphabet)を用意する。それらは変数記号( $x_0,\ldots,x_n,\ldots$ )、関数記号( $f_0,\ldots,f_n,\ldots$ )、述語記号( $p_0,\ldots,p_n,\ldots$ )、論理記号( $\vee,\wedge,\supset,\neg,\forall,\exists$ )からなる。関数記号と述語記号にはarityとよばれる自然数が一意的に定まっている。arity 0の関数記号を特に定数記号と呼ぶ。
note. 変数記号をさらに自由変数と束縛変数とを区別して導入することもあるが、ここでは2つを区別しない。arityを正整数に制限し、定数記号を別に用意することもあるが、ここでは定数記号は関数記号の一種として導入する。

関数記号を代表して $f,g,h,\ldots$ 、変数記号を代表して $x,y,z,\ldots$ 、述語記号を代表して $p,q,r,\ldots$ 、定数記号を代表して $a,b,c,\ldots$ などの(メタな)記号を用いる。

次にこれらの記号を並べる規則(文法)を定める。まず我々は項(term)と呼ばれる記号列を定め、それらを対象とする述語、論理記号の組み合わせによって論理式(formula)を定義する。これらは帰納的に定義される。

変数記号は項である。
$f$ がarity nの関数記号で、 $t_1,\ldots,t_n$ が項ならば、 $(ft_1\cdots t_n)$ も項である。 $f(t_1,\ldots,t_n)$ と定義しても同じことである。
以上より項とわかるもののみが項である。

曖昧ないときは適切に括弧を省略したり、関数記号を中置したりする。例えば $c$ がarity 0、すなわち定数記号ならば、 $(c)$ の最外部の括弧は外す。例えば $(+ab)$ は $(a+b)$ と中置する。

$p$ がarity nの述語記号で、 $t_1,\ldots,t_n$ が項ならば、 $(pt_1\cdots t_n)$ は論理式である。
$\alpha$ と $\beta$ が論理式ならば、 $(\alpha\vee\beta)$ も論理式である。 $\forall$ 、 $\exists$ を除く他の論理記号に関しても同様である。
$x$ が変数記号で、 $\alpha$ が論理式ならば、 $(\forall x\alpha)$ も論理式である。 $\exists$ に関しても同様である。
以上より論理式とわかるもののみが論理式である。

省略記法に関する注意は項の場合と同じである。 $\vee$ が``or"を表す論理記号だからといって $(\alpha\vee\beta)\vee\gamma$ の括弧を外して $\alpha\vee\beta\vee\gamma$ などとしてはいけない。何故ならばそのような省略が正当であることを我々はまだ証明していないからである。何となれば``or"が結合的でないような公理を設定できるからである。