エルブランの定理

エルブランの定理︵英: Herbrand's theorem︶は1930年にジャック・エルブランが発表した数理論理学上の基本定理である 。 エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。

$F$$F$ を節の有限集合とするとき、以下の2つは同値である。
●$F$$F$ が充足不能

●$F$$F$ から得られる基礎例︵エルブラン基底︶の有限集合で充足不能なものが存在

エルブランの定理は一階述語論理における任意の恒真な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの自動定理証明の理論的な基盤になっている。チューリングマシンの停止性問題と同様、一般的な述語論理式が証明可能かどうかを求めるアルゴリズムは存在しないが、エルブランの定理では一階述語論理を命題論理と結び付けることで、一階述語論理での証明可能性についての部分的な回答を与えている。

なお、エルブランの本来の証明は任意の一階述語論理式を対象としたものだが、多くの場合、冠頭形の論理式に制限し単純化した定理で表される。

エルブラン領域

エルブラン領域︵英: Herbrand universe︶とは、述語論理式に現れうる変数を含まない全ての項の集合である。

述語論理式の項は以下の定義から帰納的に表される。

●任意の個体定項︵定数︶は項である。

●任意の個体変項︵変数︶は項である。

●任意のn引数の関数記号 fと複数の項からなる f(t₁, .. ,t_n) は項である。

論理式を構成する記号として定数及び関数記号が定められているとき、変数を含まない項︵閉項、closed term︶の全体をエルブラン領域︵Herbrand universe︶といい、以下の式 Hで表すことができる。論理式に定数が含まれない場合は任意の定数cを付加する。

$H=\textstyle H_{\infty }$$H=\textstyle H_{\infty }$
●$H_{0}={\big \{}c{\big \}}$$H_{0}={\big \{}c{\big \}}$ ︵cは定数記号︶

●$H_{i+1}=H_{i}\cup {\big \{}f(t_{1},\ldots ,t_{n})|t_{j}\in H_{i}{\big \}}$$H_{i+1}=H_{i}\cup {\big \{}f(t_{1},\ldots ,t_{n})|t_{j}\in H_{i}{\big \}}$ ︵f はn引数の関数記号︶

例えば、定数 aと1引数関数 f及び2引数関数 gが論理式に含まれる場合のエルブラン領域は、a, f(a), f(f(a)), g(a,a), g(a,f(a)), f(g(a,a)), g(a,g(a,a)), ‥ となる。

エルブラン基底とエルブラン解釈

エルブラン領域の全ての要素を論理式を構成する原子論理式に割り当て、それぞれの真偽値を決めることで、論理式に対する任意の解釈が表現できる。

エルブラン領域の要素を引数とする原子論理式の全体をエルブラン基底︵英: Herbrand basis︶という。

例えば、x, y, zを変数とする述語 P(x) と Q(g(a,y),f(z)) からなる論理式のエルブラン基底は、P(a), P(f(a)), P(f(f(a))), P(g(a,a)), P(g(a,f(a))), ‥ ,Q(g(a,a),f(a)), ‥ となる。

一般に変数をもたない述語または節のことを基礎例(ground instance) と言う。エルブラン基底は節集合から得られる基礎例である。 エルブラン基底を導入することで、論理式を命題論理式として扱うことができ、論理式の意味を構文的に決めることができる。

エルブラン基底の任意の部分集合 Iをエルブラン解釈︵英: Herbrand interpretation︶と呼ぶ。直感的には、エルブラン基底の要素の内 Iに含まれるものは真、それ以外は偽を表し、真偽値の割り当てにより論理式全体に対する1つの解釈を定めたことになる。

エルブランの定理

エルブランの定理は、以下のように表現できる。


$F$$F$ を節の有限集合とするとき、以下の2つは同値である。
●$F$$F$ が充足不能

●$F$$F$ から得られる基礎例︵エルブラン基底︶の有限集合で充足不能なものが存在


つまり、一階述語論理式の充足不能性の判定は、エルブラン基底上の有限回の命題論理レベルでの判定で行うことができる。

エルブランの定理はこれ以外にも様々な形式で表現することができる。

一般に、論理式の真偽値は対象となる領域 Dとその解釈 Iの組︵モデル︶により異なる。例えば、${\displaystyle \forall x\exists y(x>$y)} $\forall x\exists y(x>y)$ は、自然数を領域とするか実数を領域とするかで真偽値が変わる。モデルにより以下の3通りが考えられる。

●恒真︵valid︶・・・全てのモデルで真

●充足可能︵satisfiable︶・・・少なくとも1つのモデルで真

●充足不能︵unsatisfiable︶・・どんなモデルでも偽︵=恒偽︶

以下では、例として $\forall x\forall yP(x,y)$$\forall x\forall yP(x,y)$のような全称論理式(あるいは論理式の集合) $F$$F$を考える。$P$$P$ は述語、 $a_{1},a_{2},...,a_{n},...$$a_{1},a_{2},...,a_{n},...$は変数の集まりを表す。以下の3つの特性について考える。

(一)$F$$F$ は無矛盾︵consistent︶、つまり $F$$F$を仮定した場合に矛盾︵$F\land \lnot F$$F\land \lnot F$︶を導きだせないこと。これは $\lnot F$$\lnot F$が自然演繹のような述語論理の演繹システムで導きだせないことで、次のように表記する‥$\not \vdash \lnot F$$\not \vdash \lnot F$.

(二)$F$$F$ は充足可能︵satisfiable︶、つまり $F$$F$が真となるようなモデルが存在すること。これは次のように表記できる‥$\not \vDash \lnot F$$\not \vDash \lnot F$.

(三)全ての $n$$n$に対し、以下 $Q(a_{1},...,a_{n})$$Q(a_{1},...,a_{n})$と表現する以下の論理式を真にするようなモデルが存在すること。これは次のように表記できる‥全ての $n$$n$に対して$\not \vDash \lnot Q(a_{1},...,a_{n})$$\not \vDash \lnot Q(a_{1},...,a_{n})$
$P(a_{1},a_{1})\land P(a_{1},a_{2})\land P(a_{2},a_{1})\land P(a_{2},a_{2})\land \cdots \land P(a_{1},a_{n})\land \cdots \land P(a_{n-1},a_{n})\land P(a_{n},a_{1})\land \cdots \land P(a_{n},a_{n})$$P(a_{1},a_{1})\land P(a_{1},a_{2})\land P(a_{2},a_{1})\land P(a_{2},a_{2})\land \cdots \land P(a_{1},a_{n})\land \cdots \land P(a_{n-1},a_{n})\land P(a_{n},a_{1})\land \cdots \land P(a_{n},a_{n})$
ゲーデルの完全性定理は上の(1)と(2)が同値であると主張している。さらに(2)は(3)を含み、(3)で真となるモデルは(2)のモデルとなる。エルブランの定理は逆に、エルブラン領域という特定の領域で(3)が(2)を含んでいるということを主張する。つまり、エルブラン領域という特定の領域で考えると、上の(2)と(3)はエルブランの定理の別の表現であり、(1)、(2)、(3)は同値である。なお、エルブラン領域では変数が無くなるため(3)での全称記号が消え、解くべき論理式は命題論理の命題として扱うことができる。

G = ¬F、R = ¬Q、S = ¬P と置いて双対を考えると、上と等価な3つの特性を得ることができる。

(一)$G$$G$ は証明可能︵provable︶、つまり命題論理の演繹システムで $G$$G$を導くことができること。これは次のように表記する‥$\vdash G$$\vdash G$
(二)$G$$G$ は恒真︵valid︶、つまり $G$$G$は全てのモデルで真になる。これは次のように表記する‥$\vDash G$$\vDash G$.

(三)ある$n$$n$ に対し、以下の $R(a_{1},...,a_{n})$$R(a_{1},...,a_{n})$が恒真になるような $n$$n$が存在すること。これは次のように表記する‥$\vDash R(a_{1},...,a_{n})$$\vDash R(a_{1},...,a_{n})$
$S(t_{1},t_{1})\lor S(t_{1},t_{2})\lor S(t_{2},t_{1})\lor \cdots \lor S(t_{1},t_{n})\lor \cdots \lor S(t_{n-1},t_{n})\lor S(t_{n},t_{1})\lor \cdots \lor S(t_{n},t_{n})$$S(t_{1},t_{1})\lor S(t_{1},t_{2})\lor S(t_{2},t_{1})\lor \cdots \lor S(t_{1},t_{n})\lor \cdots \lor S(t_{n-1},t_{n})\lor S(t_{n},t_{1})\lor \cdots \lor S(t_{n},t_{n})$
︵ $t_{1},t_{2},...,t_{n}$$t_{1},t_{2},...,t_{n}$は変数 $a_{1},a_{2},...,a_{n}$$a_{1},a_{2},...,a_{n}$をエルブラン領域の要素で置き換えたもの︶

前と同様、上の(2)と(3)はエルブランの定理の別の表現であり、(1)、(2)、(3)は同値である。

ここで、F が充足不能のとき︵すなわち G= ¬F が恒真のとき︶を考える。$Q(a_{1},...,a_{n})$$Q(a_{1},...,a_{n})$ を$n=1$$n=1$、$n=2$$n=2$ と調べていくと、$Q(a_{1},...,a_{n})$$Q(a_{1},...,a_{n})$ が偽となるような nが存在する︵そうでなければ全ての nで真となるため充足可能となってしまう︶。またその逆も成り立つ。 これを利用し、任意の恒真な論理式 Gの証明を行いたい場合、論理式の否定 ¬G の充足不能性を調べることで、エルブラン解釈の下での有限回の操作で調べることができる。これはエルブランの定理の重要な成果である。

それとは反対に、F が充足可能のとき、全ての nに対し $Q(a_{1},...,a_{n})$$Q(a_{1},...,a_{n})$が真となり、変数 $a_{i}$$a_{i}$が有限でない場合は計算が終わらない。これは、一般に述語計算が決定可能でないことを示している。

より形式的には、エルブランの定理は上の(2)、(3)について、論理式 $S(x,y)$$S(x,y)$をより一般化した形で表現される。また対象となる論理式は冠頭標準形の式である。以下に形式化されたエルブランの定理の例を示す。


$(\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})$$(\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})$ を一階述語論理式とする。ここで $F(y_{1},\ldots ,y_{n})$$F(y_{1},\ldots ,y_{n})$は量化子を1つも含まない論理式である。
このとき $(\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})$$(\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})$が恒真になる必要十分条件は、ある自然数 $k$$k$とエルブラン領域の項 $t_{i1},\ldots ,t_{in}$$t_{i1},\ldots ,t_{in}$︵$1\leq i\leq k$$1\leq i\leq k$︶が存在し、

$F(t_{11},\ldots ,t_{1n})\vee \ldots \vee F(t_{k1},\ldots ,t_{kn})$$F(t_{11},\ldots ,t_{1n})\vee \ldots \vee F(t_{k1},\ldots ,t_{kn})$
が恒真になることである。


このようなエルブランの定理の証明は、ゲーデルの完全性定理により恒真性が証明可能性に置き換えられることを利用し、ゲンツェンのカット除去定理を用い $\vdash (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})$$\vdash (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})$のカット規則を除去した証明を求めるものが一般的である。

エルブランが定理を証明した時にゲンツェンのカット除去定理はまだ知られておらず、ゲーデルの完全性定理も発表されていなかった。そのためエルブランによる証明はエルブラン版のカット除去定理や独自の完全性定理を含むもので、任意の一階述語論理式を対象としていた。

応用

エルブランの定理は自動定理証明の理論的基盤となった。

さらにエルブランの定理を計算機上で直接応用する試みが行われ、ギルモアのアルゴリズム(1960)やデービス・パトナムのアルゴリズム(1958,1960)が考案された。 これらはエルブランの定理の証明を直接計算機上で実行するようなやり方だったため、多数の不要な基礎例の生成が行われ、効率的ではなかった。

1965年にJ. Robinsonは単一化に基づく導出原理を発表した。導出原理ではただ1つの推論規則  ${\frac {A\vee B,\lnot A\vee C}{B\vee C}}$${\frac {A\vee B,\lnot A\vee C}{B\vee C}}$を用い、エルブランの定理により証明したい論理式の否定から空節が導かれること︵反駁︶により証明を行う。

推論の過程で多数の基礎例の生成を行うのではなく単一化により必要な基礎例のみを段階的に具体化していくことで、導出原理では効率的な推論が可能になり、その後の定理証明やPrologなどの論理プログラミング言語に大きな影響を与えた。

関連項目

• ジャック・エルブラン
• 導出原理
• 自動定理証明
• 論理プログラミング
• 数学基礎論

• 論理学者

参考文献

• Buss, Samuel R. (1995), “On Herbrand's Theorem”, in Maurice, Daniel; Leivant, Raphaël, Logic and Computational Complexity, Lecture Notes in Computer Science, Springer-Verlag, pp. 195–209, ISBN 978-3-540-60178-4, http://math.ucsd.edu/~sbuss/ResearchWeb/herbrandtheorem/ .
• 佐藤健, Marina De Vos (2008), 論理コンピューティング, <レクチャーシリーズ>知能コンピューティングとその周辺, 人工知能学会誌, Vol23(5), pp.677-686.

外部リンク

• Alex Sakharov. "Herbrand's theorem". mathworld.wolfram.com (英語).
• Alex Sakharov. "Cut Elimination Theorem". mathworld.wolfram.com (英語).