アリストテレスとゲーデル

 いつ頃からか暇なときには数学史や自然哲学史の本を読んでいます。最初は広く浅く、様子がわかってくるにつれ特定の時代、特定の人物、特定のテーマについてより深く追いかけるようになりました。最近は19世紀から20世紀初頭までの数学史と論理学史に取り組んでいます。

 18世紀後半に英国から始まった産業革命は19世紀には他の国々にも広がり、19世紀後半には第二次産業革命と呼ばれる新たな技術革新の波が起こり、鉄鋼、化学工業、電力、電信電話などの新しい産業が発展しました。この時期には科学や思想においても急速な進展が見られました。伝統論理学は哲学の一分野として捉えられてきましたが、19世紀に入ると科学全般、特に数学を語るための実用的な言語として記号論理学が生まれ、急速に発展しました。その影響により古典数学は大きな変革を遂げ、20世紀初頭にはユークリッド原論とは全く異なる現代数学の土台がほぼ完成するという歴史的転換が起こりました。

 したがってこの時代の数学を知るにはまず論理学史から始めなければなりません。今日知られている限り、論理学に関する最初の著作はアリストテレスによって著わされました。「アリストテレス全集」はオルガノン(organon, 道具)と呼ばれる一連の著作から始まります。

• カテゴリー論
• 命題論
• 分析論前書
• 分析論後書
• トポス論
• 詭弁論駁論

このオルガノンの存在により論理学はアリストテレスが創始したとされ、伝統論理学はこれらを原典として論理学を展開しています。

 カテゴリーやトポスという用語は現代数学とは異なる意味ですが、命題の意味は現代の論理学と全く同じです。分析論前書では述語論理において四つの推論規則から妥当な推論式を演繹的に導くという一つの公理体系を作り上げようとしています。これはヒルベルト学派が1920年代から30年代にかけて研究し、最終的にゲーデルにより完全性が証明された述語論理体系に相当するといってもいいかもしれません。

 ギリシアの数学や自然哲学の本はある程度読んでいましたが、オルガノンは今回初めて目を通しました。というのもこれまでは個人的なアリストテレスに対する評価があまり高くなかったからです。その理由として『自然学(Physica)』において後にガリレオにより実験科学の方法で修正される力学に関する間違った言説を展開してことがあります。しかし分析論前書の内容の詳細を知り鳥肌が立ちました。

調査方法

 数学を応用した分野では特定のテーマに関する研究に関する文献調査をする場合、次のような段階を経ることが多いでしょう。

1. 対象を記述する数学モデルの正当性検証
2. 数学モデルの数値シミュレーション
3. 数学モデルに基づく実験装置の製作とその評価

このとき各段階において調査を支援するために様々なツールが用いられます。誰でも手軽に利用できるフリーソフトやサービスを中心に例を挙げます。

• 数学モデルの正当性検証
  • 数学解析ツール:Maxima, SymPy, SageMath
  • 文献検索:Google Scholar, ResearchGate, arXiv, JSTOR
• 数値シミュレーション
  • シミュレーションソフト:分野毎
  • プログラミング言語:Python
• 設計・データ解析
  • 設計ソフト:分野毎
  • データ解析:Python, R

 記号論理学の場合は数学、哲学、言語学、計算機科学という性格が異なる複数の分野にまたがっている関係で応用数学とはかなり様子が変わってきます。これに対応できる支援環境をどうやって構築し、それらを使いこなすスキルをどうやって育成するかは大きな課題です。暫定的に次のようなものを想定しています。

• 文献検索
  • Google Scholar, ResearchGate, arXiv, JSTOR
  • PhilPapers
• 定理証明支援系
  • Coq, Lean, Isabelle/HOL, Prover9
• 記号処理プログラミング
  • Common Lisp, Prolog
  • Racket, OCaml, Haskell
  • SymPy, Graphviz

これらすべての内容を把握できているわけではありません。また生成AIはかなり有望なツールとなる可能性があり、数年以内にこの中に入ってくると思われます。

記号処理演習

 ずんぶんと昔の話になりますが数理論理学の講義を受けているとき、担当教官が自動定理証明の研究をしているといううわさを耳にしました。Lispという記号処理のためのプログラミング言語があることも聞いていたので、おそらくLispを使っていたと思われますがはっきりしたことはわかりません。このとき、いつか機会があればLispを使って論理式計算や自動定理証明をやってみたいと思っていました。

 そういう経緯もありLispで論理式を計算するツールを試しに作ってみることにしました。最初はCommon Lispの勉強から始めました。手元に『Common Lisp入門』[4]という手頃な本があったので、Ubuntu上にCLISPをインストールしていろいろ実験してみました。ある程度使えるようになったので『記号処理プログラミング』[5](2.3 定理の自動証明)を参考にして実際に命題論理式の計算をしてみました。すると思っていたよりも簡単にできることがわかりました。しかし同時にLispは様々な点で古くなっているということも感じました。その後 Scheme、RacketとLisp系の開発環境を試し、Lisp系ではRacketを選びました。

 次に自動定理証明の先人達はどのようなプログラムを開発しているのかを調べました。意外なことに入手できた情報の範囲ではLisp系やProlog系で書かれたものはほとんどなく、エディンバラ大学で開発された関数型言語ML(Meta-Language)系統のものが多いことがわかりました。その中で有名な定理証明支援系CoqはOCamlで書かれていたのでML系としてOCamlを選びました。

 この段階でC++経験者向けの記号処理プログラミングのスキル向上のための演習メニューを考えてみました。具体的にはModern C++(C++11以降)とOCaml, Racketを比較しながら基礎練習をするというものです。

1. Modern C++
2. OCaml
3. Racket

という三言語で同じ課題のプログラムを書き分けることで関数型プログラミングの特徴をある程度把握することができるようになっています。公開されたプログラムは必ずしも各課題に対する模範解答になっているとは限りません。誤りやより良い方法を見つけたとき、あるいは関連情報をご提供いただける場合はpisan-dub.jpの方へ連絡していただければ幸いです。

 この記号処理演習は今後、必要に応じて内容が増えていく予定です。

 本文書とこれに含まれるソフトウェアはMIT Licenseにより公開されています。