エルブラン化
論理式のエルブラン化(英: Herbrandization)とは、論理式のスコーレム化の双対となる構成である。ジャック・エルブランに因む。トアルフ・スコーレムは、レーヴェンハイム–スコーレムの定理(Skolem 1920)の証明の一部として、冠頭標準形の論理式のスコーレム化を考えていた。エルブランは、エルブランの定理(Herbrand 1930)を証明するため、その双対概念であるエルブラン化(冠頭標準形以外の論理式にも適用できるよう一般化されたもの)を用いた。
結果の論理式は元々の論理式と論理的同値である必要はない。充足可能性を保つスコーレム化と同様、スコーレム化の双対であるエルブラン化は論理的妥当性を保つ:結果の論理式が妥当であるのは、元々の論理式が妥当であるとき、かつそのときに限る。
F H = ∃ x [ R ( c y , x ) ∧ ¬ S ( x , f z ( x ) ) ] . {\displaystyle F^{H}=\exists x[R(c_{y},x)\wedge \neg S(x,f_{z}(x))].}
論理式のスコーレム化も、上記の第二ステップを例外とすれば、同様に得られる。第二ステップでは、次のいずれかの変数上の量化子を全て削除する: (1) 存在量化されておりかつ、偶数個の否定記号の内側にある (2) 全称量化されており、かつ奇数個の否定記号の内側にある。よって、上と同じ F {\displaystyle F} を考えれば、そのスコーレム化は
F S = ∀ y [ R ( y , f x ( y ) ) ∧ ¬ ∃ z S ( f x ( y ) , z ) ] . {\displaystyle F^{S}=\forall y[R(y,f_{x}(y))\wedge \neg \exists zS(f_{x}(y),z)].}
これらの構成の意義を理解するためには、エルブランの定理またはレーヴェンハイム–スコーレムの定理を参照。