Waseda Institute for Advanced Study (WIAS)早稲田大学 高等研究所

すべての根底にある「論理学」

物理学は学問の王様、数学は学問の女王様、といわれることがあります。それに対抗して私は、論理学は学問の「天皇陛下」であると主張したいと思っています。論理学とは、いくつかの命題（前提）から別の命題（結論）を導いていくという人間の「推論」を研究する学問です。古くはアリストテレスに始まり、20世紀には数学の基礎付けとして発展しましたが、論理学は今日、伝統的な学問の単なる象徴と考えられている節があります。
しかし、さまざまな分野を見渡すと、数学や哲学だけでなく最近では情報科学の分野でも、その基礎概念として論理学の需要はますます高まっています。たとえば、コンピュータは「計算する機械」です。計算も推論の一種で、論理学がその根底にあります。コンピュータ・サイエンスのパイオニアであるゲーデル、フォン・ノイマン、チューリングは、20世紀で最も著名な論理学者であることからも明らかでしょう。

2つの論理から新たに拡張論理を生み出す

私が行っている論理学研究の最近の成果を紹介します。私は、線形時間論理から無限論理への埋め込み定理を証明しました。そしてこの定理の考え方を使って、線形時間論理と無限論理を融合した「拡張時間論理」を生み出しました。
線形時間論理とは、時間を表現するための論理の一つです。時間の経過をパス（状態の列）としてとらえ、時間は未来に向かって直線的に進行すると考えます。枝分かれするツリー構造としてとらえる「分岐時間」と比べて、時間を直線でとらえる「線形時間」は人間の直感にあっていて、シンプルなのが特徴です。
この論理は情報科学分野において、ソフトウェア仕様・検証技術の基礎として広く使用されています。プログラムのバグを取るのに有効な「モデル検査」は、この線形時間論理をベースにしています。
無限論理は、イメージとしてはインターネットなどでよく使うアンド検索です。論理式で記述すると結合子の「アンド」が無限に続くもので、これを使うと「共有知識」を表現することができます。みんなが知る共有知識を論理的に記述すると、「jはαを知っている」「kがαを知っていることをjが知っている」ということを無限に繰り返すことになります。無限論理はこれを記述できます。
したがって、提案した拡張時間論理は「時間」と「共有知識」を同時に扱うことができる新しい論理ということになります。

情報科学分野での応用

この拡張時間論理は、今後、情報科学の分野において広く応用されると期待しています。論理学の情報科学への応用は、これまでもプログラミング言語の設計、データベース・知識ベースの設計、セキュリティープロトコルの検証、並行・分散システムの仕様・検証と多岐にわたっています。なかでも、線形時間論理はシンプルで扱いやすいため、多くの分野で利用されてきました。
ところが、現実世界に近いマルチエージェント環境においては適切に扱うことができないという弱点がありました。この環境での推論を扱うためには、「時間」だけでなく「共有知識」を適切な論理で形式化することが必要だったからです。今回提案した拡張時間論理は、「時間」と「共有知識」を同時に扱うことができ、マルチエージェント環境への適用が期待できます。

きれいな論理を見つける醍醐味

私はこの成果が、応用だけでなく本質的な観点からも意義があると考えています。線形時間論理から無限論理への埋め込みは、実は線形時間論理と無限論理という2つの論理の融合の中から導かれた定理です。これまで情報科学者が時間を解釈するために用いてきた線形時間論理は、時間という意味・解釈を取り除いて抽象的に考えると、無限論理の部分体系に過ぎないのです。
論理学は、人間の推論をむりやり記号化して分析していますが、これはコンピュータへの実装が簡単になるから、つまりはじめから応用を視野に入れているのです。このように応用を頭に入れて研究することも大切なのですが、論理学者として本音をいうなら、推論の中からきれいな論理を見つけて「推論の本質」を明らかにすることに論理学の醍醐味があると思います。

行き着いたのが「論理学」

人間の推論を記述したものはすべて「論理」です。だから、実は論理というものは無数に作られています。人間の推論は場面に応じてさまざまあり、それぞれに対応して適切な論理が考えられます。新しい分野が生まれると、それを形式化するために必要な論理が現れ、その中で一番使われるものが残っていくことになります。
私は学部時代、コンピュータの基本設計を学んでいました。そこから出発して、計算機という“考える機械”を作りたいと思いました。それを突き詰めていった結果、考えるとは推論すること、つまり論理学に行きついたというわけです。
残念ながら、日本では論理学は学問の一分野として認められているとはいえず、数学、哲学、情報科学の一分野として研究されているのが現状です。論理学は、学問の「天皇陛下」であるにもかかわらず、数学者、情報科学者を名乗っている隠れ論理学者は、案外多いのかもしれません。