数学基礎論

は、現在の日本では、もっぱら数理論理学（mathematical logic）を指す言葉として使われる。
概要.
他.
かつてはヒルベルトとベルナイスの『数学の基礎』に基づき、ヒルベルト・プログラムによって数学の諸体系の無矛盾性証明を行う超数学 (metamathematics) としての証明論を指す言葉であった。
歴史.
19世紀末に、ゲオルク・カントルにより、集合が考えられた。集合にもとづいた数学の再整理は大きな成果を生み、数学において欠くべからざる道具となってきた。一方、バートランド・ラッセルは、素朴な集合の取り扱い（内包公理）により「自分自身を要素としない集合全体の”集まり”」も集合とされるが、左記の集合は、それ自身を要素としない時、その時に限り自身を要素とするという矛盾を引き起こすことをラッセルのパラドックスとして指摘した。ここに、数学の基礎付けの問題が発生した。
パラドックスをめぐる立場は、大きく論理主義、直観主義、形式主義の３つに分けられる。
論理主義は、数学を論理学の上に基礎づける立場で、フレーゲの独創的な仕事に始まる。実は、ラッセルのパラドックスはフレーゲによる論理体系の矛盾を指摘したものであったが、その後、ラッセルは『数学原理』によってラッセルのパラドックスも解決する。
しかし、そこに用いられた公理は、もはや論理的に自明とはいえず、本来の数学の基礎付けの目的を達成したとはいえないものとなった。
直観主義は、数学的な対象や真理が、精神活動によって直接とらえられるものとする立場で、ブラウワーが提唱した。彼は数学における構成的方法を重視したが、そのため排中律の無制限な使用が不当であると非難した。たとえば、「自然数の狭義減少数列は、かならずある項で最小値をとる」という定理は、「自然数の狭義減少数列で、どの項をとってもその先により小さい項をもつものがある」という前提から矛盾を導くことで証明されるが、一方、任意の自然数の狭義減少数列に対して、どの項が最小値となるか具体的に構成する方法があるわけではない。したがって、直観主義の立場では「自然数の狭義減少数列は、かならずある項で最小値をとる」とはいえず、「自然数の狭義減少数列は、かならずある項で最小値をとることがないとはいえない」と二重否定の形で述べざるを得ないことになる。排中律を制限した非古典論理としての直観主義論理に基づく数学は、通常の排中律を認める古典論理に基づく数学とは異なる形のものとなる。
形式主義は、数学を公理と推論法則によるゲームとみなし、有限の立場により数学の無矛盾性を証明するによるヒルベルト・プログラムによって、数学の基礎付けを行う立場で、ダフィット・ヒルベルトが提唱した。ヒルベルト・プログラムは、「数学の証明を研究する数学」としての超数学である証明論を生み出した。一方、ゲーデルの不完全性定理によって「自然数論を含む帰納的公理化可能な理論が無矛盾であれば、それ自身の無矛盾性証明が存在しない」ことが示され、ヒルベルト・プログラムは一応の決着をみた。ゲーデルの仕事により、数学の形式体系の構文論（証明論）のみならず、意味論（モデル理論）や、計算可能性に関する再帰理論の研究が進むことになり、数学基礎論から数理論理学へと進化していった。
（以上、岩波数学辞典第４版の記載に基づく。ただし、直観主義の説明中の例は、照井一成「コンピュータは数学者になれるのか？」(青土社）の例から拝借した。）
日本では、数学基礎論は、歴史的経緯により、本来の数学の基礎付けの意味だけでなく、それに用いられる超数学および数理論理学の意味でも用いられる。
影響.
数学を人間の精神活動から離れて、形式主義的にかつ有限の立場から検証しなおすことにより、計算機科学の基礎と発展に大きく寄与した。たとえば、今まで自明なものとして受け入れられていた多くの数論的関数を有限の立場から考察することにより、アルゴリズムの研究に直接の影響を与えた。プログラミング言語で必ず登場するデータ型の形式的宣言や論理構造、関数の概念は遠くは数学基礎論に由来する。数学基礎論で活躍したフォン・ノイマンやチューリングが後に計算機科学において先駆的な役割を果たした。そのような意味で数学基礎論は単なる机上の空論ではなく、むしろコンピュータをインフラの一つとする現代社会の形成に多大な影響を与えた。