これは何

プログラムの性質を数学的に扱ったりするときや型理論のベースとして一階述語論理がサラッと登場したりするので、雑に触れてみよう、という記事。

量化記号(quantifier)

一階述語論理では命題(命題論理式)に以下の量化記号を導入する。

• $\forall$ : 全称記号(universal quantifier)
  • 任意の...について 、という意味
  • すべてのものは条件を満たすということを表現
• $\exists$ : 存在記号(existential quantifier)
  • ある...について、という意味
  • 条件を満たすものが存在するということを表現

述語(predicate)

0個以上の変数を受け取り真偽を返す記述のこと。雑にいうと、boolを返す関数。命題との違いは、命題はそれ自体で真または偽が定まるが、述語は変数(引数)を受け取って真偽が決まる。（0個以上なので、引数はなくてもよい）

例えば $x + x = 2$ とか $x < 0$ など。

引数として $x$ を持つ記述は $P(x)$ のように表現する。引数がない場合はカッコを付けずに述語名のみを書く。

例として、$x + x = 2$ を $P(x)$ としたとき、$P(1)$ は真、$P(2)$は偽。

述語と量化記号

引数を1個以上もつ述語は、量化記号をくっつけて量についても表現ができる。

量化記号は右側に掛かる。

例

$(\forall x)P(x)$ は すべての $x$ に対して $P(x)$ が成り立つ ということを言っている。

例えば $P(x)$ が「人間である」という述語とすると、$(\forall x)P(x)$ は「全ての $x$ は人間である」という意味。例えば $x$ がプログラマーなら、全てのプログラマーは人間である、という意味になりこの論理式は 真 と判定できる。

複数の量化記号の例

$(\forall x)(\forall y)(x + y = 0)$ は すべての $x$ と $y$ の組み合わせについて $x + y = 0$ が成り立つ、ということを表している。例えばこの論理式の対象の集合が $\mathbb{ Z }$ (整数全体の集合の記号)の場合、この論理式は 偽 である。

$(\exists y)(\forall x)P(x, y)$ は ある $y$ はすべての $x$ に対して $P$ が成り立つ という意味。たとえば $\mathbb{ Z }$ において、$P$ が $x \times y = 0$ ならこれは 真。

ある $y$ はすべての $x$ について $x \times y = 0$ となるかどうか考えると、たとえば $0$ はすべての $x$ について $x \times 0 = 0$ となる。