スコーレム標準形
∃ を消し去る
開発者向け解説
コンピュータは ∀ と ∃ が混在した式を直接扱うのが苦手です。そこで「式の矛盾性を保ったまま ∃ を完全に消す」魔法のテクニックを使います。これがスコーレム化です。
ルール：∃x の前に ∀ がなければ、x を「特定の名前（定数 a など）」に置き換えます。 前に ∀y があれば、x は y に依存して変わるため、 「関数 f(y)（スコーレム関数）」に置き換えます。
定理 4.1 により、この強引な変形でも「矛盾するかどうか」という性質は完全に保たれます。 ただし元の式と同値になるわけではない点に注意。 下のパズルでは、赤くなった ∃ をクリックして、定数か関数に置き換えてみてください。
Theorem 4.1
論理式 のスコーレム標準形を とする。 このとき
つまり、扱いにくい量化子混じりの式 を、 コンピュータが扱いやすい に置き換えて 「矛盾しているか」を調べてよい — というお墨付き。反駁手続きの根拠そのもの。
証明（∃ を 1 つ消す場合の双方向 ⇒ 数学的帰納法）
- は充足不可能だが、スコーレム化後の は 充足可能である、と仮定する。すると を真にする解釈 が存在する。
数学的帰納法へ： 上の双方向は「∃ を 1 つだけ消す」場合の補題。式 の中の存在量化子を 左から順に と消していけば、 各ステップで充足不可能性は不変。よって が結論される。 ∎
同値性ではない（保たれるのは充足不可能性だけ）
と は 論理的に等価ではない：。 同じモデル上で真理値がズレる例がある。
領域 D = {1, 2}, P(2) のみ真
真（x=2 が証拠）
スコーレム定数 a が a := 1 と解釈された場合
偽（P(1) が偽）
しかし「どんな解釈でも偽である（充足不可能）」という性質に絞れば、 と は完全に一致する。反駁は 充足不可能性だけ を見るので、これで十分。
プリセット式
いまの式（赤い ∃ をクリック）
P(x)
ステップ履歴
- Step 0もとの式
∃x P(x)