主に『論理と計算のしくみ』を参考に。

構文論

一階述語論理の構文論では述語論理式 (predicate formula) 、または単に論理式と呼ばれるものを定義する。述語論理式は述語記号、項、論理記号から構成される。

述語記号

述語記号 (predicate symbol) は述語 (predicate) を表す記号である。

述語はざっくりいえば変数を含む主張である。例えば「x は果物である」という主張は述語と考えられる。述語単体に真偽を割り当てることはできないが、変数に値を代入することで命題と同様に扱うことができる。

\( P(x, y) \) のように書いて変数 \( x, y \) を含む述語 \( P \) を表す。

項

項 (term) は関数記号、定数記号、個体変数から構成される記号のことである。

  • 関数記号 (function symbol)
    • 関数を表す記号で \( f(t_{1}, t_{2}) \) のように表記する
  • 定数記号 (constant symbol)
    • 定数を表す記号
  • 個体変数 (individual variable)
    • 述語記号の説明で 「変数」 という記述をしたが、これは個体変数と同義
    • 一階の変数と呼ぶこともある
      • 二階の変数は集合や関数を表す変数

定数記号を引数 0 の関数記号とみなした場合、項は以下の生成規則 T で表現される。

\( T ::= V \ \vert \ F(X) \ \vert \ F() \\ X ::= T \ \vert \ T, X \)

(ただし \( V \) は個体変数、 \( F \) は関数記号を生成するとみなす)

例えば \( f, g \) を関数記号、 \( 2, 3 \) を定数記号として \( f(g(2,3)) \) は項である。

また述語記号と項から作られる式は原子論理式 (atomic formula) と呼ばれる。 例えば \( P \) を二項述語として \( P(f(2), g(2,3)) \) は原子論理式である。

論理記号

述語論理で使用する論理記号は、命題論理で使用したものに以下の2つを加えたものになる。

  • 全称量化子 (universal quantifier): \( \forall \)
  • 存在量化子 (existential quantifier): \( \exists \)

述語論理式

述語論理式は原子論理式と論理記号から構成される。 \( P \) を原子論理式とした場合、述語論理式は以下の生成規則 A で表現される。

\( A ::= P \ \vert \ \lnot A \ \vert \ A \land A \ \vert \ A \lor A \ \vert \ A \rightarrow A \ \vert \ \forall x A \ \vert \ \exists x A \)

自由と束縛

述語論理で使用する変数には自由と束縛という概念が存在する。これは定積分における変数の扱いに近いものがある。

  • 束縛変数
    • 全称量化子、存在量化子で修飾された変数 ( \( \forall x, \exists x \) )
  • 自由変数
    • 束縛変数ではない変数
  • α変換
    • 束縛変数の名前を換えること
    • \( \forall x P(x) \) の \( x \) は 束縛されており、 α変換で \( \forall y P(y) \) としても同じ命題である
  • 閉じている
    • 自由変数を含まない論理式は「閉じている (closed である)」 と表現される
    • 閉じていない論理式も代入により閉じたものに変換することができる
  • 代入
    • \( A[t] \) で論理式 \( A \) の自由な変数 \( x \) に \( t \) を代入することを表す

意味論

述語論理式の意味を定義するには構造と付値が必要である。

構造

構造 (structure) は以下の2つから成る。

  • 変数が動き得る範囲である領域 (universe)
  • 関数記号、述語記号の解釈 (interpretation)

構造 \( I \) の領域を \( U \) とすると、関数記号、述語記号はそれぞれ以下のように解釈される。 ここで、 \( \mathbb{B} \) は真偽値の集合 \( \{ T, F \} \) である。

  • 関数記号: \( \mathbb{U}^n \rightarrow \mathbb{U} \) という関数
  • 述語記号: \( \mathbb{U}^n \rightarrow \mathbb{B} \) という関数

付値

付値 (valuation) は自由変数に領域内の要素を対応付ける関数である。

『論理と計算のしくみ』では構造の例として以下のものを挙げている。

  • 定数記号: \( 0, 1 \)
  • 関数記号: \( +, \times \)
  • 述語記号: \( =, < \)
  • 領域: \( \mathbb{N} \) (ただし 0 を含む)
  • 解釈 \( I \)
    • \( I(0) = 0 \)
    • \( I(1) = 1 \)
    • \( I(+)(x,y) = x + y \)
    • \( I(\times)(x,y) = x \times y \)
    • \( I(=)(x,y) = T \) iff \( x == y \)
    • \( I(<)(x,y) = T \) iff \( x < y \)

恒真

論理式 \( A \) が任意の構造と付値で真ならば、 \( A \) は恒真 (valid) であるという。 恒真であることを \( \models A \) と書くこともある。

充足可能と充足不能

論理式 \( A \) がある構造と付値で真ならば、 \( A \) は充足可能 (satisfiable) であるという。 論理式の集合に対しても同様に充足可能が定義される。

充足可能でない場合を充足不能であるという。

全称閉包と存在閉包

論理式 \( A \) の自由変数を \( x_1, x_2, …, x_n \) とする。このとき \( A \) の全称閉包 (universal closure) 、存在閉包 (existential closure) は以下のように定義される。

  • 全称閉包: \( \forall x_1 \forall x_2 … \forall x_n A \)
  • 存在閉包: \( \exists x_1 \exists x_2 … \exists x_n A \)

全称閉包、存在閉包は \( A \) に関わらず閉じた式となる。

コンパクト性

閉じた述語論理式のコンパクト性はエルブランの定理から導出される。

スコーレム化

任意の閉じた論理式 \( A \) は \( \forall x_1 … \forall x_n A[x_1, …, x_n] \) という形の閉じた論理式に書き換えることができる。このとき \( A \) に量化子は出現しない。

スコーレム化の例:

\( P(c) \land \forall x ( \exists y ( P(x) \rightarrow Q(y) ) \land \lnot Q(x) ) \\ \equiv P(c) \land \forall x \exists y ( ( P(x) \rightarrow Q(y) ) \land \lnot Q(x) ) ) \\ \equiv \forall x \exists y ( P(c) \land ( ( P(x) \rightarrow Q(y) ) \land \lnot Q(x) ) ) \\ \equiv \forall x ( P(c) \land ( ( P(x) \rightarrow Q(f(x)) ) \land \lnot Q(x) ) ) \)

エルブラン構造

スコーレム化した論理式 \( \forall x_1 … \forall x_n A[x_1, …, x_n] \) に対し、エルブラン構造 (Herbrand’s structure) を定義する。

エルブラン構造の領域はスコーレム化した論理式中に含まれる定数記号、関数記号から作られる項の全体とし、エルブラン領域 (Herbrand’s universe) と呼ぶ。ただし定数記号が一つも存在しない場合、適当なものを一つ加える。

例えば

\( \forall x \forall y ( P(x) \land Q(x,f(x,c))) \)

に対し、エルブラン領域 \( \mathbb{H} \) は

\( \{ c, f(c,c), f(f(c,c),c), … \} \)

のようになる。

エルブラン領域の解釈は任意の閉じた項 \( t \) が \( t \) 自身に解釈されるように定義する。 つまり

\( I_{H}: \mathbb{H} \rightarrow \mathbb{H} \) は \( I_{H}(t) = t \in \mathbb{H} \)

となる。

論理式を真に解釈するエルブラン構造が存在するならば、その論理式はエルブラン充足可能であるという。エルブラン充足可能でない場合はエルブラン充足不能。

閉じた論理式 \( \forall x_1 … \forall x_n A[x_1, … x_n] \) に関しては、充足可能ならばエルブラン充足可能である。

エルブランの定理

エルブランの定理 (Herbrand’s theorem) は以下のような定理である。

\( \forall x_1 … \forall x_n A[x_1, … x_n] \) が充足不能ならば、閉じた項 \(t_{ij} \in \mathbb{H} \ (1 \leq i \leq m, 1 \leq j \leq n) \) が存在して、 \( \{ A[t_{11}, …, t_{1n}], …, A[t_{m1}, …, t_{mn}] \} \) が命題論理において充足不能になる。

なおエルブランの定理の逆も成立する。

  • エルブランの定理により述語論理の充足不能性が命題論理の充足不能性に還元される
  • 充足不能な論理式の全体は帰納的に可算であるが、帰納的ではない
    • 論理式 \( A \) が充足不能である場合、部分的なアルゴリズムで充足不能であることをいつかは知ることができる
    • 論理式 \( A \) が充足不能でない場合、充足不能でないことを一般に知ることはできない

例えば \( \forall x ( P(x) \land \lnot P(f(x))) \) の充足不能性はエルブランの定理により示される。

  1. エルブラン領域 \( \mathbb{H} = \{ c, f(c), f(f(c), … \} \) を定義する
  2. \( (P(x) \land \lnot P(f(x))) \) に \( c \) , \( f(c) \) を代入した命題論理式の集合を考える
    • \( \{ (P(c) \land \lnot P(f(c)) ), (P(f(c)) \land \lnot P(f(f(c))) \} \)
  3. このとき \( P(f(c)) \) , \( \lnot P(f(c)) \) を同時に満たすエルブラン解釈は存在せず、充足不能である
  4. エルブランの定理より \( \forall x ( P(x) \land \lnot P(f(x))) \) は充足不能である

コンパクト

\( \varGamma \) を閉じた論理式の集合とする。 \( \varGamma \) をスコーレム化した論理式の集合とエルブラン構造を考えることで、以下の定理が示される (詳細は専門書を参考)。

\( \varGamma \) が充足不能ならば、 \( \varGamma \) の有限部分集合 \( \Delta \) が存在して、 \( \Delta \) は充足不能である。

演繹体系

命題論理と同様にいくつかの演繹体系が考えられている。

  • ヒルベルト流
  • シーケント計算
  • 導出原理

いずれも一階述語論理において健全であり完全である。