数理論理学

数理論理学（すうりろんりがく、英 : mathematical logic）または現代論理学、記号論理学、数学基礎論、超数学は、数学の分野の一つであり、「数学の理論を展開する際にその骨格となる論理の構造を研究する分野」を指す。数理論理学（数学基礎論）と密接に関連している分野としてはコンピュータ科学（計算機科学）や理論コンピュータ科学（理論計算機科学）などがある。
数理論理学の主な目的は形式論理の数学への応用の探求や数学的な解析などであり、共通課題としては形式的体系の表現力や形式証明系の演繹の能力の研究が含まれる。
数理論理学はしばしば集合論、モデル理論、再帰理論、証明論の4つの領域に分類される。これらの領域はロジックのとくに一階述語論理や定義可能性に関する結果を共有している。計算機科学（とくにに現れるもの）における数理論理学の役割の詳細はこの記事には含まれていない。詳細はを参照。
この分野が始まって以来、数理論理学は数学基礎論の研究に貢献し、また逆に動機付けられてきた。数学基礎論は幾何学、代数学、解析学に対する公理的枠組みの開発とともに19世紀末に始まった。20世紀初頭、数学基礎論は、ヒルベルトのプログラムによって、数学の基礎理論の無矛盾性を証明するものとして形成された。クルト・ゲーデルとゲルハルト・ゲンツェンによる結果やその他は、プログラムの部分的な解決を提供しつつ、無矛盾性の証明に伴う問題点を明らかにした。集合論における仕事は殆ど全ての通常の数学を集合の言葉で形式化できることを示した。しかしながら、集合論に共通の公理からは証明することができない幾つかの命題が存在することも知られた。むしろ現代の数学基礎論では、全ての数学を展開できる公理系を見つけるよりも、数学の一部がどのような特定の形式的体系で形式化することが可能であるか（逆数学のように）ということに焦点を当てている。
下位分野.
"Handbook of Mathematical Logic" は数理論理学を大まかに次の4つの領域に分類している：
それぞれの領域は異なる焦点を持っているものの、多くの技法や結果はそれら複数の領域の間で共有されている。これらの領域を分かつ境界線や、数理論理学と他の数学の分野とを分かつ境界線は、必ずしも明確ではない。ゲーデルの不完全性定理は再帰理論と証明論のマイルストーンであるだけではなく、様相論理におけるを導く。強制法の手法は集合論、モデル理論、再帰理論のほか直観主義的数学の研究などでも用いられる。
圏論の分野では多くの形式公理的方法を用いる。それにはの研究も含まれる。しかし圏論は普通は数理論理学の下位分野とは見做されない。圏論の応用性は多様な数学の分野に亙っているため、ソーンダース・マックレーンを含む数学者らは、集合論とは独立な数学のための基礎体系としての圏論を提案している。これはトポスと呼ばれる古典または非古典論理に基づく集合論の成す圏に類似の性質を持つ圏を基礎に置く方法である。
歴史.
数理論理学は、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世紀終わりに理解されていた記号論理学の包括的なリファレンスとなった。
基礎理論.
数学が正確な基礎の上に築かれていなかったことへの不安が、算術、解析、幾何のような数学の基礎的な領域に対する公理系の開発をもたらした。
ロジックにおいて、"算術"は自然数の理論を意味する。ジュゼッペ・ペアノ（1889）は後に彼の名前で呼ばれることになった（ペアノの公理）算術の公理系を発表した。これはブールとシュレーダーの論理体系の変種を用いているが、量化記号が追加されている点で異なる。ペアノはこのときフレーゲの仕事を知らなかった。同時期にリヒャルト・デデキントは自然数の全体はそれらの帰納法の性質によって一意的に特徴づけられることを示した。デデキント（1888）は別の特徴付けを提案した。それはペアノの公理にあったような形式論理的な性格を欠いていた。しかしながらデデキントの仕事はペアノの公理においては到達できない定理を証明していた。それには自然数の集合の（同型を除いた）一意性と、加法と乗法の後者関数と数学的帰納法に基づく再帰的定義が含まれる。
19世紀中頃、ユークリッドの幾何学の公理の欠陥が世に知られるようになった (Katz 1998, p. 774)。1826年にニコライ・ロバチェフスキーによって確立された平行線公準の独立性 (Lobachevsky 1840) に加え、数学者達は、ユークリッドが明らかと考えていた幾つかの定理が、実際には彼の公理からは証明できないことを発見した。それらの中には、直線は少なくとも二点を含むという定理や、同じ半径を持ち中心が半径と同じ距離だけ離れている二つの円は交わらねばならないという定理がある。ヒルベルト (1899) はパッシュの先行研究 (1882) のもとに、完全なの集合を開発した。幾何学の公理化の成功はヒルベルトに他の数学の分野（自然数や数直線など）の完全な公理化を探求するよう動機付けた。これが20世紀前半の主要な研究領域となることが分かる。
20世紀.
20世紀の最初の10年における研究の主領域は集合論と形式論理であった。非形式的な集合論におけるパラドックスの発見は、数学それ自身が無矛盾であるのかを疑わせるものであり、無矛盾性の証明の必要に迫られた。
1900年、ダフィット・ヒルベルトはヒルベルトの23の問題の幾つかを次の世紀へと提出した。その最初の2つは連続体仮説の解決と初等算術（実数論）の無矛盾性の証明であった。第10番は整数上の多変数多項式からなる方程式（ディオファントス方程式）が解を持つかを決定する手続きを求めるものであった。これらの問題を解くための次なる仕事は、数理論理学の方向性を決定づけ、1928年に提出されたヒルベルトの（決定問題）を解決する努力へと向かわせた。この問題は与えられた形式化された数学的言明について、それが真か偽かを決定する手続きを問うた。
集合論とパラドックス.
エルンスト・ツェルメロ（1904）は任意の集合が整列可能であることの証明を与えた。この結果はゲオルク・カントールには得ることができなかったものである。ツェルメロはその証明を完成させるために選択公理を導入した。これは数学者と集合論の先駆者達の間の激しい論戦と研究を引き起こすことになる。即座に浴びた批判から、ツェルメロは自身の結果の第2の解説を出版した（Zermelo 1908a）。この論文は彼の証明に対する批判に直接対処するものであり、これによって数学界において選択公理が広く受け入れられることになった。
選択公理に関する疑念は最近の素朴集合論におけるパラドックスの発見により強化された。チェザーレ・ブラリ・フォルティ（1897）は集合論のパラドックスについて述べた最初の人である：ブラリ＝フォルティのパラドックスは全ての順序数からなる集まりが集合を成さないことを示す。その直後に、バートランド・ラッセルは1901年にラッセルのパラドックスを、ジュール・リシャール（1905）はリシャールのパラドックスを発見した。
ツェルメロ（1908b）は集合論に対する最初の公理化を与えた。それらの公理にアドルフ・フレンケルによる置換公理を加えたものは今日ではツェルメロ＝フレンケル集合論（ZF）の名で知られる。ツェルメロの公理にはラッセルのパラドックスを回避する為のサイズの制限の原理が組み込まれた。
1910年にアルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルによる "プリンキピア・マテマティカ" の第一巻が出版された。この重要な著作は、関数と基数に関する理論を型理論の完全に形式的な枠組みの中で展開した。型理論はパラドックスを回避するラッセルとホワイトヘッドの努力のもとに開発されたものである。型理論の枠組みは数学の基礎理論として普及しなかったけれども(Ferreirós 2001, p. 445)、"プリンキピア・マテマティカ" は20世紀の最も影響力のある研究のひとつと見做されている。
フレンケル(1922)は選択公理が付きツェルメロ集合論の残りの公理からは証明できないことを証明した。後のポール・コーエン(1966)による仕事は、（その証明には）原子の追加が不要であって、選択公理はZFにおいて証明不可能であることを示した。コーエンの証明は強制法の手法を生み、今日では集合論におけるを確立する為の重要なツールとなっている。
記号論理.
（1915）とトアルフ・スコーレム（1920）はレーヴェンハイム-スコーレムの定理を得た。これは一階述語論理は無限構造の濃度を制御できないことを述べる。スコーレムは、この定理を一階で形式化された集合論へ適用でき、そのいかなる形式化も可算モデルを持つことが導かれる、ということに気付いた。この直観に反する結果はスコーレムのパラドックスとして知られることになった。
ゲーデルは自身の博士論文（1929）において完全性定理を示した。これは一階論理における構文論と意味論の間の対応を確立する。ゲーデルは完全性定理をコンパクト性定理の証明に用いた。これは一階の論理的帰結の有限性を立証する。これらの結果は一階論理を数学者にとって支配的な論理として確立することを助けた。
1931年、ゲーデルは""を出版した。ここでは、十分に強く、実効的な一階理論が不完全（完全性定理のそれとは異なる意味である）であることを示されている。この結果はゲーデルの不完全性定理として知られ、数学の公理的基礎の厳密な限界を示すものであり、ヒルベルト・プログラムに大きな打撃を与えた。これは算術の無矛盾性をいかなる算術の形式理論においても証明できないことを示している。しかしながら、ヒルベルトは、不完全性定理の重要性を、あるときまで認めなかった。
ゲーデルの定理は、十分に強く、実効的な公理系の無矛盾性の証明は、それが無矛盾である限り、それ自身からも、それよりも弱い体系からも、得られないことを示す。これはいま考えている体系で形式化できないような無矛盾性証明の可能性については未解決のまま残す。ゲンツェン（1936）は算術の無矛盾性を超限帰納法の原理を持つ有限的な体系を用いて証明した。ゲンツェンの結果はカット除去と証明論的順序数の概念を生み出し、これらは証明論における主要な道具となった。ゲーデル（1958）は別の無矛盾性証明を与えた。これは古典算術の無矛盾性を高階直観主義算術の無矛盾性に還元することで為された。
他の分科の始まり.
アルフレッド・タルスキはモデル理論の基礎を発展させた。
1935年初頭、著名な数学者らは網羅的な数学の教科書のシリーズを出版するためにニコラ・ブルバキというペンネームで集結した。これらの教科書は禁欲的かつ公理的に記述されており、厳格な記述と集合論的な基礎を強調した。これらの教科書から生まれた用語、例えば全単射、単射、全射や、教科書で採用された集合論的な基礎は、広く数学に採用された。
計算可能性の研究は再帰理論として知られるようになった。これはゲーデルとクリーネによる計算可能性の初期の定式化が関数の再帰的定義に基づいていたことによる。それらの定義がチューリングによるチューリング機械を用いた定式化と同値であることが示されたことで、計算可能関数という新しい概念が見出され、またこの定義が多数の独立な特徴付けを許すようなロバスト性を持つことが明らかになった。1931年の不完全性定理に関するゲーデルの仕事において、彼は実効的な形式的体系の厳格な概念（規定）を欠いていた。彼は計算可能性の新しい定義が不完全性定理の設定の一般化に使えることに気付いた。
再帰理論における多くの結果は1940年代にスティーヴン・コール・クリーネとエミール・ポストによって得られた。クリーネ（1943）は相対的計算可能性と算術的階層の概念を導入した。前者はチューリング（1939）で暗示されていたものである。クリーネは後に再帰理論を高階汎関数へ一般化した。クリーネとクライゼルは形式的な直観主義数学、とくに再帰理論の文脈でのそれを研究した。
形式論理体系.
数理論理学の中心では形式論理体系を用いて表現された数学の概念を取り扱う。それらの体系は、多くの細部の差異はあるが、固定した形式言語で記述されるという共通の性質がある。命題論理と一階述語論理の体系は今日では最も広く研究されている。それは数学基礎論への応用可能性とそれらの望ましい証明論的な性質の故である。より強い古典論理、例えば二階述語論理や無限論理もまた直観主義論理とともに研究されている。
一階述語論理.
一階論理は特定の形式的体系である。その構文論（証明論）は有限個の表現―構文的に正しい（well-formed）式だけからなるが、その意味論は量化子を固定された議論領域への制限として特徴付けられる。
形式論理の初期の結果は一階論理の限界を明らかにした。レーヴェンハイム＝スコーレムの定理（1919）は、可算な一階の言語における文の集合が無限モデルを持つならば、それは任意の濃度のモデルを少なくともひとつ持つことを示した。これは一階論理の公理系によって、自然数、実数ほか、いかなる無限構造も同型を除いて特徴づけることができないことを示している。初期の基礎論的研究の目標が数学の全部分の公理的理論を生み出すことであったから、この限界はとりわけ冷徹なものであった。
ゲーデルの完全性定理　(Gödel 1929)　は一階論理の論理的帰結に対する構文論的定義と意味論的定義の同値性を確立した。これは、もしある特定の文が、ある特定の公理の集合を満たすあらゆるモデルで真であるならば、それらの公理からその文への有限な演繹が存在することを示している。
他の古典論理.
一階述語論理の他にも多くの論理体系が考えられている。それらのうちには無限の長さの証明や論理式を許す無限論理や、意味論に集合論の一部分を直接含むような高階述語論理も含まれる。
最もよく調べられている無限論理は formula_1 である。この論理においては、一階述語論理のように量化子の入れ子の深さは有限（つまり深さ formula_2 未満）だけを許すが、論理式は有限または可算無限（つまり長さ formula_3 未満）の連言や選言をその内に含むことを許す。すると、例えば、ある対象が自然数であるという性質を formula_1 の論理式によって次のように書ける：
高階述語論理は議論領域の要素だけではなく議論領域の部分集合（述語）、議論領域の冪集合の部分集合（述語の述語）、さらに高階の対象に対する量化を許した論理である。その意味論は、それぞれの高階型の量化子に対して独立した議論領域を割り当てるよりは、量化子は適切な型の全ての対象に及ぶように定義される。現在の形の一階述語論理が開発される以前に研究されていた論理、例えばフレーゲの論理など、は集合論的な側面を持っていた。高階述語論理はより表現力が高く、自然数の構造の完全な公理化すら可能であるけれども、一階述語論理における完全性やコンパクト性定理に対応する性質を高階述語論理は持たない。また一階述語論理の持つ証明論的なよい性質の多くは高階述語論理では失われている。
他のタイプの論理としては不動点論理があり、これは原始帰納的関数の記述に使われるような帰納的定義を許す。
非古典論理と様相論理.
様相論理は追加の様相演算子を含む論理である。様相演算子とは例えば必然的に真である、真である可能性があるといった意味を持つ演算子である。しかしながら、様相論理は大抵は数学の公理化のために使われることはなく、一階述語論理の証明可能性（Solovay 1976）や集合論的な強制法（Hamkins and Löwe 2007）の研究などに用いられる。
直観主義論理はブラウワーの直観主義(ブラウワー自身はその形式化を避けたが)のプログラムの研究からハイティングによって形式化・発展せられたものである。直観主義論理は排中律、すなわち任意の文が真または偽であるという原理を、明確に含まない論理である。クリーネの直観主義論理の証明論に関する仕事は、直観主義的な証明からは構成的な情報が復元できることを示している。例えば、直観主義的算術のいかなる証明可能全域関数も計算可能である。このことはペアノ算術のような算術の古典理論においては成立しない。
代数的論理学.
代数的論理学は形式論理の意味論の研究に抽象代数学の手法を用いる。基本的な例としては、古典命題論理の真理値の表現にブール代数を用いたり、直観主義命題論理の真理値の表現にハイティング代数を用いたりすることが挙げられる。もっと強い論理、例えば一階述語論理や高階述語論理についても、のようなもっと複雑な代数的構造が用いられる。
モデル理論.
モデル理論は様々な形式理論のモデルを研究する。ここでとは特定の形式論理に於ける論理式とからなる集まりで、とはその理論の具体的な解釈を与える構造である。モデル理論は普遍代数と代数幾何学に密接に関係しているが、モデル理論の手法は他の分野よりも論理的な考察に重きを置いている。
特定の理論の全てのモデルからなる集合は初等クラスと呼ばれる；古典モデル理論は特定の初等クラスの性質を決定しようとしたり、あるいは構造からなる或るクラスが初等クラスとなるか否かを決定しようとする。
量化記号消去の手法は特定の理論における定義可能集合がそこまで複雑ではないことを示すことに使える。タルスキ(1948)は実閉体の量化記号消去（これは実数体の理論が決定可能であることをも示す結果である）を確立した。（彼はまた自身の手法が任意の標数の代数閉体にもそのまま適用可能であることを指摘した。）ここから発展した現代的な副分野はに関わる。
（1965）によって証明されたは、もし可算言語上の一階理論が或る非可算濃度について範疇的（つまりその濃度を持つ全てのモデルが同型）ならば、全ての非可算濃度で範疇的となることを述べる。
連続体仮説からの自明な帰結として、連続体濃度個未満の互いに非同型な可算モデルを持つような完全理論はそれ（非同型モデル）をちょうど可算個だけ持つこと、がある。に因むはこれが連続体仮説とは無関係に真であることを主張する。この予想は多くの特別なケースについて確立されている。
再帰理論.
再帰理論（計算可能性理論とも呼ばれる）は計算可能関数とチューリング次数（これは計算不可能関数を同じレベルの計算不可能性を持つ集合に分ける）の性質を研究する。再帰理論はまた一般計算可能性と定義可能性の研究を含む。再帰理論はアロンゾ・チャーチとアラン・チューリングによる1930年代の仕事（これはクリーネとポストによって1940年代に大きく拡張された）から生まれた。
古典再帰理論は自然数から自然数への関数の計算可能性に着目する。基本的な結果は、チューリング機械やラムダ計算やその他のシステムなど、多数の独立だが同値な特徴づけを持つ、ロバストかつカノニカルな計算可能関数のクラスを確立したことである。より高度な結果はチューリング次数の構造や帰納的可算集合の成す束に関するものである。
一般再帰理論は再帰理論の諸概念をもはや有限ではないような計算へと拡張する。そこには高階の型の計算可能性の研究ややなどの分野を同様に含む。
再帰理論の現代的研究には、純粋な再帰理論の新しい結果と同様に、その応用研究（例えばアルゴリズム的ランダムネス、、逆数学など）が含まれる。
アルゴリズム的に非可解な問題.
再帰理論の重要な部分領域ではアルゴリズム的に非可解な問題が研究される；決定問題または関数問題がアルゴリズム的に非可解（）あるいは決定不可能（）とは、任意の合法な入力に対して正しい解を返すような計算可能なアルゴリズムが存在しないことをいう。決定不可能性に関する最初の結果は、1936年にチャーチとチューリングによって独立に得られたもので、一階述語論理の決定問題がアルゴリズム的に非可解であるというものである。チュ―リングはこれを停止性問題の決定不可能性を示すことによって証明した。この結果は再帰理論と計算機科学の双方に広範な示唆を与えるものである。
通常の数学においても多くの決定不可能問題の例が知られている。群の語の問題は1955年のピョートル・ノビコフと1959年のW.ボーンによって独立に証明せられた。ビジービーバー問題は1962年にTibor Radóによって与えられた別のよく知られた例である。
ヒルベルトの第10問題は多変数整数係数代数方程式（ディオファントス方程式）が整数解を持つか否かを決定するアルゴリズムの存在を問うものである。部分的な解答はジュリア・ロビンソン、マーティン・デイビス、ヒラリー・パトナムらによって与えられた。この問題のアルゴリズム的非可解性はユーリ・マチャセヴィッチによって1970年に証明された（Davis 1973）。
証明論と構成的数学.
証明論は様々な論理推論体系における形式的証明の研究である。それら形式的証明は形式的な数学的対象であるから、それらの解析は数学的手法を用いて行うことができる。ヒルベルト流の体系、自然演繹の体系、ゲンツェンによって開発されたシークエント計算などを含む、いくつかの推論体系はよく考察される
数理論理学の文脈において、"構成的数学"の研究は、可述的体系の研究のような、非古典論理の体系の研究を含む。可述主義の初期の支持者はヘルマン・ワイルである。彼は実解析の大部分を可述的な方法だけを用いて展開できることを示した（Weyl 1918）。
形式的証明は完全に有限的なものであるが、構造における真理性はそうでないことから、構成的数学での作業では証明可能性を強調することが多い。古典（または非構成的）体系における証明可能性と直観主義（または構成的）体系での証明可能性との間の関係はとりわけ関心が持たれる。ゲーデル・ゲンツェン変換のような結果は古典論理を直観主義論理に埋め込む（翻訳する）ことが可能であることを示している。直観主義的証明に関するある性質は古典論理の証明に関するそれに逆翻訳できる。
最近の証明論における発展にはUlrich Kohlenbachによるproof miningの研究やMichael Rathjenによる証明論的順序数の研究が含まれる。
計算機科学との関係.
計算機科学における計算可能性理論の研究は数理論理学における計算可能性の研究と密接に関係している。ただしその重視されている点に違いがある。計算機科学者はしばしば具体的なプログラミング言語と実際的計算可能性に焦点を当てるが、数理論理学における研究者達は理論的な概念としての計算可能性と計算不可能性に焦点を当てる。
プログラミング言語の意味論の理論はプログラム検証（とくにモデル検査）などモデル理論に関係する。証明とプログラムの間のカリー・ハワード対応は証明論のとくに直観主義論理に関係する。ラムダ計算やコンビネータ論理のような形式計算は理想化されたプログラミング言語として研究される。
計算機科学はまた自動定理証明や論理プログラミングのような自動検証や証明探索の技術の開発によって数学に寄与している。
記述計算量理論は論理と計算量を関係づける。この領域での最初の重要な結果であるフェイギンの定理（1974）はNPがexistencialな二階述語論理の論理式で表現可能な言語の成す集合とちょうど一致することを示す。