Logo

Nola's Backyard

一階述語論理

対象を表す変数、対象の性質・関係を表す述語、そして「すべて」(∀)(\forall)／「ある」(∃)(\exists)を使って、対象についての命題を記述する論理。

Info

このノートでは、主に「どのような論理式を書けるか」という構文を扱う。
シグネチャ、対象領域、構造、モデルなど、論理式に意味を与える仕組みについては一階述語論理の意味論を参照。

# 命題論理との違い

命題論理では、文全体を1つの命題記号として扱う。

  • PP：太郎はプログラマーである
  • QQ：太郎はHaskellを使う
  • P⇒QP\Rightarrow Q

一階述語論理では、文を「対象」と「性質・関係」に分解できる。

  • Programmer(x)\mathrm{Programmer}(x)：xx はプログラマー
  • Uses(x,y)\mathrm{Uses}(x,y)：xx は yy を使う
  • ∀x (Programmer(x)⇒Uses(x,Git))\forall x\,(\mathrm{Programmer}(x)\Rightarrow\mathrm{Uses}(x,\mathrm{Git}))

# なぜ「一階」なのか

量化できるのが、数や人などの対象そのものだから。

∀x Even(x) \forall x\,\mathrm{Even}(x)

ここでは対象を表す変数 xx を量化している。一方、

∀P P(x) \forall P\,P(x)

のように述語 PP 自体を量化するのは二階以上の論理になる。

プログラミング風の比較
  • 命題論理：何も量化しない
  • 一階述語論理：値について量化する
  • 二階以上の論理：述語や関係などについても量化する

# 一階言語の構文

# シグネチャ

一階述語論理では、最初に使用できる非論理記号と、その引数の個数を決める。この記号の構成をシグネチャという。

  • 定数記号：特定の対象を指す
  • 関数記号：対象から別の対象を作る
  • 述語記号：対象の性質や関係を表す

例えば、

L={0,+,Even} L=\{0,+,\mathrm{Even}\}

では、00 が定数記号、++ が2引数の関数記号、Even\mathrm{Even} が1引数の述語記号である。

Hint

シグネチャが決めるのは、その言語で何を表現できるかである。各記号が具体的に何を意味するかは、構造によって与えられる。

# 項

項は、対象を指すための式。

  • 変数：x,yx,y
  • 定数記号：00
  • 関数記号を項に適用したもの：x+0x+0

述語や等号の引数には項を置く。

# 述語と原子論理式

述語は、対象の性質や対象同士の関係を表す。

  • Even(x)\mathrm{Even}(x)：「xx は偶数」
  • Loves(x,y)\mathrm{Loves}(x,y)：「xx は yy を愛している」

述語を項に適用した式や、2つの項を等号で結んだ式を原子論理式という。

Even(x),Loves(x,y),x+0=0 \mathrm{Even}(x),\qquad \mathrm{Loves}(x,y),\qquad x+0=0
Hint

📝プログラマーのための圏論の「述語は Bool を返す関数」という見方をすれば、次のように書ける。

even  :: Integer -> Bool
loves :: Person -> Person -> Bool

# 論理式

原子論理式を、論理演算子と量化子によって組み合わせたもの。

  • ¬φ\lnot\varphi：「φ\varphi ではない」
  • φ∧ψ\varphi\land\psi：「φ\varphi かつ ψ\psi」
  • φ∨ψ\varphi\lor\psi：「φ\varphi または ψ\psi」
  • φ⇒ψ\varphi\Rightarrow\psi：「φ\varphi ならば ψ\psi」
  • ∀x φ\forall x\,\varphi：「すべての xx について φ\varphi」
  • ∃x φ\exists x\,\varphi：「φ\varphi を満たす xx が存在する」
Example
∀x (Human(x)⇒Mortal(x)) \forall x\,(\mathrm{Human}(x)\Rightarrow\mathrm{Mortal}(x))

すべての人間は死ぬ。

∃x (Programmer(x)∧Uses(x,Haskell)) \exists x\,(\mathrm{Programmer}(x)\land\mathrm{Uses}(x,\mathrm{Haskell}))

Haskellを使うプログラマーが少なくとも一人いる。

# 自由変数と束縛変数

Even(x) \mathrm{Even}(x)

の xx は、量化子によって束縛されていない自由変数である。この式は xx の値が決まらないと真偽が確定しない。

∃x Even(x) \exists x\,\mathrm{Even}(x)

では、xx は ∃x\exists x によって束縛されている。自由変数を持たない論理式を文といい、その構造において真偽が確定する。

# 等号

等号 == は、2つの項が対象領域内の同じ対象を指すことを表す。

等号つき一階述語論理では、次の3つの層に分けて考える。

  1. 構文
    • == は特別な原始記号であり、ほかの論理記号から定義しない
  2. 意味論
    • == は対象領域上の同一性として解釈される
    • 対象領域を DD とすれば、== が表す関係は {(d,d)∣d∈D}\{(d,d)\mid d\in D\}
  3. 証明体系
    • 同一性の振る舞いを、反射律と代入原理などによって形式化する
Caution

通常の二項述語 EE を「同値関係かつ、その言語で表現可能なすべての論理式について代入原理を満たす」と定めても、本当の同一性になるとは限らない。
それは「その言語では区別できない」という観察的同値性にすぎない可能性がある。

Note

== は対象領域が決まれば、非論理記号のシグネチャに依存せずに定まる。
そのため、任意のシグネチャから本当の同一性を一般的に定義することはできず、等号つき一階述語論理では == を特別な論理記号として扱う。