エルブラン化のソースを表示

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

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

==定義と例==
<math>F</math> を[[一階述語論理]]の言語で書かれた論理式とする。ここで <math>F</math> は異なる量化記号の出現において束縛されるような変数は持たず<!-- 訳注：異なる量化記号の出現が束縛する変数記号は互いに異なる-->、いかなる変数も束縛変数と自由変数の両方として出現することはない<!--訳注：ひとつの変数記号が自由変数と束縛変数の両方として使われることはない-->と仮定してよい。（つまり、<math></math> は、結果として同値な論理式が得られるように文字を付け替えることで、これらの条件を保証することができる。）

このとき <math>F</math> の'''スコーレム化'''は次のようにして得られる：

* 第一に、<math>F</math> の全ての変数を定数記号に置き換える。
* 第二に、次のいずれかの変数上の量化子を全て削除する： (1) 全称量化されておりかつ、偶数個の否定記号の内側にある (2) 存在量化されており、かつ奇数個の否定記号の内側にある。
* 最後に、それらの変数 <math>v</math> を関数記号 <math>f_v(x_1, \ldots, x_k)</math> に置き換える。ここで <math>x_1,\ldots,x_k</math> は依然として量化されたままの変数であって、それら量化記号は <math>v</math> を支配している。<!--訳注：つまり量化のスコープに <math>v</math> を含んでいる。-->

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

: <math> F^H = \exists x [R(c_y,x) \wedge \neg S(x,f_z(x))]. </math>

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

: <math> F^S = \forall y [R(y,f_x(y)) \wedge \neg\exists z S(f_x(y),z)]. </math>

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

== 関連項目 ==
* [[述語関手論理]]

==参照文献==

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

{{デフォルトソート:えるふらん}}
[[Category:論理学]]
[[Category:数学のエポニム]]
[[Category:数学に関する記事]]