ハーブブランド化

論理式のヘルブラン化（ジャック・ヘルブランにちなんで名付けられた）は、論理式の スコレム化と双対となる構成法である。トーラルフ・スコレムは、レーヴェンハイム＝スコレムの定理の証明の一部として、プレネックス形式の論理式のスコレム化を検討していた（スコレム 1920）。ヘルブラントは、ヘルブラントの定理を証明するために、このヘルブラン化の双対概念を、プレネックス形式以外の論理式にも適用できるように一般化して用いた（ヘルブラント 1930）。

結果として得られる式は、必ずしも元の式と等価であるとは限りません。充足可能性のみを保持するスコレム化と同様に、スコレム化の双対であるヘルブラン化は妥当性を保持します。つまり、結果として得られる式は、元の式が妥当である場合に限り妥当です。

させて${\displaystyle F}$一階述語論理の言語における式であると仮定します。${\displaystyle F}$2 つの異なる量化子の出現によって束縛される変数はなく、束縛と自由の両方で出現する変数もありません。（つまり、${\displaystyle F}$これらの条件を満たすように文字を書き換えることが可能であり、その結果として同等の式が得られる。

ハーブブランド化${\displaystyle F}$は次のようにして得られます。

• まず、自由変数を置き換えます。${\displaystyle F}$定数記号によって。
• 次に、(1) 偶数個の否定記号の範囲内で全称量化されている変数、または (2) 奇数個の否定記号の範囲内で存在量化されている変数のすべての量化子を削除します。
• 最後に、そのような変数をそれぞれ置き換えます。${\displaystyle v}$関数記号付き${\displaystyle f_{v}(x_{1},\dots ,x_{k})}$、 どこ${\displaystyle x_{1},\dots ,x_{k}}$は依然として定量化されている変数であり、その定量化子は${\displaystyle v}$。

例えば、次の式を考えてみましょう。${\displaystyle F:=\forall y\exists x[R(y,x)\wedge \neg \exists zS(x,z)]}$置き換える自由変数はありません。${\displaystyle y,z}$これらは第2段階で検討する種類のものであるため、量化子を削除します。$\displaystyle \forall y}$そして${\displaystyle \exists z}$最後に、${\displaystyle y}$一定の${\displaystyle c_{y}}$（他に量化子がなかったため）${\displaystyle y}$)、そして私たちは${\displaystyle z}$関数記号付き${\displaystyle f_{z}(x)}$:

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

式のスコレム化も同様に得られますが、上記の2番目のステップでは、(1)存在量化されており、かつ偶数個の否定の範囲内にある変数、または(2)全称量化されており、かつ奇数個の否定の範囲内にある変数の量化子を削除します。したがって、同じ式を考慮すると、${\displaystyle F}$上から見ると、そのスコレム化は次のようになる。

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

これらの構成の意義を理解するには、ヘルブラントの定理またはレーヴェンハイム・スコレムの定理を参照してください。

• 述語関数論理