2002年 9月 1日 作成 述語論理の公理系 >> 目次 （テーマ ごと）
2007年11月 1日 補遺 　


　
　今回は、述語論理の公理系を扱う。

　理論は、いくつかの命題を前提にして、それらの命題だけを用いて構築される。
　前提とされる命題が 「公理」 であり、前提の命題を集めた全体を公理系 （system of axioms） と呼ぶ。
　現代数学では、公理を理論の前提 （仮定） として扱う。

　公理は理論の仮定であるから、どのような公理を選ぶかという点は恣意的である。
　ただし、その理論が整合性を保全するためには、以下の 3点が保証されていなければならない。

　（1） 無矛盾性（consistency, noncontradiction）
　　　A ∧ ¬A となるような論理式 A が存在しない。

　（２） 独立性（independence）
　　　任意の公理 A が、それが属する公理系の他の公理から導かれない。

　（３） 完全性（complete, categorical）
　　　任意の論理式 A に関して、それが トートロジー ならば、体系のなかで証明可能である。
　　　つまり、「恒真」 とは 「証明可能」 のことをいう。

[ 参考 ]
　命題が要素命題のいかなる真・偽の可能性に対しても、常に、真になるとき、同語反復的命題 （トートロジー） である、という。

　
　算術の公理系として、ペアノ の公理系がある。
　集合論の公理系には、ZF や BG がある。
　述語論理の公理系には、ラッセル と ホワイトヘッド が示した公理系--彼らの共著 「Principia Mathematica」 の頭文字を使って、通常、PM と呼ばれている--とか、ヒルベルト と ベルナイス が示した公理系--通常、H と略称される--がある。

　公理系 H は、以下の 12個の公理を用意している。

　（1）　A ⇒ （B ⇒ A）.
　（2）　（A ⇒ B） ⇒ （A ⇒ （B ⇒ C）） ⇒ （A ⇒ C）.
　（3）　A ⇒ （B ⇒ A ∧ B）.
　（4）　A ∧ B ⇒ A.
　（5）　A ∧ B ⇒ B.
　（6）　A ⇒ A ∨ B.
　（7）　B ⇒ A ∨ B.
　（8）　（A ⇒ C） ⇒ （（B ⇒ C） ⇒ （A ∨ B ⇒ C））.
　（9）　（A ⇒ B） ⇒ （（A ⇒ ¬B） ⇒ ¬A）.
　（10） ¬¬A ⇒ A.
　（11） A (t) ⇒ ∃x A (x).
　（12） ∀x A(x) ⇒ A (t).

　以上の 12個の 「述語論理の公理」 から、（11） と （12） を外したら、「命題論理の公理」 となる。
　ちなみに、H では、同一律・矛盾律および排中律が公理になっていないことに注意されたい。
　そして、¬¬A ＝ A が公理として扱われている点を注目されたい。
　以上の公理を前提にして、H の体系では、以下の 3つの推論規則が用意されている。

　（1） 　A, A ⇒ B　
　　　　　　　 B

　（2） 　A (a) ⇒ C　
　　　 ∃x A (x) ⇒ C

　（3） 　C ⇒ A (a)　
　　　 C ⇒ ∃x A (x)

　以上の 3つの推論規則のなかで、命題論理の推論規則は （1） の三段論法だけである。
　（1） の推論規則を 「モーダス・ポーネンス （modus ponens）」 という。

[ 参考 ]
　伝統的な論理学では、三段論法は、いくつかの形式があるが、それらのなかでも、（1） の三段論法を モーダス・ポーネンス という。

　述語論理の完全性を証明した人物が ゲーデル である。 □

　



[ 補遺 ] （2007年11月 1日）

　ゲーデル の 「完全性定理」 は、第一階述語論理において、「恒真命題 （トートロジー） は、すべて、証明可能である」 ということを証明した定理です。「完全性定理」 を読むには、まず、以下の 4つの概念を把握しておかなければ、読んでも理解できないでしょうね （数学の専門家にとっては、以下の 4つの概念は既知のことでしょうが、私のような シロート が 「完全性定理」 の論文を最初に読んだとき、皆目、理解できなくて、[ 廣瀬・横田 共著 「ゲーデル の世界」 を案内役として、] 再読した際に、以下の 4つの概念が大切な役割を演じていることに、やっと、気づいた次第です）。

　　（1） 無矛盾 （T ├ ¬A ⇒ ｛T, ¬A｝ は無矛盾である）
　　（2） 恒真、充足的、恒偽
　　（3） 証明可能性
　　（4） 対偶 （A ⇒ B ≡ ¬B ⇒ ¬A）

　ゲーデル の 「完全性定理」 は、「T ├ ¬A」 （｛T, ¬A｝ は、或る モデル で充足的である） に対して対偶を使っていて--すなわち、「A が モデル M で恒真である ⇒ ¬A は モデル M で充足的でない」 という対偶を使っていて--、「¬A は、T の任意の モデル で充足的でない」 ことを示して、「T ├ A」 として、「恒真 ＝ 証明可能性」 を導いています。これらの概念 （無矛盾、恒真・充足的・恒偽、証明可能性、対偶） を前提にして、「完全性定理」 が、どのようにして構成されているかという点を 拙著 「論理 データベース 論考」 （131ページ） に示したので、参照してみて下さい。

　ちなみに、「完全性定理」 は、一般形として、「T が無矛盾なら、T の可算 モデル が存在し、そして、モデル が存在すれば、その形式的体系は無矛盾である」 という主張になるのですが、この モデル の存在性が、「不完全性定理」 に使われました。「完全性定理」 とか 「不完全性定理」 というふうに、ふつう、簡略名称が使われるので、われわれ シロート は、「完全性」 が証明された直後に、「不完全性」 が証明されたというのが奇妙に思われるのですが、それぞれの定理では、対象が違うのです--「完全性」 は 「述語論理の完全性」 であり、「不完全性」 は、「『或る条件の下--すなわち、算術化された体系--では』、体系が無矛盾であっても、『真』 とも 『偽』 とも判断できない命題を作ることができる」 という意味です。

　さて、「トートロジー （同語反復）」 という用語は、ウィトゲンシュタイン が 「論理哲学論考」 のなかで導入した概念で、以後、「命題論理」 のなかで、「命題関数 （真理関数）」 の恒真命題に対して使われるようになりました。述語論理の恒真性は、以下のような 「基本定理」 として まとめられるそうです。

　　　　述語論理の恒真性 ＝ トートロジー ＋ 量化定理

　「証明可能性」 も、ゲーデル 以後、ゲンツェン が 演繹体系 LK を導入して （1934年）、「証明」 の構造的研究が進み、そして、ヘンキン が 「不完全性定理」 を一般的な形で構成しました （1949年）。ゲンツェン の LK と ヘンキン の証明法を基にして、タブロー 法が作られました。

　述語論理の 「基本定理」 と タブロー 法を使って、ゲーデル の 「完全性定理」 を証明した書物として、以下を読んでみて下さい。

　　「ゲーデル と 20世紀の論理学 （2）[ 完全性定理と モデル 理論 ]」、田中一之 編、東京大学出版会。




　 << もどる ベーシックス すすむ >>
　 数学基礎論