コンピュータ定理証明における弁証法 − 私が作りたいシステム

■	コンピュータ定理証明

コンピュータ上での定理証明は、整えられた環境でコンピュータにガイドされながら、特殊なプログラムを書く作業であると言っていい。そのプログラムが実行されると、入力物である真偽不明であった命題が、真なる定理として型付けされ出力されるのだ。

記号論理を勉強したことがある方は、その証明のフェーズを思い出して欲しい。まず証明しようとする命題を一番下に置き、その命題に使えるルールを上に足したり、上に書かれた前提からルールを使って一時的な定理を導出したりして下の命題とルールで結ぼうとする。

コンピュータ上では、これがさらに便利になって、自動的に適用するルールを決めたり、ルールの繰り返しができたりする。

それどころか、ほとんどのフェーズを自動的にやってしまい、命題を入力したあとは、適当なルールセットを指定すれば、本当に自動的に証明がなされ、定理が得られることも多い。

ただ、なぜ「多い」かというと、命題を小分けにしてほとんど自明なものにする場合が「多い」だけなのかもしれないけれど。

■

理論モジュール

一種のプログラムであることもあり、C や JAVA などと同じくモジュールに分けることがある。基礎となる集合論のモジュールがあり、そこに実数の理論のモジュールを足したり、ラムダ計算のモジュールを足したり、といった感じである。

モジュールというのは加えたり加えなかったりが簡単にできることがその原義だが、理論のモジュールはプログラミング言語のモジュールほど柔軟ではない。

プログラミング言語の場合、関数名がその中のプログラムを隠して「モジュール化」してしまうが、定理証明システムの場合、定理がその証明プログラムを隠しても、定理そのものが構造を持っているため、その定理のちょっとした変更などが、その理論モジュールを使うモジュールに影響してしまう。

しかし、このしばりも若干緩和することができる。それは自動証明のルールセットの中に定理を入れ、理論モジュールを使うときは定理をそのまま使うのではなく、自動証明のルールセットを使うようにすれば、定理の形の多少の違いは自動証明のフェーズの中で消化されてしまう。

ただし、自動証明は万能なものではないため、結局定理やその変形物をそのまま扱わねばならないこともしばしばである。

■

弁証法

さて少し話は変わるが、「弁証法」という論理的手法をご存知だろうか。記号論理ばかりやってる方は意外に忘れるか習わない言葉である。

ヘーゲルの書で有名な手法で《Wikipedia：弁証法》には

> ● ある命題（テーゼ＝正）と、それと矛盾する命題（アンチテーゼ＝反）、もしくは、それを否定する反対の命題、そして、それらを本質的に統合した命題（ジンテーゼ＝合）の３つである。全てのものは己のうちに矛盾を含んでおり、それによって必然的に己と対立するものを生み出す。生み出したものと生み出されたものは互いに対立しあうが（ここに優劣関係はない）、同時にまさにその対立によって互いに結びついている（相互媒介）。最後には二つがアウフヘーベン aufheben（止揚）される。このアウフヘーベンは「否定の否定」であり、一見すると単なる二重否定すなわち肯定＝正のようである。しかしアウフヘーベンにおいては、正のみならず、正に対立していた反もまた保存されているのである。ドイツ語のアウフヘーベンは「捨てる」と「持ち上げる」という、互いに相反する二つの意味をもちあわせている。 (なお、ヘーゲルの弁証法における「矛盾」は数学や(記号)論理学における「矛盾」 とは全く別物であるので注意が必要である。)

とある。(私は「矛盾」は「全く別物」とは思っていない。念のため。)

記号論理においては矛盾があれば、それで終りであるが、記号論理において弁証法をムリヤリあてはめるとすると、それは矛盾を解消するための理論の再構築を意味するだろう。

高階論理の立場から私は最も単純に弁証法とは矛盾などの解消のため理論のパラメータを一つ足す行為に相当すると考える。Pure Type System などの高階論理の立場では公理を足すのもパラメータを足すのとほぼ同じことなので、これだけで私の言いたいことは言い得ていると思う。

パラメータを一つ足すと言えば簡単に聞こえるかもしれないが、その影響は測りしれない。足された定理だけでなくその理論やそれに続く理論すべてに影響が及ぶことがあるのである。

だから、このようなことはコストが高く、記号論理の世界では慎しむべきことだった。

記号論理の世界では？

では、コンピュータ定理証明ではどうだろうか。

自動証明が、その影響を打消してくれるなら、必ずしもコストが高いとは限らない。もちろん、今は自動証明そのものがマシンコストがかかるものではあるが、これもコンピュータの発展により少なくなってきている。

私は「弁証法」に対応することを目的としたコンピュータ定理証明の改良を夢見て研究をしていた。

■	私が作りたいシステム

しかし、上のようなシステムの提案は難しく、今は、上のコンピュータ定理証明を想起させるようなプログラミング言語のインタプリタを創りたいと考えています。

スピードなどより主に仕様を重視して、Smalltalk が「オブジェクト指向」を提示したように、一つのパラダイムを提示するものを作りたいと考えています。とはいえ、これも現在、言語の仕様のアイデアを羅列していくところまでしかいっていません

■

参考文献

自動証明のくだりなどは Isabelle のシステムを参考に書いています。

Pure Type Systemは“Lambda calculi with types” (Henk P. Barendregt, In “Handbook of Logic in Computer Science, Vol.II”, Oxford University Press, 1992)に載っている高解論理のメタシステムです。

哲学者的な「弁証法」理解は私のものとはかなり違うようです。《数学屋のメガネ：弁証法論理の理解》を参考に挙げておきます。

以前、このブログで少しこのあたりのことを言及しています。《なぜ記号論理学から社会科学を目指すようになったのか》

更新：	2006-09-07
初公開：	2006年09月07日 17:29:40
最新版：	2006年09月07日 18:10:20