スコーレム標準形のソースを表示

'''スコーレム標準形'''（スコーレムひょうじゅんけい、{{lang-en-short|Skolem normal form}}）とは、[[数理論理学]]において[[一階述語論理]]における[[存在記号]]がすべて[[全称記号]]の前にある[[冠頭標準形]]の[[論理式 (数学)|論理式]]を言う。

[[トアルフ・スコーレム]]によるスコーレムの定理により、第一階述語論理における任意の論理式に対して、演繹的に等価（deductive equivalence）<ref>スコーレム化（Skolemization）によって得られる標準形の論理式は元の論理式と等価とは限らないが、その充足可能性は同値である。</ref>なスコーレム標準形の論理式が存在する<ref>[[#HA(1960)|ヒルベルト、アッケルマン(1954)]] p.95</ref>。

== 定義 ==
=== 冠頭標準形（prenex normal form） ===
{{main|冠頭標準形}}
第一階述語論理における任意の論理式は、論理式の一番前にすべて否定形でない前置記号を持ち、その作用域がどれも論理式の終わりまで及ぶような標準形に直すことができる。

このような標準形を'''冠頭標準形'''（prenex normal form）と呼ぶ<ref>この冠頭標準形の利点は、前置記号の後の論理式を命題論理における複合命題と同等に扱うことができるところにある。また考慮すべき論理式の範囲を著しく限定することができるため、論理式の一般的な性質を明らかにするにあたって都合が良い。[[#HA(1960)|ヒルベルト、アッケルマン]] pp.93-94</ref>。なお、冠頭標準形の一番前から数えて存在記号の前にある全称記号の数を、その冠頭標準形の'''次数'''（degree）と呼ぶ。

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

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

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

:<math>\forall x \Big( g(x) \vee \exists y  R(x,y) \Big) \iff \forall x \Big( g(x) \vee R(x,f(x)) \Big)</math>
ここで
:<math>f(x)</math> は y を x でマッピングする関数である。

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

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

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

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

== 脚注 ==
{{reflist}}

== 関連項目 ==
* [[述語論理]]
* [[一階述語論理]]

== 参考文献 ==
* {{cite book | 和書 | author=D.ヒルベルト、W.アッケルマン | editor=伊藤誠（訳） | title=記号論理学の基礎（第3版） | year=1960 | publisher=大阪教育図書社 | ref=HA(1960) | id={{NDLDC|2967702|format=NDLJP}} }}

== 外部リンク ==
* [https://planetmath.org/Skolemization Skolemization on PlanetMath.org]

{{logic}}

{{DEFAULTSORT:すこれむひようしゆんけい}}
[[Category:標準形 (論理)]]
[[Category:トアルフ・スコーレム]]
[[Category:数学に関する記事]]
[[Category:数学のエポニム]]