エルブラン化

論理式のエルブラン化（英: Herbrandization）とは、論理式のスコーレム化の双対となる構成である。ジャック・エルブランに因む。トアルフ・スコーレムは、レーヴェンハイム–スコーレムの定理（Skolem 1920）の証明の一部として、冠頭標準形の論理式のスコーレム化を考えていた。エルブランは、エルブランの定理（Herbrand 1930）を証明するため、その双対概念であるエルブラン化（冠頭標準形以外の論理式にも適用できるよう一般化されたもの）を用いた。

結果の論理式は元々の論理式と論理的同値である必要はない。充足可能性を保つスコーレム化と同様、スコーレム化の双対であるエルブラン化は論理的妥当性を保つ：結果の論理式が妥当であるのは、元々の論理式が妥当であるとき、かつそのときに限る。

定義と例

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

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

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

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

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

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

$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.