スコーレム標準形
スコーレム化は、一階述語論理での充足可能性の定義に二階述語論理の等価性を適用するものである。その等価性によれば、存在量化子は全称量化子の前に移動できる。
∀ x ( g ( x ) ∨ ∃ y R ( x , y ) ) ⟺ ∀ x ( g ( x ) ∨ R ( x , f ( x ) ) ) {\displaystyle \forall x{\Big (}g(x)\vee \exists yR(x,y){\Big )}\iff \forall x{\Big (}g(x)\vee R(x,f(x)){\Big )}}
ここで
f ( x ) {\displaystyle f(x)} は y を x でマッピングする関数である。
直観的に、「全ての x について、ある y が存在し、R(x,y) が成り立つ」とは、「ある関数 f が全ての x を y にマッピングし、全ての x について R(x,f(x)) が成り立つ」と書き換えても等価である。
一階述語論理の充足可能性は、関数シンボルの評価に対して暗黙のうちに存在量化を施すような定義になっているため、この等価性が役立つ。ここで、一階述語論理式 Φ {\displaystyle \Phi } は、モデル M {\displaystyle M} が存在し、その論理式を「真」であると評価させるような自由変項の評価の組合せ μ {\displaystyle \mu } があるとき、充足可能である。
従って F 2 {\displaystyle F_{2}} が充足可能であるときのみ F 1 {\displaystyle F_{1}} も充足可能であると言える。これとは別に、 F 2 {\displaystyle F_{2}} が充足可能であるなら、それを充足させるモデル M ′ {\displaystyle M'} が存在し、関数 f {\displaystyle f} の評価が含まれ、全ての x 1 , ... , x n {\displaystyle x_{1},\dots ,x_{n}} の値の組合せについて論理式 R ( x 1 , ... , x n , f ( x 1 , ... , x n ) ) {\displaystyle R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))} が成り立つ。結果として、 M ′ {\displaystyle M'} における f {\displaystyle f} の評価を使って、全ての x 1 , ... , x n {\displaystyle x_{1},\ldots ,x_{n}} の値の組合せについて y = f ( x 1 , ... , x n ) {\displaystyle y=f(x_{1},\dots ,x_{n})} となるような値を選択できるため、 F 1 {\displaystyle F_{1}} も同じモデルで充足可能となる。