数理論理学の概略と特徴

本稿では、数理論理学 Mathematical Logic とは何かを簡単に説明します。

本稿は、論計舎から発行している数理論理学スターターマニュアルからの抜粋・改稿です。

数理論理学とは

数理論理学は、数学における 推論 deduction を形式化し、その 推論自体を数学の対象とする取り組みです。 「推論の形式化」はFregeに、「数学の推論自体を対象とする数学」はHilbertに端を発しています。
われわれ論理学者は、数学における証明や論理式をメタ的に換言すると外から眺め、証明や論理式自体に内在する性質を調べています。

論理学者の関心に従って数理論理学を 大別すると以下のようになります。

• 公理的集合論 Axiomatic Set Theory

• モデル理論 Model Theory

• 計算理論 Computability Theory

• 証明論 Proof Thoery

私たち論計舎は証明論と計算論を得意とします。 したがって、ここで両分野をその繋がりとともに紹介します。

証明論とは

証明論とは、 証明を数学的構造として形式化し、証明に内在する性質を調べる分野です。

証明論は、 Hilbert計画に端を発すると言えるでしょう。
その詳細には触れませんが、 Hilbert計画は、すべての数学を公理化すなわち公理的な形式体系に還元してその公理化が無矛盾 consistent であることを証明しよう、 というものです。
Hilbertは、この無矛盾性証明が「有限的な finitary 」手法でのみ行われるべきと考え、 その考え方を 有限の立場 Finitary Point of View と言います。 Gödelによる完全性定理 Completeness Theorem
という結果は、Hilbertの有限主義的形式体系に数学を還元するという目的に沿ったものでした。にもかかわらず、 それに続くGödelのかの有名な不完全性定理 Incompleteness
Theorem は、その不可能性を強く示唆する結果となりました。
しかしながら、 それに続くGentzenの業績、特に算術の無矛盾性証明は有限の立場における成果として評価する向きもあります。

一部の数学者が証明論をGentzenの業績を理解する試みであると位置付けるほど、Gentzenが証明論に与えた影響は大きいものです。

計算理論とは

計算理論は、 関数が計算可能であることが意味するところとか計算不可能関数がその不可能性に基づいてどのように階層分けされるかなどを、根源的な問いとします。

計算理論は、1930年代のTuring[^7]による人間が行う計算に関する数学的分析や、Kleeneによる数学の中での計算という操作の数学的本性の研究などに起源を持ちます。
こうした探求から発展していく過程で、この分野は、どのような関数が計算可能なのかとか関数をはじめとするどの数学的諸概念が厳密に定義可能なのかとかと問えるようになりました。 それぞれは、計算可能性、定義可能性と呼ばれ、現在でも強く関心を持たれています。
計算理論は、先述した根源的な問いへの答えを探す中で豊かな理論に成長したのです。
また計算理論は証明論と密接に関わりをもちますし、理論計算機科学へと発展していきました。

HilbertとGödelはまた、 計算理論においても重要人物です。HilbertとAckermannは、 一階述語論理 First-order Logic 内の任意の文が、 FoLで導出可能かを決定することの可能性を問いました。これをEntscheidungsproblemと言います。 Entscheidungsproblemに対してChurchとTuringが、数学的には実行的に決定できない問題があるという証明を、Gödelの不完全性定理の証明の技法を用いて、それぞれ独立に行ったのです。

また、 歴史的にコンピュータは、 計算は機械的に実行できるという計算理論による 示唆から発生しているという見方ができます。論計舎のもう一つの柱である理論計算機科学は、こうした機械的に計算を実行するというプロセス自体の研究です。

このように、証明論と計算理論とそして理論計算機学は深く関連する分野なのです。

論計舎と数理論理学スターターマニュアルもよろしくお願いします！