数理論理学とは何か
数理論理学は、数学における推論 deduction を形式化し、その推論自体を数学の対象とする取り組みです。
「推論の形式化」はGottlob Frege (1848-1925) に、「数学の推論自体を対象とする数学」はDavid Hilbert (1862-1943)に端を発しています。
われわれ論理学者は、数学における証明や論理式をメタ的に換言すると外から眺め、証明や論理式自体に内在する性質を調べています。
論理学者の関心に従って数理論理学を大別すると以下のようになります。
- 公理的集合論 Axiomatic Set Theory
- モデル理論 Model Theory
- 計算理論 Computability Theory
- 証明論 Proof Thoery
論計舎は主に証明論と計算論を得意とします。
証明論とは
証明論とは、証明を数学的構造として形式化し、証明に内在する性質を調べる分野です。
証明論は、Hilbert計画に端を発すると言えるでしょう。その詳細には触れませんが、Hilbert計画は、すべての数学を公理化すなわち公理的な形式体系に還元してその公理化が無矛盾 consistent であることを証明しよう、というものです。
Hilbertは、この無矛盾性証明が「有限的な finitary 」手法でのみ行われるべきと考え、その考え方を有限の立場 Finitary Point of View と言います。
Kurt Gödel (1906-1978) による完全性定理 Completeness Theorem という結果は、Hilbertの有限主義的形式体系に数学を還元するという目的に沿ったものでした。
にもかかわらず、それに続くGödelのかの有名な不完全性定理 Incompleteness Theorem は、その不可能性を強く示唆する結果となりました。
しかしながら、それに続くGerhard Karl Erich Gentzen (1909-1945)の業績、特に算術の無矛盾性証明は有限の立場における成果として評価する向きもあります。
一部の数学者が証明論をGentzenの業績を理解する試みであると位置付けるほど、Gentzenが証明論に与えた影響は大きいものです。
計算理論とは
計算理論は、関数が計算可能であることが意味するところとか
計算不可能関数がその不可能性に基づいてどのように階層分けされるかなどを、根源的な問いとします。
計算理論は、1930年代のAlan Mathison Turing (1912-1954) による人間が行う計算に関する数学的分析や、Stephen Cole Kleene (1909-1994)による数学の中での計算という操作の数学的本性の研究などに起源を持ちます。
こうした探求から発展していく過程で、この分野は、どのような関数が計算可能なのかとか関数をはじめとするどの数学的諸概念が厳密に定義可能なのかとかと問えるようになりました。それぞれは、計算可能性、定義可能性と呼ばれ、現在でも強く関心を持たれています。
計算理論は、先述した根源的な問いへの答えを探す中で豊かな理論に成長したのです。
また計算理論は証明論と密接に関わりをもちますし、理論計算機科学へと発展していきました。
HilbertとGödelはまた、計算理論においても重要人物です。
Wilhelm Friedrich Ackermann (1886-1962) とともにHilbertは、一階述語論理 First-order Logic 内の任意の文が、一階述語論理で導出可能かを決定することの可能性を問いました。
これを決定問題 Entscheidungsproblemと言います。決定問題に対して
ChurchとTuringが、数学的には実行的に決定できない問題があるという証明を、Gödelの不完全性定理の証明の技法を用いて、それぞれ独立に行ったのです。
また、歴史的にコンピュータは、計算は機械的に実行できるという計算理論による示唆から発生しているという見方ができます。論計舎のもう一つの柱である理論計算機科学は、
こうした機械的に計算を実行するというプロセス自体の研究です。
このように、証明論と計算理論とそして理論計算機学は深く関連する分野なのです。
使用テキスト例
リンク先は出版社ページです。