第7章 標準形とエルブラン定理(2)

スコーレム標準形

スコーレム標準形とは、存在限量子を含まず、全称限量子の変数が全て異なる冠頭標準形のことである。

スコーレム標準形は任意の論理式に同値な論理式が存在するとは限らないが、任意のAに対してスコーレム標準形Bが存在し、
　Aが充足不能 iff Bが充足不能
が成り立つ。（Aを真にする解釈が存在しなければBを真にする解釈は存在しない）

A = ∀x∀y∃z(P0⊃P1(z,f(x))
B = ∀x∀y (P0⊃P1(g(xy),f(x))
このとき関数記号gをスコーレム関数記号という
Aの式では、全てのx,yについてzが存在するという意味なので、x,yとzの間に何らかの対応関係が存在すると考えられる。この対応関係をスコーレム関数として新たに置き換えたものがスコーレム標準形といえる。

全称限量子がない場合
A = ∃xP(x,y)
B = P(b,y)
アリティ0のスコーレム関数記号b（定数）を導入する。

スコーレム標準形に変換することをスコーレム化という。

まとめ：変換手順

論理式の多重集合Γに対して

1. P-NF（冠頭標準形への変換）を施す
2. C-NF（連言標準形への変換）を施す
3. S-NF（スコーレム標準形への変換）を施す

結果、意味的同値ではないが充足可能性が同値な関数ができる。

エルブラン定理

（省略）