数理論理学

数理論理学（すうりろんりがく、英 : mathematical logic）または現代論理学^[1][2]、記号論理学^[1][2]、数学基礎論^[3]、超数学は^[4]、数学の分野の一つであり^[4]、「数学の理論を展開する際にその骨格となる論理の構造を研究する分野」を指す^{[3][注 1]}。数理論理学（数学基礎論）と密接に関連している分野としてはコンピュータ科学（計算機科学）^[4]や理論コンピュータ科学（理論計算機科学）などがある^{[5][注 2]}。

前現代の論理学については「伝統的論理学」を参照

数理論理学の主な目的は形式論理の数学への応用の探求や数学的な解析などであり、共通課題としては(形式的体系)の表現力や形式証明系の演繹の能力の研究が含まれる。

数理論理学はしばしば集合論、モデル理論、再帰理論、証明論の4つの領域に分類される。これらの領域はロジックのとくに一階述語論理や(定義可能性)に関する結果を共有している。計算機科学（とくに(ACM Classification)（英語版）に現れるもの）における数理論理学の役割の詳細はこの記事には含まれていない。詳細は(計算機科学におけるロジック)（英語版）を参照。

この分野が始まって以来、数理論理学は数学基礎論の研究に貢献し、また逆に動機付けられてきた。数学基礎論は幾何学、代数学、解析学に対する公理的枠組みの開発とともに19世紀末に始まった。20世紀初頭、数学基礎論は、ヒルベルトのプログラムによって、数学の基礎理論の無矛盾性を証明するものとして形成された。クルト・ゲーデルとゲルハルト・ゲンツェンによる結果やその他は、プログラムの部分的な解決を提供しつつ、無矛盾性の証明に伴う問題点を明らかにした。集合論における仕事は殆ど全ての通常の数学を集合の言葉で形式化できることを示した。しかしながら、集合論に共通の公理からは証明することができない幾つかの命題が存在することも知られた。むしろ現代の数学基礎論では、全ての数学を展開できる公理系を見つけるよりも、数学の一部がどのような特定の形式的体系で形式化することが可能であるか（逆数学のように）ということに焦点を当てている。

下位分野

Handbook of Mathematical Logic は数理論理学を大まかに次の4つの領域に分類している：

1. 集合論
2. モデル理論
3. 再帰理論
4. 証明論と(構成的数学) （これらはひとつの領域の2つの部分と見做される）

それぞれの領域は異なる焦点を持っているものの、多くの技法や結果はそれら複数の領域の間で共有されている。これらの領域を分かつ境界線や、数理論理学と他の数学の分野とを分かつ境界線は、必ずしも明確ではない。ゲーデルの不完全性定理は再帰理論と証明論のマイルストーンであるだけではなく、様相論理における(レープの定理)（英語版）を導く。強制法の手法は集合論、モデル理論、再帰理論のほか(直観主義的数学)の研究などでも用いられる。

圏論の分野では多くの形式公理的方法を用いる。それには(圏論的論理)（英語版）の研究も含まれる。しかし圏論は普通は数理論理学の下位分野とは見做されない。圏論の応用性は多様な数学の分野に亙っているため、ソーンダース・マックレーンを含む数学者らは、集合論とは独立な数学のための基礎体系としての圏論を提案している。これはトポスと呼ばれる古典または非古典論理に基づく集合論の成す圏に類似の性質を持つ圏を基礎に置く方法である。

歴史

数理論理学は、19世紀の中頃、伝統的論理学とは独立な数学の下位分野として登場した（Ferreirós 2001, p. 443）。これが登場する以前、論理学は修辞学また哲学とともに、三段論法を通じて研究されていた。20世紀の前半は数学の基礎に関する活発な議論とともに、基本的な多くの結果が見られる。

初期の歴史

「論理学の歴史」も参照

論理に関する理論は多くの文化と歴史の中で発展してきた。その中には中国、インド、ギリシャ、(イスラーム世界)が含まれる。18世紀のヨーロッパでは、形式論理の演算子を記号的または代数的な方法の中で取り扱おうという試みが、哲学的数学者によってなされた。その中にはゴットフリート・ライプニッツとランベルトが含まれる。しかし彼らの仕事は孤立して残っているばかりでよく知られていない。

19世紀

19世紀中葉、ジョージ・ブールとそしてオーガスタス・ド・モルガンは体系的で数学的な論理の取り扱いを与えた。彼らの仕事は、(ジョージ・ピーコック)などの代数学者の仕事の上に打ち立てられたものであり、アリストテレスの伝統的論理学を数学基礎論の研究に十分な枠組みに拡張した（Katz 1998, p. 686）。

チャールズ・サンダース・パースはブールの研究の上に関係と量化子のための論理体系を作り上げた。彼の1870年から1885年に出版されたいくつかの論文において為された。

ゴットロープ・フレーゲは1879年に出版された彼の概念記法において、量化子を含む論理の独自の開発を提示した。この仕事は論理の歴史におけるターニングポイントを特徴づけるものであると一般に考えられている。フレーゲの仕事は、この世紀の変わり目にバートランド・ラッセルがそれを宣伝するまで、日の目を見なかった。フレーゲの2次元的な表記法は広くは受け入れられず同時代のテキストでも使用されていない。

1890年から1905年、(エルンスト・シュレーダー)は Vorlesungen über die Algebra der Logik を3つの巻に出版した。彼の仕事はブール、ド・モルガン、パースらの仕事をまとめ、拡張し、19世紀終わりに理解されていた記号論理学の包括的なリファレンスとなった。

基礎理論

数学が正確な基礎の上に築かれていなかったことへの不安が、算術、解析、幾何のような数学の基礎的な領域に対する公理系の開発をもたらした。

ロジックにおいて、算術は自然数の理論を意味する^{[注 3]}。ジュゼッペ・ペアノ（1889）は後に彼の名前で呼ばれることになった（ペアノの公理）算術の公理系を発表した。これはブールとシュレーダーの論理体系の変種を用いているが、量化記号が追加されている点で異なる。ペアノはこのときフレーゲの仕事を知らなかった。同時期にリヒャルト・デデキントは自然数の全体はそれらの帰納法の性質によって一意的に特徴づけられることを示した。デデキント（1888）は別の特徴付けを提案した。それはペアノの公理にあったような形式論理的な性格を欠いていた。しかしながらデデキントの仕事はペアノの公理においては到達できない定理を証明していた。それには自然数の集合の（同型を除いた）一意性と、加法と乗法の後者関数と数学的帰納法に基づく再帰的定義が含まれる。

19世紀中頃、ユークリッドの幾何学の公理の欠陥が世に知られるようになった (Katz 1998, p. 774)。1826年にニコライ・ロバチェフスキーによって確立された平行線公準の独立性 (Lobachevsky 1840) に加え、数学者達は、ユークリッドが明らかと考えていた幾つかの定理が、実際には彼の公理からは証明できないことを発見した。それらの中には、直線は少なくとも二点を含むという定理や、同じ半径を持ち中心が半径と同じ距離だけ離れている二つの円は交わらねばならないという定理がある。ヒルベルト (1899) は(パッシュの先行研究) (1882) のもとに、完全な(幾何学の公理)（英語版）の集合を開発した。幾何学の公理化の成功はヒルベルトに他の数学の分野（自然数や数直線など）の完全な公理化の探求するよう動機付けた。これが20世紀前半の主要な研究領域となることが分かる。

20世紀

20世紀の最初の10年における研究の主領域は集合論と形式論理であった。非形式的な集合論におけるパラドックスの発見は、数学それ自身が無矛盾であるのかを疑わせるものであり、無矛盾性の証明の必要に迫られた。

1900年、ダフィット・ヒルベルトはヒルベルトの23の問題の幾つかを次の世紀へと提出した。その最初の2つは連続体仮説の解決と初等算術（実数論）の無矛盾性の証明であった。第10番は整数上の多変数多項式からなる方程式（ディオファントス方程式）が解を持つかを決定する手続きを求めるものであった。これらの問題を解くための次なる仕事は、数理論理学の方向性を決定づけ、1928年に提出されたヒルベルトの(Entscheidungsproblem)（英語版）（決定問題）を解決する努力へと向かわせた。この問題は与えられた形式化された数学的言明について、それが真か偽かを決定する手続きを問うた。

集合論とパラドックス

エルンスト・ツェルメロ（1904）は任意の集合が整列可能であることの証明を与えた。この結果はゲオルク・カントールには得ることができなかったものである。ツェルメロはその証明を完成させるために選択公理を導入した。これは数学者と集合論の先駆者達の間の激しい論戦と研究を引き起こすことになる。即座に浴びた批判から、ツェルメロは自身の結果の第2の解説を出版した（Zermelo 1908a）。この論文は彼の証明に対する批判に直接対処するものであり、これによって数学界において選択公理が広く受け入れられることになった。

選択公理に関する疑念は最近の素朴集合論におけるパラドックスの発見により強化された。(チェザーレ・ブラリ・フォルティ)（1897）は集合論のパラドックスについて述べた最初の人である：ブラリ＝フォルティのパラドックスは全ての順序数からなる集まりが集合を成さないことを示す。その直後に、バートランド・ラッセルは1901年にラッセルのパラドックスを、ジュール・リシャール（1905）はリシャールのパラドックスを発見した。

ツェルメロ（1908b）は集合論に対する最初の公理化を与えた。それらの公理にアドルフ・フレンケルによる置換公理を加えたものは今日ではツェルメロ＝フレンケル集合論（ZF）の名で知られる。ツェルメロの公理にはラッセルのパラドックスを回避する為の(サイズの制限)の原理が組み込まれた。

1910年にアルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルによる プリンキピア・マテマティカ の第一巻が出版された。この重要な著作は、関数と基数に関する理論を型理論の完全に形式的な枠組みの中で展開した。型理論はパラドックスを回避するラッセルとホワイトヘッドの努力のもとに開発されたものである。型理論の枠組みは数学の基礎理論として普及しなかったけれども(Ferreirós 2001, p. 445)、プリンキピア・マテマティカ は20世紀の最も影響力のある研究のひとつと見做されている。

フレンケル(1922)は選択公理が(原子)（英語版）付きツェルメロ集合論の残りの公理からは証明できないことを証明した。後のポール・コーエン(1966)による仕事は、（その証明には）原子の追加が不要であって、選択公理はZFにおいて証明不可能であることを示した。コーエンの証明は強制法の手法を生み、今日では集合論における(独立性結果)（英語版）を確立する為の重要なツールとなっている^{[注 4]}。

記号論理

(レオポルト・レーヴェンハイム)（英語版）（1915）とトアルフ・スコーレム（1920）はレーヴェンハイム-スコーレムの定理を得た。これは一階述語論理は無限構造の濃度を制御できないことを述べる。スコーレムは、この定理を一階で形式化された集合論へ適用でき、そのいかなる形式化も可算モデルを持つことが導かれる、ということに気付いた。この直観に反する結果は(スコーレムのパラドックス)として知られることになった。

ゲーデルは自身の博士論文（1929）において完全性定理を示した。これは(一階論理)における構文論と意味論の間の対応を確立する。ゲーデルは完全性定理をコンパクト性定理の証明に用いた。これは一階の論理的帰結の有限性を立証する。これらの結果は一階論理を数学者にとって支配的な論理として確立することを助けた。

1931年、ゲーデルは(プリンキピア・マテマティカとそれに関連する体系において形式的に決定不可能な命題について)（英語版）を出版した。ここでは、十分に強く、実効的な一階理論が不完全（完全性定理のそれとは異なる意味である）であることを示されている。この結果はゲーデルの不完全性定理として知られ、数学の公理的基礎の厳密な限界を示すものであり、ヒルベルト・プログラムに大きな打撃を与えた。これは算術の無矛盾性をいかなる算術の形式理論においても証明できないことを示している。しかしながら、ヒルベルトは、不完全性定理の重要性を、あるときまで認めなかった。

ゲーデルの定理は、十分に強く、実効的な公理系の無矛盾性の証明は、それが無矛盾である限り、それ自身からも、それよりも弱い体系からも、得られないことを示す。これはいま考えている体系で形式化できないような無矛盾性証明の可能性については未解決のまま残す。ゲンツェン（1936）は算術の無矛盾性を超限帰納法の原理を持つ有限的な体系を用いて証明した。ゲンツェンの結果は(カット除去)と(証明論的順序数)の概念を生み出し、これらは証明論における主要な道具となった。ゲーデル（1958）は別の無矛盾性証明を与えた。これは古典算術の無矛盾性を高階直観主義算術の無矛盾性に還元することで為された。

他の分科の始まり

アルフレッド・タルスキはモデル理論の基礎を発展させた。

1935年初頭、著名な数学者らは網羅的な数学の教科書のシリーズを出版するためにニコラ・ブルバキというペンネームで集結した。これらの教科書は禁欲的かつ公理的に記述されており、厳格な記述と集合論的な基礎を強調した。これらの教科書から生まれた用語、例えば全単射、単射、全射や、教科書で採用された集合論的な基礎は、広く数学に採用された。

計算可能性の研究は再帰理論として知られるようになった。これはゲーデルとクリーネによる計算可能性の初期の定式化が関数の再帰的定義に基づいていたことによる^{[注 5]}。それらの定義がチューリングによるチューリング機械を用いた定式化と同値であることが示されたことで、計算可能関数という新しい概念が見出され、またこの定義が多数の独立な特徴付けを許すようなロバスト性を持つことが明らかになった。1931年の不完全性定理に関するゲーデルの仕事において、彼は実効的な形式的体系の厳格な概念（規定）を欠いていた。彼は計算可能性の新しい定義が不完全性定理の設定の一般化に使えることに気付いた。

再帰理論における多くの結果は1940年代にスティーヴン・コール・クリーネとエミール・ポストによって得られた。クリーネ（1943）は相対的計算可能性と算術的階層の概念を導入した。前者はチューリング（1939）で暗示されていたものである。クリーネは後に再帰理論を高階汎関数へ一般化した。クリーネとクライゼルは形式的な直観主義数学、とくに再帰理論の文脈でのそれを研究した。

形式論理体系

数理論理学の中心では形式論理体系を用いて表現された数学の概念を取り扱う。それらの体系は、多くの細部の差異はあるが、固定した形式言語で記述されるという共通の性質がある。命題論理と一階述語論理の体系は今日では最も広く研究されている。それは数学基礎論への応用可能性とそれらの望ましい証明論的な性質の故である^{[注 6]}。より強い古典論理、例えば二階述語論理や無限論理もまた直観主義論理とともに研究されている。

一階述語論理

詳細は「一階述語論理」を参照

一階論理は特定の(形式的体系)である。その(構文論)（証明論）は有限個の表現―構文的に正しい（well-formed）式だけからなるが、その意味論は量化子を固定された議論領域への制限として特徴付けられる。

形式論理の初期の結果は一階論理の限界を明らかにした。レーヴェンハイム＝スコーレムの定理（1919）は、可算な一階の言語における文の集合が無限モデルを持つならば、それは任意の濃度のモデルを少なくともひとつ持つことを示した。これは一階論理の公理系によって、自然数、実数ほか、いかなる無限構造も同型を除いて特徴づけることができないことを示している。初期の基礎論的研究の目標が数学の全部分の公理的理論を生み出すことであったから、この限界はとりわけ冷徹なものであった。

ゲーデルの完全性定理　(Gödel 1929)　は一階論理の論理的帰結に対する構文論的定義と意味論的定義の同値性を確立した。これは、もしある特定の文が、ある特定の公理の集合を満たすあらゆるモデルで真であるならば、それらの公理からその文への有限な演繹が存在することを示している。

他の古典論理

一階述語論理の他にも多くの論理体系が考えられている。それらのうちには無限の長さの証明や論理式を許す無限論理や、意味論に集合論の一部分を直接含むような高階述語論理も含まれる。

最もよく調べられている無限論理は ${\displaystyle L_{\omega _{1},\omega }}$  である。この論理においては、一階述語論理のように量化子の入れ子の深さは有限（つまり深さ ${\displaystyle \omega }$  未満）だけを許すが、論理式は有限または可算無限（つまり長さ ${\displaystyle \omega _{1}}$  未満）の連言や選言をその内に含むことを許す。すると、例えば、ある対象が自然数であるという性質を ${\displaystyle L_{\omega _{1},\omega }}$  の論理式によって次のように書ける：

${\displaystyle (x=0)\lor (x=1)\lor (x=2)\lor \cdots .}$ 

高階述語論理は議論領域の要素だけではなく議論領域の部分集合（述語）、議論領域の冪集合の部分集合（述語の述語）、さらに高階の対象に対する量化を許した論理である。その意味論は、それぞれの高階型の量化子に対して独立した議論領域を割り当てるよりは、量化子は適切な型の全ての対象に及ぶように定義される。現在の形の一階述語論理が開発される以前に研究されていた論理、例えばフレーゲの論理など、は集合論的な側面を持っていた。高階述語論理はより表現力が高く、自然数の構造の完全な公理化すら可能であるけれども、一階述語論理における完全性やコンパクト性定理に対応する性質を高階述語論理は持たない。また一階述語論理の持つ証明論的なよい性質の多くは高階述語論理では失われている。

他のタイプの論理としては(不動点論理)があり、これは原始帰納的関数の記述に使われるような帰納的定義を許す。

非古典論理と様相論理

様相論理は追加の様相演算子を含む論理である。様相演算子とは例えば必然的に真である、真である可能性があるといった意味を持つ演算子である。しかしながら、様相論理は大抵は数学の公理化のために使われることはなく、一階述語論理の証明可能性（Solovay 1976）や集合論的な強制法（Hamkins and Löwe 2007）の研究などに用いられる。

直観主義論理はブラウワーの直観主義(ブラウワー自身はその形式化を避けたが)のプログラムの研究からハイティングによって形式化・発展せられたものである。直観主義論理は排中律、すなわち任意の文が真または偽であるという原理を、明確に含まない論理である。クリーネの直観主義論理の証明論に関する仕事は、直観主義的な証明からは構成的な情報が復元できることを示している。例えば、直観主義的算術のいかなる証明可能全域関数も計算可能である。このことはペアノ算術のような算術の古典理論においては成立しない。

代数的論理学

(代数的論理学)は形式論理の意味論の研究に抽象代数学の手法を用いる。基本的な例としては、古典命題論理の真理値の表現にブール代数を用いたり、直観主義命題論理の真理値の表現にハイティング代数を用いたりすることが挙げられる。もっと強い論理、例えば一階述語論理や高階述語論理についても、(筒状代数)（英語版）のようなもっと複雑な代数的構造が用いられる。

集合論

詳細は「集合論」を参照

モデル理論

詳細は「モデル理論」を参照

モデル理論は様々な形式理論のモデルを研究する。ここで(理論)（英語版）とは特定の形式論理に於ける論理式と(シグネチャ)（英語版）からなる集まりで、(モデル)（英語版）とはその理論の具体的な解釈を与える構造である。モデル理論は普遍代数と代数幾何学に密接に関係しているが、モデル理論の手法は他の分野よりも論理的な考察に重きを置いている。

特定の理論の全てのモデルからなる集合は(初等クラス)と呼ばれる；古典モデル理論は特定の初等クラスの性質を決定しようとしたり、あるいは構造からなる或るクラスが初等クラスとなるか否かを決定しようとする。

(量化記号消去)の手法は特定の理論における定義可能集合がそこまで複雑ではないことを示すことに使える。タルスキ(1948)は実閉体の量化記号消去（これは実数体の理論が決定可能であることをも示す結果である）を確立した。（彼はまた自身の手法が任意の標数の代数閉体にもそのまま適用可能であることを指摘した。）ここから発展した現代的な副分野は(順序極小構造)（英語版）に関わる。

(マイケル・D・モーレイ)（英語版）（1965）によって証明された(モーレイの範疇性定理)（英語版）は、もし可算言語上の一階理論が或る非可算濃度について範疇的（つまりその濃度を持つ全てのモデルが同型）ならば、全ての非可算濃度で範疇的となることを述べる。

連続体仮説からの自明な帰結として、連続体濃度個未満の互いに非同型な可算モデルを持つような完全理論はそれ（非同型モデル）をちょうど可算個だけ持つこと、がある。(ロバート・ローソン・ヴォート)（英語版）に因む(ヴォート予想)（英語版）はこれが連続体仮説とは無関係に真であることを主張する。この予想は多くの特別なケースについて確立されている。

再帰理論

詳細は「再帰理論」を参照

再帰理論（計算可能性理論とも呼ばれる）は計算可能関数とチューリング次数（これは計算不可能関数を同じレベルの計算不可能性を持つ集合に分ける）の性質を研究する。再帰理論はまた一般計算可能性と定義可能性の研究を含む。再帰理論はアロンゾ・チャーチとアラン・チューリングによる1930年代の仕事（これはクリーネと(ポスト)によって1940年代に大きく拡張された）から生まれた。

古典再帰理論は自然数から自然数への関数の計算可能性に着目する。基本的な結果は、チューリング機械やラムダ計算やその他のシステムなど、多数の独立だが同値な特徴づけを持つ、ロバストかつカノニカルな計算可能関数のクラスを確立したことである。より高度な結果はチューリング次数の構造や帰納的可算集合の成す束に関するものである。

一般再帰理論は再帰理論の諸概念をもはや有限ではないような計算へと拡張する。そこには高階の型の計算可能性の研究や(超算術的理論)（英語版）や(アルファ再帰理論)（英語版）などの分野を同様に含む。

再帰理論の現代的研究には、純粋な再帰理論の新しい結果と同様に、その応用研究（例えばアルゴリズム的ランダムネス、(計算可能モデル理論)（英語版）、逆数学など）が含まれる。

アルゴリズム的に非可解な問題

再帰理論の重要な部分領域ではアルゴリズム的に非可解な問題が研究される；決定問題または関数問題がアルゴリズム的に非可解（英: algorithmically unsolvable）あるいは決定不可能（英: undecidable）とは、任意の合法な入力に対して正しい解を返すような計算可能なアルゴリズムが存在しないことをいう。決定不可能性に関する最初の結果は、1936年にチャーチとチューリングによって独立に得られたもので、(一階述語論理の決定問題)がアルゴリズム的に非可解であるというものである。チュ―リングはこれを停止性問題の決定不可能性を示すことによって証明した。この結果は再帰理論と計算機科学の双方に広範な示唆を与えるものである。

通常の数学においても多くの決定不可能問題の例が知られている。(群の語の問題)は1955年の(ピョートル・ノビコフ)と1959年のW.ボーンによって独立に証明せられた。ビジービーバー問題は1962年に(Tibor Radó)によって与えられた別のよく知られた例である。

(ヒルベルトの第10問題)は多変数整数係数代数方程式（ディオファントス方程式）が整数解を持つか否かを決定するアルゴリズムの存在を問うものである。部分的な解答はジュリア・ロビンソン、(マーティン・デイビス)、ヒラリー・パトナムらによって与えられた。この問題のアルゴリズム的非可解性はユーリ・マチャセヴィッチによって1970年に証明された（Davis 1973）。

証明論と構成的数学

詳細は「証明論」を参照

証明論は様々な論理推論体系における形式的証明の研究である。それら形式的証明は形式的な数学的対象であるから、それらの解析は数学的手法を用いて行うことができる。(ヒルベルト流の体系)、自然演繹の体系、ゲンツェンによって開発されたシークエント計算などを含む、いくつかの推論体系はよく考察される

数理論理学の文脈において、構成的数学の研究は、(可述的)体系の研究のような、非古典論理の体系の研究を含む。可述主義の初期の支持者はヘルマン・ワイルである。彼は実解析の大部分を可述的な方法だけを用いて展開できることを示した（Weyl 1918）。

形式的証明は完全に有限的なものであるが、構造における真理性はそうでないことから、構成的数学での作業では証明可能性を強調することが多い。古典（または非構成的）体系における証明可能性と直観主義（または構成的）体系での証明可能性との間の関係はとりわけ関心が持たれる。(ゲーデル・ゲンツェン変換)のような結果は古典論理を直観主義論理に埋め込む（翻訳する）ことが可能であることを示している。直観主義的証明に関するある性質は古典論理の証明に関するそれに逆翻訳できる。

最近の証明論における発展には(Ulrich Kohlenbach)による(proof mining)の研究や(Michael Rathjen)による(証明論的順序数)の研究が含まれる。

計算機科学との関係

(計算機科学における計算可能性理論)の研究は数理論理学における計算可能性の研究と密接に関係している。ただしその重視されている点に違いがある。計算機科学者はしばしば具体的なプログラミング言語と(実際的計算可能性)に焦点を当てるが、数理論理学における研究者達は理論的な概念としての計算可能性と計算不可能性に焦点を当てる。

プログラミング言語の意味論の理論はプログラム検証（とくにモデル検査）などモデル理論に関係する。証明とプログラムの間のカリー・ハワード対応は証明論のとくに直観主義論理に関係する。ラムダ計算やコンビネータ論理のような形式計算は理想化されたプログラミング言語として研究される。

計算機科学はまた自動定理証明や論理プログラミングのような自動検証や証明探索の技術の開発によって数学に寄与している。

記述計算量理論は論理と計算量を関係づける。この領域での最初の重要な結果である(フェイギンの定理)（1974）はNPがexistencialな二階述語論理の論理式で表現可能な言語の成す集合とちょうど一致することを示す。

数学基礎論

詳細は「数学基礎論」を参照

関連項目

• 計算可能性理論
• 再帰理論
• 集合論
• 証明論
• 数学基礎論
• 非古典論理
• モデル理論
• 計算言語学

脚注

注釈

1. ^ 以下、『岩波　数学入門辞典』からの引用^[3]。

   数理論理学
   　mathematical logic
   

   　数学の理論を展開する際にその骨格となる論理の構造を研究する分野をいう．数学基礎論とほぼ同義である．^[3]

2. ^ 以下、『岩波　数学入門辞典』からの引用^[4]。

   数学基礎論
   　foundations of mathematics
   

   　数理論理学や超数学とほぼ同じ意味で，論理を扱う数学の一分野である． … ゲーデルの不完全性定理は有限の立場（形式主義）で数学の無矛盾性を証明することはできないことを示した．ゲンツェン（Gentzen）は，有限の立場より緩い制限のもとで自然数論の無矛盾性を証明した．
   　数学基礎論は計算機科学〔コンピュータ科学〕とも密接に結びついている．^[4]

3. ^ これに反して(ヒルベルトの第2問題)における「算術」は実数論のことであって自然数論のことではない。
4. ^ See also Cohen 2008.
5. ^ この用語に関する詳しいサーベイはSoare （1996）による。
6. ^ Ferreirós (2001) surveys the rise of first-order logic over other formal logics in the early 20th century.

出典

1. ^ ^{a b} 『日本大百科全書』
2. ^ ^{a b} 『世界大百科事典 第２版』
3. ^ ^{a b c d} 青本 et al. 2005, p. 297.
4. ^ ^{a b c d e} 青本 et al. 2005, p. 294.
5. ^ Undergraduate texts include Boolos, Burgess, and Jeffrey (2002), (Enderton) (2001), and Mendelson (1997). A classic graduate text by Shoenfield (2001) first appeared in 1967.

参考文献

学部教科書

• 青本和彦（編）; 上野健爾（編）; 加藤和也（編）; 神保道夫（編）; 砂田利一（編）; 高橋陽一郎（編）; 深谷賢治（編）; 俣野博（編） ほか『岩波　数学入門辞典』（第1刷）岩波書店、2005年9月29日。ISBN (978-4000802093)。 
• Walicki, Michał (2011), Introduction to Mathematical Logic, Singapore: (World Scientific Publishing), ISBN (978-981-4343-87-9) .
• Boolos, George; Burgess, John; Jeffrey, Richard (2002), Computability and Logic (4th ed.), Cambridge: Cambridge University Press, ISBN (978-0-521-00758-0) .
• Crossley, J.N.; Ash, C.J.; Brickhill, C.J.; Stillwell, J.C.; Williams, N.H. (1972), What is mathematical logic?, London-Oxford-New York: Oxford University Press, ISBN (0-19-888087-1), Zbl 0251.02001 .
• Enderton, Herbert (2001), A mathematical introduction to logic (2nd ed.), Boston, MA: (Academic Press), ISBN (978-0-12-238452-3) .
• Hamilton, A.G. (1988), Logic for Mathematicians (2nd ed.), Cambridge: Cambridge University Press, ISBN (978-0-521-36865-0) .
• Ebbinghaus, H.-D.; Flum, J.; Thomas, W. (1994), Mathematical Logic (2nd ed.), New York: , ISBN (0-387-94258-0), http://www.springer.com/mathematics/book/978-0-387-94258-2 .
• Katz, Robert (1964), Axiomatic Analysis, Boston, MA: (D. C. Heath and Company) .
• Mendelson, Elliott (1997), Introduction to Mathematical Logic (4th ed.), London: (Chapman & Hall), ISBN (978-0-412-80830-2) .
• (Rautenberg, Wolfgang) (2010), A Concise Introduction to Mathematical Logic (3rd ed.), New York: , doi:10.1007/978-1-4419-1221-3, ISBN (978-1-4419-1220-6), http://www.springerlink.com/content/978-1-4419-1220-6/ .
• Schwichtenberg, Helmut (2003–2004), Mathematical Logic, Munich, Germany: Mathematisches Institut der Universität München, http://www.mathematik.uni-muenchen.de/~schwicht/lectures/logic/ws03/ml.pdf .
• Shawn Hedman, A first course in logic: an introduction to model theory, proof theory, computability, and complexity, Oxford University Press, 2004, (ISBN 0-19-852981-3). Covers logics in close relation with (computability theory) and (complexity theory)

大学院教科書

• Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (2nd ed.), Boston: Kluwer Academic Publishers, ISBN (978-1-4020-0763-7) .
• Barwise, Jon, ed. (1989), Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, North Holland, ISBN (978-0-444-86388-1) .
• (Hodges, Wilfrid) (1997), A shorter model theory, Cambridge: Cambridge University Press, ISBN (978-0-521-58713-6) .
• Jech, Thomas (2003), Set Theory: Millennium Edition, Springer Monographs in Mathematics, Berlin, New York: Springer-Verlag, ISBN (978-3-540-44085-7) .
• Shoenfield, Joseph R. (2001) [1967], Mathematical Logic (2nd ed.), (A K Peters), ISBN (978-1-56881-135-2) .
• Troelstra, Anne Sjerp; Schwichtenberg, Helmut (2000), Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science (2nd ed.), Cambridge: Cambridge University Press, ISBN (978-0-521-77911-1) .

研究論文、モノグラフ、教科書、サーベイ

• Cohen, P. J. (1966), Set Theory and the Continuum Hypothesis, Menlo Park, CA: W. A. Benjamin .
• (Cohen, Paul Joseph) (2008) [1966]. Set theory and the continuum hypothesis. Mineola, New York: Dover Publications. ISBN (978-0-486-46921-8) .
• (Davis, Martin) (1973), “Hilbert's tenth problem is unsolvable”, (The American Mathematical Monthly) (The American Mathematical Monthly, Vol. 80, No. 3) 80 (3): 233–269, doi:10.2307/2318447, JSTOR 2318447, https://jstor.org/stable/2318447 , reprinted as an appendix in Martin Davis, Computability and Unsolvability, Dover reprint 1982. JStor
• Felscher, Walter (2000), “Bolzano, Cauchy, Epsilon, Delta”, The American Mathematical Monthly (The American Mathematical Monthly, Vol. 107, No. 9) 107 (9): 844–862, doi:10.2307/2695743, JSTOR 2695743, https://jstor.org/stable/2695743 . JSTOR
• Ferreirós, José (2001), “The Road to Modern Logic-An Interpretation”, Bulletin of Symbolic Logic (The Bulletin of Symbolic Logic, Vol. 7, No. 4) 7 (4): 441–484, doi:10.2307/2687794, JSTOR 2687794, https://jstor.org/stable/2687794 . JStor
• Hamkins, Joel David; (Benedikt Löwe), “The modal logic of forcing”, Transactions of the American Mathematical Society , to appear. Electronic posting by the journal
• Katz, Victor J. (1998), A History of Mathematics, Addison–Wesley, ISBN (0-321-01618-1) .
• (Morley, Michael) (1965), “Categoricity in Power”, (Transactions of the American Mathematical Society) (Transactions of the American Mathematical Society, Vol. 114, No. 2) 114 (2): 514–538, doi:10.2307/1994188, JSTOR 1994188, https://jstor.org/stable/1994188 .
• Soare, Robert I. (1996), “Computability and recursion”, Bulletin of Symbolic Logic (The Bulletin of Symbolic Logic, Vol. 2, No. 3) 2 (3): 284–321, doi:10.2307/420992, JSTOR 420992, https://jstor.org/stable/420992 .
• (Solovay, Robert M.) (1976), “Provability Interpretations of Modal Logic”, Israel Journal of Mathematics 25 (3–4): 287–304, doi:10.1007/BF02757006 .
• Woodin, W. Hugh (2001), “The Continuum Hypothesis, Part I”, Notices of the American Mathematical Society 48 (6) . PDF

古典的な論文、教科書、論文集

• Burali-Forti, Cesare (1897), A question on transfinite numbers , reprinted in van Heijenoort 1976, pp. 104–111.
• Dedekind, Richard (1872), Stetigkeit und irrationale Zahlen . English translation of title: "Consistency and irrational numbers".
• Dedekind, Richard (1888), Was sind und was sollen die Zahlen?  Two English translations:
  • 1963 (1901). Essays on the Theory of Numbers. Beman, W. W., ed. and trans. Dover.
  • 1996. In From Kant to Hilbert: A Source Book in the Foundations of Mathematics, 2 vols, Ewald, William B., ed., Oxford University Press: 787–832.
• Fraenkel, Abraham A. (1922), “Der Begriff 'definit' und die Unabhängigkeit des Auswahlsaxioms”, Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-mathematische Klasse, pp. 253–257  (German), reprinted in English translation as "The notion of 'definite' and the independence of the axiom of choice", van Heijenoort 1976, pp. 284–289.

• Frege Gottlob (1879), (Begriffsschrift), eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle a. S.: Louis Nebert. Translation: Concept Script, a formal language of pure thought modelled upon that of arithmetic, by S. Bauer-Mengelberg in (Jean Van Heijenoort), ed., 1967. From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. Harvard University Press.
• Frege Gottlob (1884), Die Grundlagen der Arithmetik: eine logisch-mathematische Untersuchung über den Begriff der Zahl. Breslau: W. Koebner. Translation: (J. L. Austin), 1974. The Foundations of Arithmetic: A logico-mathematical enquiry into the concept of number, 2nd ed. Blackwell.
• (Gentzen, Gerhard) (1936), “Die Widerspruchsfreiheit der reinen Zahlentheorie”, Mathematische Annalen 112: 132–213, doi:10.1007/BF01565428 , reprinted in English translation in Gentzen's Collected works, M. E. Szabo, ed., North-Holland, Amsterdam, 1969.(Template:Specify)
• Gödel, Kurt (1929), Über die Vollständigkeit des Logikkalküls, doctoral dissertation, University Of Vienna . English translation of title: "Completeness of the logical calculus".
• Gödel, Kurt (1930), “Die Vollständigkeit der Axiome des logischen Funktionen-kalküls”, Monatshefte für Mathematik und Physik 37: 349–360, doi:10.1007/BF01696781 . English translation of title: "The completeness of the axioms of the calculus of logical functions".
• Gödel, Kurt (1931), “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”, Monatshefte für Mathematik und Physik 38 (1): 173–198, doi:10.1007/BF01700692 , see (On Formally Undecidable Propositions of Principia Mathematica and Related Systems) for details on English translations.
• Gödel, Kurt (1958), “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes”, Dialectica. International Journal of Philosophy 12 (3–4): 280–287, doi:10.1111/j.1746-8361.1958.tb01464.x , reprinted in English translation in Gödel's Collected Works, vol II, Soloman Feferman et al., eds. Oxford University Press, 1990.(Template:Specify)
• (van Heijenoort, Jean), ed. (1967, 1976 3rd printing with corrections), From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (3rd ed.), Cambridge, Mass: Harvard University Press, ISBN (0-674-32449-8), (pbk.) 
• Hilbert, David (1899), Grundlagen der Geometrie, Leipzig: Teubner , English 1902 edition (The Foundations of Geometry) republished 1980, Open Court, Chicago.
• David, Hilbert (1929), “Probleme der Grundlegung der Mathematik”, Mathematische Annalen 102: 1–9, doi:10.1007/BF01782335, http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=GDZPPN002273500&L=1 . Lecture given at the International Congress of Mathematicians, 3 September 1928. Published in English translation as "The Grounding of Elementary Number Theory", in Mancosu 1998, pp. 266–273.
• Kleene, Stephen Cole (1943), “Recursive Predicates and Quantifiers”, American Mathematical Society Transactions (Transactions of the American Mathematical Society, Vol. 53, No. 1) 54 (1): 41–73, doi:10.2307/1990131, JSTOR 1990131, https://jstor.org/stable/1990131 .
• (Lobachevsky, Nikolai) (1840), Geometrishe Untersuchungen zur Theorie der Parellellinien  (German). Reprinted in English translation as "Geometric Investigations on the Theory of Parallel Lines" in Non-Euclidean Geometry, Robert Bonola (ed.), Dover, 1955. (ISBN 0-486-60027-0)
• Löwenheim, Leopold (1915), “Über Möglichkeiten im Relativkalkül”, Mathematische Annalen 76 (4): 447–470, doi:10.1007/BF01458217, ISSN 0025-5831, http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=GDZPPN002266121&L=1  (German). Translated as "On possibilities in the calculus of relatives" in (Jean van Heijenoort), 1967. A Source Book in Mathematical Logic, 1879–1931. Harvard Univ. Press: 228–251.
• (Mancosu, Paolo), ed. (1998), From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford: Oxford University Press .
• Pasch, Moritz (1882), Vorlesungen über neuere Geometrie .
• Peano, Giuseppe (1889), (Arithmetices principia, nova methodo exposita)  (Latin), excerpt reprinted in English stranslation as "The principles of arithmetic, presented by a new method", van Heijenoort 1976, pp. 83 97.
• Richard, Jules (1905), “Les principes des mathématiques et le problème des ensembles”, Revue générale des sciences pures et appliquées 16: 541  (French), reprinted in English translation as "The principles of mathematics and the problems of sets", van Heijenoort 1976, pp. 142–144.
• (Skolem, Thoralf) (1920), “Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen”, Videnskapsselskapet Skrifter, I. Matematisk-naturvidenskabelig Klasse 6: 1–36 .
• Tarski, Alfred (1948), A decision method for elementary algebra and geometry, Santa Monica, California: (RAND Corporation) 
• (Turing, Alan M.) (1939), “Systems of Logic Based on Ordinals”, (Proceedings of the London Mathematical Society) 45 (2): 161–228, doi:10.1112/plms/s2-45.1.161 
• Zermelo, Ernst (1904), “Beweis, daß jede Menge wohlgeordnet werden kann”, Mathematische Annalen 59 (4): 514–516, doi:10.1007/BF01445300, http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=GDZPPN002260018&L=1  (German), reprinted in English translation as "Proof that every set can be well-ordered", van Heijenoort 1976, pp. 139–141.
• Zermelo, Ernst (1908a), “Neuer Beweis für die Möglichkeit einer Wohlordnung”, Mathematische Annalen 65: 107–128, doi:10.1007/BF01450054, ISSN 0025-5831, http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=GDZPPN002261952&L=1  (German), reprinted in English translation as "A new proof of the possibility of a well-ordering", van Heijenoort 1976, pp. 183–198.
• Zermelo, Ernst (1908b), “Untersuchungen über die Grundlagen der Mengenlehre”, Mathematische Annalen 65 (2): 261–281, doi:10.1007/BF01449999, http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=PPN235181684_0065&DMDID=DMDLOG_0018&L=1 .

外部リンク

• Hazewinkel, Michiel, ed. (2001), "Mathematical logic", Encyclopaedia of Mathematics, Springer, ISBN 978-1-55608-010-4。（英語）
• Polyvalued logic and Quantity Relation Logic（英語）
• forall x: an introduction to formal logic（英語）, a free textbook by P. D. Magnus.
• A Problem Course in Mathematical Logic（英語）, a free textbook by Stefan Bilaniuk.
• Detlovs, Vilnis, and Podnieks, Karlis (University of Latvia), Introduction to Mathematical Logic.（英語） (hyper-textbook).
• In the Stanford Encyclopedia of Philosophy:

  Classical Logic（英語） by (Stewart Shapiro).

  First-order Model Theory（英語） by (Wilfrid Hodges).

• In the London Philosophy Study Guide^[]:

  Mathematical Logic^[]

  Set Theory & Further Logic^[]

  Philosophy of Mathematics^[]