1.3 述語論理 | 情報数学入門

「すべてのユーザーは名前を持つ」「ある商品が在庫切れである」。このような文を数学的に表現するには、命題論理だけでは足りない。「すべて」や「ある」という量化の概念を扱う述語論理は、データベース設計から型理論まで、プログラミングの随所に顔を出す。

述語論理全称量化子存在量化子命題述語

命題論理から述語論理へ

命題論理（propositional logic）は、「真または偽」が定まる文（命題）を扱う。「今日は雨だ」「xは3より大きい」などである。しかし命題論理では、「すべてのxについて」「あるxが存在して」という表現ができない。

述語論理（predicate logic、一階述語論理とも）は、この制限を取り払う。変数と量化子を導入し、より表現力の高い論理体系を構築する。

述語（Predicate）

変数を含み、その変数に具体的な値を代入すると命題になるもの。

例：P(x) = 「xは偶数である」

P(2) は真、P(3) は偽となる。

全称量化子 ∀（for all）

「すべての〜について」を表す。

∀x P(x) は「すべてのxについてP(x)が真」の意味。

反例が1つでもあれば偽。

存在量化子 ∃（there exists）

「〜が存在する」を表す。

∃x P(x) は「P(x)を満たすxが少なくとも1つ存在する」の意味。

1つでも真になる例があれば真。

量化子の否定には重要な規則がある。

元の式	否定	意味
¬(∀x P(x))	∃x ¬P(x)	「すべてがPでない」=「Pでないものが存在する」
¬(∃x P(x))	∀x ¬P(x)	「Pが存在しない」=「すべてがPでない」

これはド・モルガンの法則の拡張と見なせる。

プログラミングでよく見る表現を述語論理で書いてみる。

データベース制約：「すべての注文には顧客が存在する」は外部キー制約として実装される。

バリデーション：「すべての入力フィールドが有効である」をチェックする処理。

配列メソッド：every()は∀、some()は∃に対応する。

型システム：ジェネリクスの型制約は全称量化。

論理推論：知識グラフでの推論規則は述語論理で記述される。

形式検証：プログラムの正しさを証明する際の仕様記述言語。