スコーレム標準形

スコーレム標準形（英: Skolem normal form）とは、冠頭標準形に全称量化子しか含まれない一階述語論理の論理式の形式である。名称の由来はトアルフ・スコーレム。全ての一階述語論理の論理式はスコーレム標準形に変換でき、そのスコーレム化（Skolemization）に際して充足可能性は変化しない。スコーレム化によって得られる式は元の式と等価とは限らないが、元の式が充足されるときのみ充足される。

概要 [編集]

スコーレム化は、存在量化された変項 $y$ を新規の項 $f(x_1,\ldots,x_n)$ （シンボル $f$ は元の論理式には出現していない）に全て置き換えることでなされる。この項の各変項は、次のようなものである。もしその論理式が冠頭標準形なら、 $x_1,\ldots,x_n$ の各変項は全称量化されていて、その量化子は $y$ の量化子より前に置かれている。一般に、論理式には全称量化が行われていて、 $\exists y$ はその量化子のスコープ内にあると考えられる。ここで導入される関数 $f$ をスコーレム関数（Skolem function、アリティがゼロならスコーレム定項）と呼び、項全体をスコーレム項（Skolem term）と呼ぶ。

例として、論理式 $\forall x \exists y \forall z. P(x,y,z)$ を考える。これには存在量化子 $\exists y$ があるので、スコーレム標準形ではない。スコーレム化では $y$ を $f(x)$ で置き換える。このとき、 $f$ は新たな関数シンボルであり、置換と同時に $y$ の量化子を除去する。結果として得られる論理式は $\forall x \forall z . P(x,f(x),z)$ となる。スコーレム項 $f(x)$ は $x$ は含むが $z$ は含まない。これは除去された量化子 $\exists y$ が $\forall x$ のスコープには入っているが、 $\forall z$ のスコープには入っていないためである。この論理式は冠頭標準形なので、量化子のリストにおいて $x$ は $y$ の前にあるが $z$ はそうではない、と言うこともできる。この変換で得られた論理式は、元の論理式が充足される場合のみ充足される。

スコーレム化 [編集]

スコーレム化は、一階述語論理での充足可能性の定義に二階述語論理の等価性を適用するものである。その等価性によれば、存在量化子は全称量化子の前に移動できる。

$\forall x \Big( g(x) \vee \exists y R(x,y) \Big) \iff \forall x \Big( g(x) \vee R(x,f(x)) \Big)$

ここで

$f(x)$ は y を x でマッピングする関数である。

直観的に、「全ての x について、ある y が存在し、R(x,y) が成り立つ」とは、「ある関数 f が全ての x を y にマッピングし、全ての x について R(x,f(x)) が成り立つ」と書き換えても等価である。

一階述語論理の充足可能性は、関数シンボルの評価に対して暗黙のうちに存在量化を施すような定義になっているため、この等価性が役立つ。ここで、一階述語論理式 $\Phi$ は、モデル $M$ が存在し、その論理式を「真」であると評価させるような自由変項の評価の組合せ $\mu$ があるとき、充足可能である。このモデルには、全関数シンボルの評価も含まれるので、スコーレム関数も暗黙のうちに存在量化される。上記の例 $\forall x . R(x,f(x))$ は、 $\forall x . R(x,f(x))$ が真となるような自由変項（この例では自由変項はない）の評価と $f$ の評価を含むモデル $M$ が存在するときのみ充足可能であると言える。これを二階述語論理で表すと $\exists f \forall x . R(x,f(x))$ となる。上記の等価性により、これは $\forall x \exists y . R(x,y)$ の充足可能性と同じである。

メタレベルとしては、論理式 $\Phi$ の一階述語論理としての充足可能性は $\exists M \exists \mu ~.~ ( M,\mu \models \Phi)$ と表され、ここで $M$ がモデル、 $\mu$ が自由変項群の評価である。一階述語モデルは全関数シンボルの評価を含むので、任意のスコーレム関数 $\Phi$ は $\exists M$ によって暗黙のうちに存在量化される。結果として、ある変項への存在量化子を論理式の最初での関数群への存在量化子に置換し、それら存在量化子を除去することで、論理式を一階述語論理式のまま扱うことができる。この最後の段階での $\exists f \forall x . R(x,f(x))$ を $\forall x . R(x,f(x))$ として扱うことは、関数が $\exists M$ によって暗黙に存在量化されるという一階述語の充足可能性の定義によるものである。

スコーレム化の正しさを示す例として、論理式 $F_1 = \forall x_1 \dots \forall x_n \exists y R(x_1,\dots,x_n,y)$ を考える。この論理式がモデル $M$ で充足されるのは、そのモデルのドメインにおいて $x_1,\dots,x_n$ がとりうる全ての値について、同じモデルのドメインにおいて $y$ の値が存在し、それらの値を適用して評価したとき $R(x_1,\dots,x_n,y)$ が真になる場合のみである。選択公理により、 $y = f(x_1,\dots,x_n)$ となる関数 $f$ が存在する。結果として、 $M$ に $f$ の評価を加えたモデルを使えば、論理式 $F_2 = \forall x_1 \dots \forall x_n R(x_1,\dots,x_n,f(x_1,\dots,x_n))$ は充足可能である。従って $F_2$ が充足可能であるときのみ $F_1$ も充足可能であると言える。これとは別に、 $F_2$ が充足可能であるなら、それを充足させるモデル $M'$ が存在し、関数 $f$ の評価が含まれ、全ての $x_1,\dots,x_n$ の値の組合せについて論理式 $R(x_1,\dots,x_n,f(x_1,\dots,x_n))$ が成り立つ。結果として、 $M'$ における $f$ の評価を使って、全ての $x_1,\ldots,x_n$ の値の組合せについて $y=f(x_1,\dots,x_n)$ となるような値を選択できるため、 $F_1$ も同じモデルで充足可能となる。