|
|
| 1行目: |
1行目: |
| − | '''エルブランの定理'''（{{lang-en-short|''Herbrand's theorem''}}）は1930年に[[ジャック・エルブラン]]が発表した[[数理論理学]]上の基本定理である
| + | {{テンプレート:20180815sk}} __NOINDEX__ |
| − | <ref>J. Herbrand, ''Recherches sur la théorie de la démonstration''. Travaux de la Societe des Sciences et des Lettres de Varsovie, Class III, Sciences Mathematiques et Physiques, 33, pp.33-160, 1930.</ref>。
| |
| − | エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。
| |
| − | :<math>F</math> を節の有限集合とするとき、以下の2つは同値である。
| |
| − | :* <math>F</math> が充足不能
| |
| − | :* <math>F</math> から得られる基礎例（エルブラン基底）の有限集合で充足不能なものが存在
| |
| − | | |
| − | エルブランの定理は[[一階述語論理]]における任意の[[恒真式|恒真]]な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの[[自動定理証明]]の理論的な基盤になっている。[[チューリングマシン]]の[[停止性問題]]と同様、一般的な述語論理式が証明可能かどうかを求めるアルゴリズムは存在しないが、エルブランの定理では[[一階述語論理]]を[[命題論理]]と結び付けることで、一階述語論理での証明可能性についての部分的な回答を与えている。
| |
| − | | |
| − | なお、エルブランの本来の証明は任意の一階述語論理式を対象としたものだが<ref name=Buss1995>Buss, Samuel R., "On Herbrand's Theorem", in Maurice, Daniel; Leivant, Raphaël, Logic and Computational Complexity, Lecture Notes in Computer Science, Springer-Verlag, pp. 195–209. 1995.</ref>、多くの場合、[[冠頭標準形|冠頭形]]の論理式に制限し単純化した定理で表される。
| |
| − | | |
| − | == エルブラン領域 ==
| |
| − | '''エルブラン領域'''（{{lang-en-short|''Herbrand universe''}}）とは、述語論理式に現れうる変数を含まない全ての項の集合である。
| |
| − | | |
| − | 述語論理式の''項''は以下の定義から帰納的に表される。
| |
| − | * 任意の個体定項（''定数''）は項である。
| |
| − | * 任意の個体変項（''変数''）は項である。
| |
| − | * 任意の n [[アリティ|引数]]の''関数記号'' ''f'' と複数の項からなる ''f(t<sub>1</sub>, .. ,t<sub>n</sub>)'' は項である。
| |
| − | | |
| − | 論理式を構成する記号として定数及び関数記号が定められているとき、変数を含まない項（''閉項''、''{{lang|en|closed term}}''）の全体を''エルブラン領域''（''{{lang|en|Herbrand universe}}''）といい、以下の式 ''H'' で表すことができる。論理式に定数が含まれない場合は任意の定数 c を付加する。
| |
| − | :<math>H =\textstyle H_{\infty}</math> | |
| − | :* <math>H_0 = \big\{ c \big\}</math> （cは定数記号）
| |
| − | :* <math>H_{i+1} = H_i \cup \big\{f(t1,\ldots,tn)|t_j \in H_i \big\}</math> （''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)), ‥ '' となる。
| |
| − | | |
| − | == エルブラン基底とエルブラン解釈 ==
| |
| − | エルブラン領域の全ての要素を論理式を構成する[[原子論理式]]に割り当て、それぞれの真偽値を決めることで、論理式に対する任意の解釈が表現できる。
| |
| − | | |
| − | エルブラン領域の要素を引数とする[[原子論理式]]の全体を'''エルブラン基底'''（{{lang-en-short|''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)), ‥ '' となる。
| |
| − | | |
| − | 一般に変数をもたない述語または節のことを''基礎例''(''{{lang|en|ground instance}}'') と言う。エルブラン基底は節集合から得られる基礎例である。
| |
| − | エルブラン基底を導入することで、論理式を[[命題論理]]式として扱うことができ、論理式の意味を[[統語論|構文的]]に決めることができる。
| |
| − | | |
| − | エルブラン基底の任意の部分集合 ''I'' を'''エルブラン解釈'''（{{lang-en-short|''Herbrand interpretation''}}）と呼ぶ。直感的には、エルブラン基底の要素の内 ''I'' に含まれるものは真、それ以外は偽を表し、真偽値の割り当てにより論理式全体に対する1つの解釈を定めたことになる。
| |
| − | | |
| − | == エルブランの定理 ==
| |
| − | エルブランの定理は、以下のように表現できる。
| |
| − | | |
| − | <blockquote class="toccolours" style="text-align:justify; width:60%; float:center; padding: 10px; display:table; margin-left:80px;">
| |
| − | :<math>F</math> を節の有限集合とするとき、以下の2つは同値である。
| |
| − | :* <math>F</math> が充足不能
| |
| − | :* <math>F</math> から得られる基礎例（エルブラン基底）の有限集合で充足不能なものが存在
| |
| − | </blockquote>
| |
| − | | |
| − | つまり、[[一階述語論理]]式の充足不能性の判定は、エルブラン基底上の有限回の[[命題論理]]レベルでの判定で行うことができる。
| |
| − | | |
| − | エルブランの定理はこれ以外にも様々な形式で表現することができる。
| |
| − | | |
| − | 一般に、論理式の真偽値は対象となる領域 ''D'' とその解釈 ''I'' の組（モデル）により異なる。例えば、<math>\forall x \exists y(x>y)</math> は、[[自然数]]を領域とするか[[実数]]を領域とするかで真偽値が変わる。モデルにより以下の3通りが考えられる。
| |
| − | * 恒真（''{{lang|en|valid}}''）・・・全てのモデルで真
| |
| − | * 充足可能（''{{lang|en|satisfiable}}''）・・・少なくとも１つのモデルで真
| |
| − | * 充足不能（''{{lang|en|unsatisfiable}}''）・・どんなモデルでも偽（=恒偽）
| |
| − | | |
| − | 以下では、例として <math>\forall x \forall y P(x,y)</math> のような全称論理式(あるいは論理式の集合) <math>F</math> を考える。<math>P</math> は述語、 <math>a_1, a_2, ..., a_n, ...</math> は変数の集まりを表す。以下の3つの特性について考える。
| |
| − | # <math>F</math> は'''無矛盾'''（''{{lang|en|consistent}}''）、つまり <math>F</math> を仮定した場合に矛盾（<math>F \land \lnot F</math>）を導きだせないこと。これは <math>\lnot F</math> が[[自然演繹]]のような述語論理の演繹システムで導きだせないことで、次のように表記する：<math>\not\vdash \lnot F</math>.
| |
| − | # <math>F</math> は'''充足可能'''（''{{lang|en|satisfiable}}''）、つまり <math>F</math> が真となるようなモデルが存在すること。これは次のように表記できる：<math>\not\vDash \lnot F</math>.
| |
| − | # 全ての <math>n</math> に対し、以下 <math>Q(a_1, ..., a_n)</math> と表現する以下の論理式を真にするようなモデルが存在すること。これは次のように表記できる：全ての <math>n</math> に対して<math>\not\vDash \lnot Q(a_1, ..., a_n)</math>
| |
| − | | |
| − | :<math>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)</math>
| |
| − | | |
| − | [[ゲーデルの完全性定理]]は上の(1)と(2)が同値であると主張している。さらに(2)は(3)を含み、(3)で真となるモデルは(2)のモデルとなる。エルブランの定理は逆に、エルブラン領域という特定の領域で(3)が(2)を含んでいるということを主張する。つまり、エルブラン領域という特定の領域で考えると、上の(2)と(3)はエルブランの定理の別の表現であり、(1)、(2)、(3)は同値である。なお、エルブラン領域では変数が無くなるため(3)での全称記号が消え、解くべき論理式は[[命題論理]]の命題として扱うことができる。
| |
| − | | |
| − | ''G'' = ''¬F''、''R'' = ''¬Q''、''S'' = ''¬P'' と置いて[[双対]]を考えると、上と等価な3つの特性を得ることができる。
| |
| − | # <math>G</math> は'''証明可能'''（''{{lang|en|provable}}''）、つまり命題論理の演繹システムで <math>G</math> を導くことができること。これは次のように表記する：<math>\vdash G</math>
| |
| − | # <math>G</math> は'''恒真'''（''{{lang|en|valid}}''）、つまり <math>G</math> は全てのモデルで真になる。これは次のように表記する：<math>\vDash G</math>.
| |
| − | # ある<math>n</math> に対し、以下の <math>R(a_1, ..., a_n)</math> が恒真になるような <math>n</math> が存在すること。これは次のように表記する：<math>\vDash R(a_1, ..., a_n)</math>
| |
| − | | |
| − | :<math> 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)</math>
| |
| − | :（ <math>t_1, t_2, ..., t_n</math>は変数 <math>a_1, a_2, ..., a_n</math> をエルブラン領域の要素で置き換えたもの）
| |
| − | | |
| − | 前と同様、上の(2)と(3)はエルブランの定理の別の表現であり、(1)、(2)、(3)は同値である。
| |
| − | | |
| − | ここで、''F'' が充足不能のとき（すなわち ''G'' = ''¬F'' が恒真のとき）を考える。<math>Q(a_1, ..., a_n)</math> を<math>n=1</math>、<math>n=2</math> と調べていくと、<math>Q(a_1, ..., a_n)</math> が偽となるような ''n'' が存在する（そうでなければ全ての ''n'' で真となるため充足可能となってしまう）。またその逆も成り立つ。
| |
| − | これを利用し、任意の[[恒真式|恒真]]な論理式 ''G'' の証明を行いたい場合、論理式の否定 ''¬G'' の充足不能性を調べることで、エルブラン解釈の下での有限回の操作で調べることができる。これはエルブランの定理の重要な成果である。
| |
| − | | |
| − | それとは反対に、''F'' が充足可能のとき、全ての ''n'' に対し <math>Q(a_1, ..., a_n)</math> が真となり、変数 <math>a_i</math> が有限でない場合は計算が終わらない。これは、一般に述語計算が[[決定可能]]でないことを示している。
| |
| − | | |
| − | より形式的には、エルブランの定理は上の(2)、(3)について、論理式 <math>S(x,y)</math> をより一般化した形で表現される。また対象となる論理式は[[冠頭標準形]]の式である。以下に形式化されたエルブランの定理の例を示す。
| |
| − | | |
| − | <blockquote class="toccolours" style="text-align:justify; width:80%; float:center; padding: 10px; display:table; margin-left:80px;">
| |
| − | <math>(\exists y_1,\ldots,y_n)F(y_1,\ldots,y_n)</math> を[[一階述語論理]]式とする。ここで <math>F(y_1,\ldots,y_n)</math> は[[量化|量化子]]を1つも含まない論理式である。
| |
| − | | |
| − | このとき <math>(\exists y_1,\ldots,y_n)F(y_1,\ldots,y_n)</math> が[[恒真式|恒真]]になる必要十分条件は、ある自然数 <math>k</math> とエルブラン領域の項 <math>t_{i1},\ldots,t_{in}</math> （<math>1 \le i \le k</math>）が存在し、
| |
| − | ::<math>F(t_{11},\ldots,t_{1n}) \vee \ldots \vee F(t_{k1},\ldots,t_{kn})</math>
| |
| − | が恒真になることである。
| |
| − | </blockquote>
| |
| − | | |
| − | このようなエルブランの定理の証明は、[[ゲーデルの完全性定理]]により[[恒真式|恒真性]]が証明可能性に置き換えられることを利用し、[[ゲルハルト・ゲンツェン|ゲンツェン]]の[[カット除去定理]]を用い <math>\vdash (\exists y_1,\ldots,y_n)F(y_1,\ldots,y_n)</math> のカット規則を除去した証明を求めるものが一般的である。
| |
| − | | |
| − | [[ジャック・エルブラン|エルブラン]]が定理を証明した時にゲンツェンのカット除去定理はまだ知られておらず、ゲーデルの完全性定理も発表されていなかった。そのためエルブランによる証明はエルブラン版のカット除去定理や独自の[[ゲーデルの完全性定理|完全性定理]]を含むもので<ref name=Buss1995></ref>、任意の一階述語論理式を対象としていた<ref name=Buss1995></ref>。
| |
| − | | |
| − | == 応用 ==
| |
| − | エルブランの定理は[[自動定理証明]]の理論的基盤となった。
| |
| − | | |
| − | さらにエルブランの定理を計算機上で直接応用する試みが行われ、[[ギルモアのアルゴリズム]](1960)や[[デービス・パトナムのアルゴリズム]](1958,1960)が考案された。
| |
| − | これらはエルブランの定理の証明を直接計算機上で実行するようなやり方だったため、多数の不要な基礎例の生成が行われ、効率的ではなかった。
| |
| − | | |
| − | 1965年にJ. Robinsonは[[ユニフィケーション|単一化]]に基づく[[導出|導出原理]]を発表した。導出原理ではただ1つの推論規則
| |
| − | <math>\frac{A \vee B, \lnot A \vee C} {B \vee C}</math> を用い、エルブランの定理により証明したい論理式の否定から空節が導かれること（反駁）により証明を行う。
| |
| − | | |
| − | 推論の過程で多数の基礎例の生成を行うのではなく[[ユニフィケーション|単一化]]により必要な基礎例のみを段階的に具体化していくことで、導出原理では効率的な推論が可能になり、その後の[[自動定理証明|定理証明]]や[[Prolog]]などの[[論理プログラミング]]言語に大きな影響を与えた。
| |
| − | | |
| − | == 関連項目 ==
| |
| − | *[[ジャック・エルブラン]]
| |
| − | *[[導出|導出原理]]
| |
| − | *[[自動定理証明]]
| |
| − | *[[論理プログラミング]]
| |
| − | *[[数学基礎論]]
| |
| − | | |
| − | *[[論理学者]]
| |
| − | | |
| − | == 参考文献 ==
| |
| − | *{{Citation | last1=Buss | first1=Samuel R. | editor1-last=Maurice | editor1-first=Daniel | editor2-last=Leivant | editor2-first=Raphaël | title=Logic and Computational Complexity | publisher=Springer-Verlag| series=Lecture Notes in Computer Science | isbn=978-3-540-60178-4 | year=1995 | chapter=On Herbrand's Theorem | chapterurl=http://math.ucsd.edu/~sbuss/ResearchWeb/herbrandtheorem/ | pages=195–209}}.
| |
| − | *佐藤健, Marina De Vos (2008), ''[http://ci.nii.ac.jp/naid/110006894566 論理コンピューティング]'', <レクチャーシリーズ>知能コンピューティングとその周辺, 人工知能学会誌, Vol23(5), pp.677-686.
| |
| − | | |
| − | == 脚注 ==
| |
| − | <div class="references-small">
| |
| − | <references/>
| |
| − | </div>
| |
| − | | |
| − | == 外部リンク ==
| |
| − | *{{MathWorld | urlname=HerbrandsTheorem | title=Herbrand's theorem | author=Alex Sakharov}}
| |
| − | *{{MathWorld | urlname=CutEliminationTheorem | title=Cut Elimination Theorem | author=Alex Sakharov}}
| |
| − | | |
| − | {{数学}}
| |
| − | | |
| − | {{DEFAULTSORT:えるふらんのていり}}
| |
| − | | |
| − | [[Category:数理論理学]]
| |
| − | [[Category:論理学]]
| |
| − | [[Category:数学基礎論の定理]]
| |
| − | [[Category:数学に関する記事]]
| |
| − | [[Category:エポニム]]
| |