エルブラン化

${\displaystyle F}$ を一階述語論理の言語で書かれた論理式とする。ここで ${\displaystyle F}$ は異なる量化記号の出現において束縛されるような変数は持たず、いかなる変数も束縛変数と自由変数の両方として出現することはないと仮定してよい。（つまり、${\displaystyle }$ は、結果として同値な論理式が得られるように文字を付け替えることで、これらの条件を保証することができる。）

このとき ${\displaystyle F}$ のスコーレム化は次のようにして得られる：

• 第一に、${\displaystyle F}$ の全ての変数を定数記号に置き換える。
• 第二に、次のいずれかの変数上の量化子を全て削除する： (1) 全称量化されておりかつ、偶数個の否定記号の内側にある (2) 存在量化されており、かつ奇数個の否定記号の内側にある。
• 最後に、それらの変数 ${\displaystyle v}$ を関数記号 ${\displaystyle f_{v}(x_{1},\ldots ,x_{k})}$ に置き換える。ここで ${\displaystyle x_{1},\ldots ,x_{k}}$ は依然として量化されたままの変数であって、それら量化記号は ${\displaystyle v}$ を支配している。

例として、論理式 ${\displaystyle F:=\forall y\exists x[R(y,x)\wedge \neg \exists zS(x,z)]}$ を考えよう。（最初のステップで）置換される自由変数は存在しない。変数 ${\displaystyle y,z}$ は第二ステップで考慮される種類の変数であるから、量化子 ${\displaystyle \forall y}$ と ${\displaystyle \exists z}$ を削除する。最後に、${\displaystyle y}$ を定数記号 ${\displaystyle c_{y}}$ に置き換え（${\displaystyle y}$ を支配する量化子は存在しなかったのだから）、${\displaystyle z}$ を関数記号 ${\displaystyle f_{z}(x)}$ に置き換える：

${\displaystyle F^{H}=\exists x[R(c_{y},x)\wedge \neg S(x,f_{z}(x))].}$

論理式のスコーレム化も、上記の第二ステップを例外とすれば、同様に得られる。第二ステップでは、次のいずれかの変数上の量化子を全て削除する： (1) 存在量化されておりかつ、偶数個の否定記号の内側にある (2) 全称量化されており、かつ奇数個の否定記号の内側にある。よって、上と同じ ${\displaystyle F}$ を考えれば、そのスコーレム化は

${\displaystyle F^{S}=\forall y[R(y,f_{x}(y))\wedge \neg \exists zS(f_{x}(y),z)].}$

これらの構成の意義を理解するためには、エルブランの定理またはレーヴェンハイム–スコーレムの定理を参照。

• 述語関手論理

• Skolem, T. "Logico-combinatorial investigations in the satisfiability or provability of mathematical propositions: A simplified proof of a theorem by L. Löwenheim and generalizations of the theorem". (In van Heijenoort 1967, 252-63.)
• Herbrand, J. "Investigations in proof theory: The properties of true propositions". (In van Heijenoort 1967, 525-81.)
• van Heijenoort, J. From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Harvard University Press, 1967.