スコーレム標準形（スコーレムひょうじゅんけい、）とは、数理論理学において一階述語論理における存在記号がすべて全称記号の前にある冠頭標準形の論理式を言う。トアルフ・スコーレムによるスコーレムの定理により、第一階述語論理における任意の論理式に対して、演繹的に等価（deductive equivalence）なスコーレム標準形の論理式が存在する。第一階述語論理における任意の論理式は、論理式の一番前にすべて否定形でない前置記号を持ち、その作用域がどれも論理式の終わりまで及ぶような標準形に直すことができる。このような標準形を冠頭標準形（prenex normal form）と呼ぶ。なお、冠頭標準形の一番前から数えて存在記号の前にある全称記号の数を、その冠頭標準形の次数（degree）と呼ぶ。スコーレム化は、存在量化された変項 formula_1 を新規の項 formula_2（シンボル formula_3 は元の論理式には出現していない）に全て置き換えることでなされる。この項の各変項は、次のようなものである。もしその論理式が冠頭標準形なら、formula_4 の各変項は全称量化されていて、その量化子は formula_1 の量化子より前に置かれている。一般に、論理式には全称量化が行われていて、formula_6 はその量化子のスコープ内にあると考えられる。ここで導入される関数 formula_3 をスコーレム関数（Skolem function、アリティがゼロならスコーレム定項）と呼び、項全体をスコーレム項（Skolem term）と呼ぶ。例として、論理式 formula_8 を考える。これには存在量化子 formula_6 があるので、スコーレム標準形ではない。スコーレム化では formula_1 を formula_11 で置き換える。このとき、formula_3 は新たな関数シンボルであり、置換と同時に formula_1 の量化子を除去する。結果として得られる論理式は formula_14 となる。スコーレム項 formula_11 は formula_16 は含むが formula_17 は含まない。これは除去された量化子 formula_6 が formula_19 のスコープには入っているが、formula_20 のスコープには入っていないためである。この論理式は冠頭標準形なので、量化子のリストにおいて formula_16 は formula_1 の前にあるが formula_17 はそうではない、と言うこともできる。この変換で得られた論理式は、元の論理式が充足される場合のみ充足される。スコーレム化は、一階述語論理での充足可能性の定義に二階述語論理の等価性を適用するものである。その等価性によれば、存在量化子は全称量化子の前に移動できる。ここで直観的に、「全ての x について、ある y が存在し、R(x,y) が成り立つ」とは、「ある関数 f が全ての x を y にマッピングし、全ての x について R(x,f(x)) が成り立つ」と書き換えても等価である。一階述語論理の充足可能性は、関数シンボルの評価に対して暗黙のうちに存在量化を施すような定義になっているため、この等価性が役立つ。ここで、一階述語論理式 formula_26 は、モデル formula_27 が存在し、その論理式を「真」であると評価させるような自由変項の評価の組合せ formula_28 があるとき、充足可能である。このモデルには、全関数シンボルの評価も含まれるので、スコーレム関数も暗黙のうちに存在量化される。上記の例 formula_29 は、formula_29 が真となるような自由変項（この例では自由変項はない）の評価と formula_3 の評価を含むモデル formula_27 が存在するときのみ充足可能であると言える。これを二階述語論理で表すと formula_33 となる。上記の等価性により、これは formula_34 の充足可能性と同じである。メタレベルとしては、論理式 formula_26 の一階述語論理としての充足可能性は formula_36 と表され、ここで formula_27 がモデル、formula_28 が自由変項群の評価である。一階述語モデルは全関数シンボルの評価を含むので、任意のスコーレム関数 formula_26 は formula_40 によって暗黙のうちに存在量化される。結果として、ある変項への存在量化子を論理式の最初での関数群への存在量化子に置換し、それら存在量化子を除去することで、論理式を一階述語論理式のまま扱うことができる。この最後の段階での formula_33 を formula_29 として扱うことは、関数が formula_40 によって暗黙に存在量化されるという一階述語の充足可能性の定義によるものである。スコーレム化の正しさを示す例として、論理式 formula_44 を考える。この論理式がモデル formula_27 で充足されるのは、そのモデルのドメインにおいて formula_46 がとりうる全ての値について、同じモデルのドメインにおいて formula_1 の値が存在し、それらの値を適用して評価したとき formula_48 が真になる場合のみである。選択公理により、formula_49 となる関数 formula_3 が存在する。結果として、formula_27 に formula_3 の評価を加えたモデルを使えば、論理式 formula_53 は充足可能である。従って formula_54 が充足可能であるときのみ formula_55 も充足可能であると言える。これとは別に、formula_54 が充足可能であるなら、それを充足させるモデル formula_57 が存在し、関数 formula_3 の評価が含まれ、全ての formula_46 の値の組合せについて論理式 formula_60 が成り立つ。結果として、formula_57 における formula_3 の評価を使って、全ての formula_4 の値の組合せについて formula_64 となるような値を選択できるため、formula_55 も同じモデルで充足可能となる。

出典:wikipedia