数理論理学のソースを表示

'''数理論理学'''（すうりろんりがく、[[英語|英]] : mathematical logic）または'''現代[[論理学]]'''<ref name="nipponica">[https://kotobank.jp/word/%E8%AB%96%E7%90%86%E5%AD%A6-153697#E6.97.A5.E6.9C.AC.E5.A4.A7.E7.99.BE.E7.A7.91.E5.85.A8.E6.9B.B8.28.E3.83.8B.E3.83.83.E3.83.9D.E3.83.8B.E3.82.AB.29 『日本大百科全書』]</ref><ref name="worldEnc2nd">[https://kotobank.jp/word/%E8%A8%98%E5%8F%B7%E8%AB%96%E7%90%86%E5%AD%A6-50279#E4.B8.96.E7.95.8C.E5.A4.A7.E7.99.BE.E7.A7.91.E4.BA.8B.E5.85.B8.20.E7.AC.AC.EF.BC.92.E7.89.88 『世界大百科事典 第２版』]</ref>、'''記号論理学'''<ref name="nipponica" /><ref name="worldEnc2nd" />、'''[[数学基礎論]]'''{{Sfn|青本|上野|加藤|神保|2005|p=297}}、'''[[超数学]]'''{{Sfn|青本|上野|加藤|神保|2005|p=294}}は、[[数学]]の分野の一つであり{{Sfn|青本|上野|加藤|神保|2005|p=294}}、「[[数学]]の[[理論]]を展開する際にその骨格となる[[論理]]の構造を研究する分野」を指す{{Sfn|青本|上野|加藤|神保|2005|p=297}}{{Efn2|以下、『岩波　数学入門辞典』からの引用{{Sfn|青本|上野|加藤|神保|2005|p=297}}。{{Quotation|
'''数理論理学'''<br>　'''mathematical logic'''<br>
　数学の理論を展開する際にその骨格となる論理の構造を研究する分野をいう．数学基礎論とほぼ同義である．{{Sfn|青本|上野|加藤|神保|2005|p=297}}}}}}。数理論理学（数学基礎論）と密接に関連している分野としては[[計算機科学]]{{Interp|コンピュータ科学||和文=1}}{{Sfn|青本|上野|加藤|神保|2005|p=294}}や[[理論計算機科学]]などがある{{Efn2|以下、『岩波　数学入門辞典』からの引用{{Sfn|青本|上野|加藤|神保|2005|p=294}}。{{Quotation|
 '''数学基礎論'''<br>　'''foundations of mathematics'''<br>
　数理論理学や超数学とほぼ同じ意味で，論理を扱う数学の一分野である． … [[ゲーデルの不完全性定理]]は[[形式主義_(数学)|有限の立場（形式主義）]]で数学の[[無矛盾性]]を証明することはできないことを示した．[[:en:Gentzen's consistency proof|ゲンツェン（Gentzen）]]は，有限の立場より緩い制限のもとで自然数論の無矛盾性を証明した．<br>　数学基礎論は計算機科学とも密接に結びついている．{{Sfn|青本|上野|加藤|神保|2005|p=294}}}}}}{{Efn2|学部の教科書には Boolos, Burgess and Jeffrey [[数理論理学#CITEREFBoolosBurgessJeffrey2002|(2002)]]、 [[Herbert Enderton|Enderton]] [[数理論理学#CITEREFEnderton2001|(2001)]]、Mendelson [[数理論理学#CITEREFMendelson1997|(1997)]]がある。Shoenfield [[数理論理学#CITEREFShoenfield2001|(2001)]] による古典的な大学院の教科書は1967年に誕生した。}}。
{{See2|前現代の論理学については「[[伝統的論理学]]」を}}

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

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

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

==下位分野==
''Handbook of Mathematical Logic'' は数理論理学を大まかに次の4つの領域に分類している：
#[[集合論]]
#[[モデル理論]]
#[[再帰理論]]
#[[証明論]]と[[構成的数学]] （これらはひとつの領域の2つの部分と見做される）
それぞれの領域は異なる焦点を持っているものの、多くの技法や結果はそれら複数の領域の間で共有されている。これらの領域を分かつ境界線や、数理論理学と他の数学の分野とを分かつ境界線は、必ずしも明確ではない。[[ゲーデルの不完全性定理]]は再帰理論と証明論のマイルストーンであるだけではなく、[[様相論理]]における[[レーブの定理]]を導く。[[強制法]]の手法は集合論、モデル理論、再帰理論のほか[[直観主義的数学]]の研究などでも用いられる。

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

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

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

=== 19世紀 ===
<!-- symbolic logic -->
19世紀半ば、[[ジョージ・ブール]]と[[オーガスタス・ド・モルガン]]は体系的で数学的な論理の取り扱いを与えた。ブールらの仕事は、[[ジョージ・ピーコック]]などの代数学者の仕事の上に打ち立てられたものであり、アリストテレスの伝統的論理学を、[[数学基礎論]]を十分に研究できる枠組みに拡張した（[[#CITEREFKatz1998|Katz 1998]], p.&nbsp;686）。

[[チャールズ・サンダース・パース]]は、1870年から1885年の自身の論文において、ブールの研究の上に関係と量化子のための論理体系を作り上げた。

[[ゴットロープ・フレーゲ]]は1879年に発表した自身の[[概念記法]]において、量化子を含む論理の独自の開発を提示した。この仕事は論理の歴史における特徴的な転換点であると一般に考えられている。フレーゲの仕事は、この世紀の変わり目に[[バートランド・ラッセル]]が宣伝するまで日の目を見なかった。フレーゲの2次元的な表記法は広くは受け入れられず同時代のテキストでも使用されていない。<!-- 一方、 T proves A を意味する記号 \infer や、否定記号 \neg はフレーゲの記法を変形したものとして、現代でも使用されている。 -->

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

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

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

<!-- geometry -->
19世紀中頃、ユークリッドの幾何学の公理の欠陥が世に知られるようになった ([[#CITEREFKatz1998|Katz 1998]], p.&nbsp;774)。1826年に[[ニコライ・ロバチェフスキー]]によって確立された[[平行線公準]]の独立性 ([[#CITEREFLobachevsky1840|Lobachevsky 1840]]) に加え、数学者達は、ユークリッドが明らかと考えていた幾つかの定理が、実際にはユークリッドの公理からは証明できないことを発見した。それらの中には、直線は少なくとも二点を含むという定理や、同じ半径を持ち中心が半径と同じ距離だけ離れている二つの円は交わらねばならないという定理がある。ヒルベルト ([[#CITEREFHilbert1899|1899]]) は[[パッシュの公理|パッシュの先行研究]] ([[#CITEREFPasch1882|1882]]) のもとに、完全な{{仮リンク|幾何学の公理|en|Hilbert's axioms}}の集合を開発した。幾何学の公理化の成功はヒルベルトに他の数学の分野（自然数や[[数直線]]など）の完全な公理化を探求するよう動機付けた。これが20世紀前半の主要な研究領域となることが分かる。
<!-- The 19th century saw great advances in the theory of [[real analysis]], including theories of convergence of functions and [[Fourier series]]. Mathematicians such as [[Karl Weierstrass]] began to construct functions that stretched intuition, such as [[Continuous, nowhere differentiable function|nowhere-differentiable continuous functions]]. Previous conceptions of a function as a rule for computation, or a smooth graph, were no longer adequate.  Weierstrass began to advocate the [[arithmetization of analysis]], which sought to axiomatize analysis using properties of the natural numbers. The modern [[(ε, δ)-definition of limit]] and [[continuous function]]s was already developed by [[Bernard Bolzano|Bolzano]] in 1817 ([[#CITEREFFelscher2000|Felscher 2000]]), but remained relatively unknown.
[[Cauchy]] in 1821 defined continuity in terms of [[infinitesimal]]s (see Cours d'Analyse, page 34).  In 1858, Dedekind proposed a definition of the real numbers in terms of [[Dedekind cuts]] of rational numbers [[#CITEREFDedekind1872|(Dedekind 1872)]], a definition still employed in contemporary texts.

[[Georg Cantor]] developed the fundamental concepts of infinite set theory. His early results developed the theory of [[cardinality]] and [[Cantor's first uncountability proof|proved]] that the reals and the natural numbers have different cardinalities (Cantor 1874). Over the next twenty years, Cantor developed a theory of [[transfinite number]]s in a series of publications. In 1891, he published a new proof of the uncountability of the real numbers that introduced the [[Cantor's diagonal argument|diagonal argument]], and used this method to prove [[Cantor's theorem]] that no set can have the same cardinality as its [[powerset]]. Cantor believed that every set could be [[well-ordered]], but was unable to produce a proof for this result, leaving it as an open problem in 1895 ([[#CITEREFKatz1998|Katz 1998, p.&nbsp;807]]). -->

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

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

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

選択公理に関する疑念は最近の素朴集合論におけるパラドックスの発見により強化された。集合論のパラドックスについて初めて述べたのは[[チェザーレ・ブラリ・フォルティ]]（[[#CITEREFBurali-Forti1897|1897]]）である：[[ブラリ＝フォルティのパラドックス]]は全ての[[順序数]]からなる集まりが集合を成さないことを示す。<!-- 訳注：これはZFCにおいて解釈した場合である。もとは素朴集合論の矛盾を指摘したものである。 -->その直後に、[[バートランド・ラッセル]]は1901年に[[ラッセルのパラドックス]]を、[[ジュール・リシャール]]（[[#CITEREFRichard1905|1905]]）は[[リシャールのパラドックス]]を発見した。

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

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

フレンケル([[#CITEREFFraenkel1922|1922]])は、選択公理が{{仮リンク|原子 (数理論理学)|en|urelement|label=原子}}付きツェルメロ集合論の残りの公理からは証明できないことを証明した。後の[[ポール・コーエン (数学者)|ポール・コーエン]]([[#CITEREFCohen1966|1966]])による仕事は、（その証明には）原子の追加が不要であって、選択公理はZFにおいて証明不可能であることを示した。コーエンの証明は[[強制法]]の手法を生み、今日では集合論における{{仮リンク|独立性結果|en|Independence (mathematical logic)}}を確立するための重要なツールとなっている{{Efn2|{{harvnb|Cohen|2008}}を参照}}。

==== 記号論理 ====
{{仮リンク|レオポルト・レーヴェンハイム|en| Leopold  Löwenheim |preserve=1}}（[[#CITEREFL.C3.B6wenheim1915|1915]]）と[[トアルフ・スコーレム]]（[[#CITEREFSkolem1920|1920]]）は[[レーヴェンハイム-スコーレムの定理]]を得た。これは一階述語論理は無限構造の濃度を制御できないことを述べる。スコーレムは、この定理を一階で形式化された集合論へ適用でき、そのいかなる形式化も[[可算]][[数理モデル|モデル]]を持つことが導かれる、ということに気付いた。この直観に反する結果は[[スコーレムのパラドックス]]として知られることになった。

ゲーデルは自身の博士論文（[[#CITEREFGödel1929|1929]]）において[[完全性定理]]を示した。これは[[一階述語論理|一階論理]]における構文論と意味論の間の対応を確立する。<!-- 正確には証明可能性と真理性の間の対応というべきであろう。証明体系は論理式という形式言語を証明可能性という尺度で分類するものであり、これは意味論に分類される作業である。（モデル論的意味論はモデルにおける真理性という尺度で論理式を分類するわけである。）他方、そこで扱われる形式的証明は構文論「的」な対象であり、その扱いは記号操作に基づく構文論「的」なものであるから、証明体系による論理式の分類という作業は構文論「的」である。元々の文章における構文論と意味論という言葉を、形容詞的に解釈するならばそのままの表現でも問題はないが、名詞的に解釈するならば問題がある。-->ゲーデルは完全性定理を[[コンパクト性定理]]の証明に用いた。これは一階の[[論理的帰結]]の有限性を立証する。これらの結果は一階論理を数学者にとって支配的な論理として確立することを助けた。

1931年、ゲーデルは''{{仮リンク|プリンキピア・マテマティカとそれに関連する体系において形式的に決定不可能な命題について|en|On Formally Undecidable Propositions of Principia Mathematica and Related Systems}}''を出版した。ここでは、十分に強く、実効的な一階理論<!-- 原文ママ。ゲーデルの論文ではこのような設定のもとでは証明されていないはず。例えばプリンキピア・マテマティカ（をゲーデルが簡単化した体系）は一階論理ではない。要修正。 -->が不完全（完全性定理のそれとは異なる意味である）であることを示されている。この結果は[[ゲーデルの不完全性定理]]として知られ、数学の公理的基礎の厳密な限界を示すものであり、ヒルベルト・プログラムに大きな打撃を与えた。これは算術の無矛盾性をいかなる算術の形式理論においても証明できないことを示している。<!-- 原文ママ。この書き方だと、ペアノ算術にある構成的順序数までの超限帰納法（ゲンツェン）や、その他の組合せ論的原理を追加した体系からも、ペアノ算術の無矛盾性は証明できないかのように読めてしまう。いかなる（ある程度強力な）算術の形式理論もそれ自身の無矛盾性を証明できない、と書いた方がよい。-->しかしながら、ヒルベルトは、不完全性定理の重要性を、あるときまで認めなかった。

ゲーデルの定理は十分に強く、実効的な公理系の無矛盾性の証明はそれが無矛盾である限り、それ自身からもそれよりも弱い体系からも得られないことを示す。これはいま考えている体系で形式化できないような無矛盾性証明の可能性については未解決のまま残す。ゲンツェン（[[#CITEREFGentzen1936|1936]]）は算術の無矛盾性を<!-- ある構成的順序数（<math>\varepsilon_{0}</math>）までの -->[[超限帰納法]]の原理を持つ有限的な体系を用いて証明した。ゲンツェンの結果は[[カット除去定理|カット除去]]と[[証明論的順序数]]の概念を生み出し、これらは証明論における主要な道具となった。ゲーデル（[[#CITEREFGödel1958|1958]]）は別の無矛盾性証明を与えた。これは古典算術の無矛盾性を高階直観主義算術の無矛盾性に還元することで為された。<!-- ダイアレクティカ解釈 -->

====他の分科の始まり====
[[アルフレッド・タルスキ]]は[[モデル理論]]の基礎を発展させた。

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

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

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

== 形式論理体系 ==
数理論理学の中心では形式論理体系を用いて表現された数学の概念を取り扱う。それらの体系は、多くの細部の差異はあるが、固定した形式言語で記述されるという共通の性質がある。[[命題論理]]と[[一階述語論理]]の体系は今日では最も広く研究されている。それは[[数学基礎論]]への応用可能性とそれらの望ましい証明論的な性質の故である{{Efn2|Ferreirós ([[#CITEREFFerreir.C3.B3s2001|2001]]) は、20世紀初頭の他の形式論理に対する一階論理の進歩をまとめている。}}。より強い古典論理、例えば[[二階述語論理]]や[[無限論理]]もまた[[直観主義論理]]とともに研究されている。

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

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

[[ゲーデルの完全性定理]]　([[#CITEREFG.C3.B6del1929|Gödel 1929]])　は一階論理の[[論理的帰結]]に対する構文論的定義と意味論的定義の同値性を確立した。これは、もしある特定の文が、ある特定の公理の集合を満たすあらゆるモデルで真であるならば、それらの公理からその文への有限な演繹が存在することを示している。<!-- The [[compactness theorem]] first appeared as a lemma in Gödel's proof of the completeness theorem, and it took many years before logicians grasped its significance and began to apply it routinely. It says that a set of sentences has a model [[if and only if]] every finite subset has a model, or in other words that an inconsistent set of formulas must have a finite inconsistent subset. The completeness and compactness theorems allow for sophisticated analysis of logical consequence in first-order logic and the development of [[model theory]], and they are a key reason for the prominence of first-order logic in mathematics.

[[Gödel's incompleteness theorems]] ([[#CITEREFG.C3.B6del1931|Gödel 1931]]) establish additional limits on first-order axiomatizations. The '''first incompleteness theorem''' states that for any sufficiently strong, effectively given logical system there exists a statement which is true but not provable within that system. Here a logical system is effectively given if it is possible to decide, given any formula in the language of the system, whether the formula is an axiom. A logical system is sufficiently strong if it can express the [[Peano axioms]]. When applied to first-order logic, the first incompleteness theorem implies that any sufficiently strong, consistent, effective first-order theory has models that are not [[elementary substructure|elementarily equivalent]], a stronger limitation than the one established by the Löwenheim–Skolem theorem. The '''second incompleteness theorem''' states that no sufficiently strong, consistent, effective axiom system for arithmetic can prove its own consistency, which has been interpreted to show that Hilbert's program cannot be completed. -->

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

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

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

他のタイプの論理としては[[不動点論理]]があり、これは[[原始帰納的関数]]の記述に使われるような[[帰納的定義]]を許す。
<!-- One can formally define an extension of first-order logic &mdash; a notion which encompasses all logics in this section because they behave like first-order logic in certain fundamental ways, but does not encompass all logics in general, e.g. it does not encompass intuitionistic, modal or [[fuzzy logic]]. [[Lindström's theorem]] implies that the only extension of first-order logic satisfying both the [[compactness theorem]] and the Downward [[Löwenheim–Skolem theorem]] is first-order logic. -->

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

[[直観主義論理]]は[[ライツェン・エヒベルトゥス・ヤン・ブラウワー|ブラウワー]]の直観主義(ブラウワー自身はその形式化を避けたが)のプログラムの研究から[[アレン・ハイティング|ハイティング]]によって形式化・発展せられたものである。直観主義論理は[[排中律]]、すなわち任意の文が真または偽であるという原理を、明確に含まない論理である。[[スティーヴン・コール・クリーネ|クリーネ]]の直観主義論理の証明論に関する仕事は、直観主義的な証明からは構成的な情報が復元できることを示している。例えば、直観主義的算術のいかなる証明可能全域関数も[[計算可能関数|計算可能]]である。<!-- 明らかに誤りである。どんな算術の形式的体系であろうと、その体系が再帰的公理化可能である限り、全ての証明可能全域関数は計算可能である。次のように改めるべきである：直観主義算術において <math>\forall x \exists y \varphi(x,y)</math> が示されたならば、その証明から <math>\varphi(n, f(n))</math> を満たす関数 <math>f</math> を計算するプログラムを抽出することができる。-->このことは[[ペアノ算術]]のような算術の古典理論においては成立しない。

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

== 集合論 ==
{{Main|集合論}}
<!-- '''[[Set theory]]''' is the study of [[Set (mathematics)|sets]], which are abstract collections of objects. Many of the basic notions, such as ordinal and cardinal numbers, were developed informally by Cantor before formal axiomatizations of set theory were developed. The first such axiomatization, due to Zermelo ([[#CITEREFZermelo1908b|1908b]]), was extended slightly to become [[Zermelo–Fraenkel set theory]] (ZF), which is now the most widely used foundational theory for mathematics.

Other formalizations of set theory have been proposed, including [[von Neumann–Bernays–Gödel set theory]] (NBG), [[Morse–Kelley set theory]] (MK), and [[New Foundations]] (NF).  Of these, ZF, NBG, and MK are similar in describing a [[cumulative hierarchy]] of sets. New Foundations takes a different approach; it allows objects such as the set of all sets at the cost of restrictions on its set-existence axioms. The system of [[Kripke–Platek set theory]] is closely related to generalized recursion theory.

Two famous statements in set theory are the [[axiom of choice]] and the [[continuum hypothesis]]. The axiom of choice, first stated by Zermelo ([[#CITEREFZermelo1904|1904]]), was proved independent of ZF by Fraenkel ([[#CITEREFFraenkel1922|1922]]), but has come to be widely accepted by mathematicians.  It states that given a collection of nonempty sets there is a single set ''C'' that contains exactly one element from each set in the collection. The set ''C'' is said to "choose" one element from each set in the collection. While the ability to make such a choice is considered obvious by some, since each set in the collection is nonempty, the lack of a general, concrete rule by which the choice can be made renders the axiom nonconstructive. [[Stefan Banach]] and [[Alfred Tarski]] (1924) showed that the axiom of choice can be used to decompose a solid ball into a finite number of pieces which can then be rearranged, with no scaling, to make two solid balls of the original size. This theorem, known as the [[Banach–Tarski paradox]], is one of many counterintuitive results of the axiom of choice.

The continuum hypothesis, first proposed as a conjecture by Cantor, was listed by David Hilbert as one of his 23 problems in 1900. Gödel showed that the continuum hypothesis cannot be disproven from the axioms of Zermelo–Fraenkel set theory (with or without the axiom of choice), by developing the [[constructible universe]] of set theory in which the continuum hypothesis must hold. In 1963, [[Paul Cohen (mathematician)|Paul Cohen]] showed that the continuum hypothesis cannot be proven from the axioms of Zermelo–Fraenkel set theory ([[#CITEREFCohen1966|Cohen 1966]]). This independence result did not completely settle Hilbert's question, however, as it is possible that new axioms for set theory could resolve the hypothesis. Recent work along these lines has been conducted by [[W. Hugh Woodin]], although its importance is not yet clear ([[#CITEREFWoodin2001|Woodin 2001]]).

Contemporary research in set theory includes the study of [[large cardinal]]s and [[determinacy]].  Large cardinals are [[cardinal numbers]] with particular properties so strong that the existence of such cardinals cannot be proved in ZFC. The existence of the smallest large cardinal typically studied, an [[inaccessible cardinal]], already implies the consistency of ZFC.  Despite the fact that large cardinals have extremely high [[cardinality]], their existence has many ramifications for the structure of the real line.  ''Determinacy'' refers to the possible existence of winning strategies for certain two-player games (the games are said to be ''determined''). The existence of these strategies implies structural properties of the real line and other [[Polish space]]s. -->

== モデル理論 ==
{{Main|モデル理論}}
'''[[モデル理論]]'''は様々な形式理論のモデルを研究する。ここで{{仮リンク|理論 (数理論理学)|en|theory (mathematical logic)|label=理論}}とは特定の形式論理に於ける論理式と{{仮リンク|シグネチャ (論理学)|en|Signature (logic)|label=シグネチャ}}からなる集まりで、{{仮リンク|モデル (数理論理学)|en|Structure (mathematical logic)|label=モデル}}とはその理論の具体的な解釈を与える構造である。モデル理論は[[普遍代数]]と[[代数幾何学]]に密接に関係しているが、モデル理論の手法は他の分野よりも論理的な考察に重きを置いている。

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

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

{{仮リンク|マイケル・D・モーレイ|en|Michael D. Morley}}（1965）によって証明された{{仮リンク|モーレイの範疇性定理|en|Morley's categoricity theorem}}は、もし可算言語上の一階理論が或る非可算濃度について範疇的（つまりその濃度を持つ全てのモデルが同型）ならば、全ての非可算濃度で範疇的となることを述べる。

[[連続体仮説]]からの自明な帰結として、連続体濃度個未満の互いに非同型な可算モデルを持つような完全理論はそれ（非同型モデル）をちょうど可算個だけ持つこと、がある。{{仮リンク|ロバート・ローソン・ヴォート|en|Robert Lawson Vaught}}に因む{{仮リンク|ヴォート予想|en|Vaught conjecture}}はこれが連続体仮説とは無関係に真であることを主張する。<!-- 訳注：つまり非可算個の可算モデル（の同型類）を持つ完全理論は存在しない -->この予想は多くの特別なケースについて確立されている。

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

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

一般再帰理論は再帰理論の諸概念をもはや有限ではないような計算へと拡張する。そこには高階の型の計算可能性の研究や{{仮リンク|超算術的理論|en|hyperarithmetical theory}}や{{仮リンク|アルファ再帰理論|en|alpha recursion theory}}などの分野を同様に含む。

再帰理論の現代的研究には、純粋な再帰理論の新しい結果と同様に、その応用研究（例えば[[アルゴリズム的ランダムな無限列|アルゴリズム的ランダム性]]、{{仮リンク|計算可能モデル理論|en|Computable model theory}}、[[逆数学]]など）が含まれる。

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

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

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

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

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

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

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

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

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

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

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

== 数学基礎論 ==
{{Main|数学基礎論}}
<!-- In the 19th century, mathematicians became aware of logical gaps and inconsistencies in their field. It was shown that [[Euclid]]'s axioms for geometry, which had been taught for centuries as an example of the axiomatic method, were incomplete. The use of [[infinitesimal]]s, and the very definition of [[Function (mathematics)|function]], came into question in analysis, as pathological examples such as Weierstrass' nowhere-[[differentiable]] continuous function were discovered.

Cantor's study of arbitrary infinite sets also drew criticism. [[Leopold Kronecker]] famously stated "God made the integers; all else is the work of man," endorsing a return to the study of finite, concrete objects in mathematics. Although Kronecker's argument was carried forward by constructivists in the 20th century, the mathematical community as a whole rejected them. [[David Hilbert]] argued in favor of the study of the infinite, saying "No one shall expel us from the Paradise that Cantor has created."

Mathematicians began to search for axiom systems that could be used to formalize large parts of mathematics. In addition to removing ambiguity from previously naive terms such as function, it was hoped that this axiomatization would allow for consistency proofs.  In the 19th century, the main method of proving the consistency of a set of axioms was to provide a model for it. Thus, for example, [[non-Euclidean geometry]] can be proved consistent by defining ''point'' to mean a point on a fixed sphere and ''line'' to mean a [[great circle]] on the sphere. The resulting structure, a model of [[elliptic geometry]], satisfies the axioms of plane geometry except the parallel postulate.

With the development of formal logic, Hilbert asked whether it would be possible to prove that an axiom system is consistent by analyzing the structure of possible proofs in the system, and showing through this analysis that it is impossible to prove a contradiction. This idea led to the study of [[proof theory]]. Moreover, Hilbert proposed that the analysis should be entirely concrete, using the term ''finitary'' to refer to the methods he would allow but not precisely defining them. This project, known as [[Hilbert's program]], was seriously affected by Gödel's incompleteness theorems, which show that the consistency of formal theories of arithmetic cannot be established using methods formalizable in those theories. Gentzen showed that it is possible to produce a proof of the consistency of arithmetic in a finitary system augmented with axioms of [[transfinite induction]], and the techniques he developed to do so were seminal in proof theory.

A second thread in the history of foundations of mathematics involves [[nonclassical logic]]s and [[constructive mathematics]]. The study of constructive mathematics includes many different programs with various definitions of ''constructive''. At the most accommodating end, proofs in ZF set theory that do not use the axiom of choice are called constructive by many mathematicians. More limited versions of constructivism limit themselves to [[natural numbers]], [[number-theoretic function]]s, and sets of natural numbers (which can be used to represent real numbers, facilitating the study of [[mathematical analysis]]). A common idea is that a concrete means of computing the values of the function must be known before the function itself can be said to exist. [plz add ref "Varieties of constructive mathematics"]

In the early 20th century, [[Luitzen Egbertus Jan Brouwer]] founded [[intuitionism]] as a philosophy of mathematics. This philosophy, poorly understood at first, stated that in order for a mathematical statement to be true to a mathematician, that person must be able to ''intuit'' the statement, to not only believe its truth but understand the reason for its truth. A consequence of this definition of truth was the rejection of the [[law of the excluded middle]], for there are statements that, according to Brouwer, could not be claimed to be true while their negations also could not be claimed true.  Brouwer's philosophy was influential, and the cause of bitter disputes among prominent mathematicians. Later, Kleene and Kreisel would study formalized versions of intuitionistic logic (Brouwer rejected formalization, and presented his work in unformalized natural language). With the advent of the [[BHK interpretation]] and [[Kripke model]]s, intuitionism became easier to reconcile with classical mathematics. -->

== 関連項目 ==
{{ウィキプロジェクトリンク|数学|[[画像:Nuvola apps edu mathematics blue-p.svg|34px|Project:数学]]}}
{{ウィキポータルリンク|数学|[[画像:Nuvola apps edu mathematics-p.svg|34px|Portal:数学]]}}
{{Portal|Logic}}
* [[数学基礎論]]
* [[計算可能性理論]] - [[計算科学]]
** [[計算論]]／計算理論
* [[再帰理論]]
* [[集合論]]
* [[証明論]]
* [[非古典論理]]
* [[モデル理論]]
* [[:Category:研究の計算分野]]
** [[計算言語学]] - [[計算論的哲学]]

== 脚注 ==
=== 注釈 ===
{{Notelist2}}
=== 引用 ===
{{Reflist}}

==参考文献==

=== 学部教科書 ===
*{{Citation|和書
 |last1       = 青本
 |first1      = 和彦（編）
 |last2       = 上野
 |first2      = 健爾（編）
 |last3       = 加藤
 |first3      = 和也（編）
 |last4       = 神保
 |first4      = 道夫（編）
 |last5       = 砂田
 |first5      = 利一（編）
 |last6       = 高橋
 |first6      = 陽一郎（編）
 |last7       = 深谷
 |first7      = 賢治（編）
 |last8       = 俣野
 |first8      = 博（編）
 |last9       = 室田
 |first9      = 一雄（編）
 |authorlink1 = 青本和彦
 |authorlink2 = 上野健爾
 |authorlink3 = 加藤和也_(数学者)
 |authorlink4 = 神保道夫
 |date        = 2005-09-29
 |title       = 岩波　数学入門辞典
 |edition     = 第1刷
 |publisher   = 岩波書店
 |isbn        = 978-4000802093
 |ref         = harv}}
* {{Citation
  |last1=Walicki
  |first1=Michał
  |title=Introduction to Mathematical Logic
  |publisher=[[World Scientific Publishing]]
  |location=Singapore
  |isbn=978-981-4343-87-9 
  |year=2011}}.
* {{Citation
  |last1=Boolos
  |first1=George
  |author1-link=:en:George Boolos
  |last2=Burgess
  |first2=John
  |last3=Jeffrey
  |first3=Richard
  |author3-link=:en:Richard Jeffrey
  |title=Computability and Logic
  |publisher=[[Cambridge University Press]]
  |location=Cambridge
  |edition=4th
  |isbn=978-0-521-00758-0 
  |year=2002}}.
* {{citation | last1=Crossley | first1=J.N. | last2=Ash | first2=C.J. | last3=Brickhill | first3=C.J. | last4=Stillwell | first4=J.C. | last5=Williams | first5=N.H. | title=What is mathematical logic? | zbl=0251.02001 | location=London-Oxford-New York | publisher=[[Oxford University Press]] | year=1972 | isbn=0-19-888087-1 }}.
* {{Citation
  |last1=Enderton
  |first1=Herbert
  |title=A mathematical introduction to logic
  |publisher=[[Academic Press]]
  |location=Boston, MA
  |edition=2nd
  |isbn=978-0-12-238452-3
  |year=2001}}.
* {{Citation
  |last1=Hamilton
  |first1=A.G.
  |title=Logic for Mathematicians
  |publisher=Cambridge University Press
  |location=Cambridge
  |edition=2nd
  |isbn=978-0-521-36865-0
  |year=1988}}.
*{{Citation
  |last1=Ebbinghaus
  |first1=H.-D.
  |last2=Flum
  |first2=J.
  |last3=Thomas
  |first3=W.
  |doi=
  |title=Mathematical Logic
  |url=http://www.springer.com/mathematics/book/978-0-387-94258-2
  |publisher=[[Springer Science+Business Media|Springer]]
  |location=[[ニューヨーク|New York]]
  |edition=2nd
  |isbn=0-387-94258-0
  |year=1994}}.
* {{Citation
  |last1=Katz
  |first1=Robert
  |title=Axiomatic Analysis
  |publisher=[[D. C. Heath and Company]]
  |location=Boston, MA
  |year=1964}}.
* {{Citation
  |last1=Mendelson
  |first1=Elliott
  |title=Introduction to Mathematical Logic
  |publisher=[[Chapman & Hall]]
  |location=London
  |edition=4th
  |isbn=978-0-412-80830-2
  |year=1997}}.
* {{Citation
  |last=Rautenberg
  |first=Wolfgang
  |authorlink=Wolfgang Rautenberg
  |doi=10.1007/978-1-4419-1221-3
  |title=A Concise Introduction to Mathematical Logic
  |url=http://www.springerlink.com/content/978-1-4419-1220-6/
  |publisher=[[Springer Science+Business Media]]
  |location=[[ニューヨーク|New York]]
  |edition=3rd
  |isbn=978-1-4419-1220-6
  |year=2010}}.
* {{Citation
  |last1=Schwichtenberg
  |first1=Helmut
  |title=Mathematical Logic
  |publisher=Mathematisches Institut der Universität München
  |location=Munich, Germany
  |url=http://www.mathematik.uni-muenchen.de/~schwicht/lectures/logic/ws03/ml.pdf
  |year=2003–2004}}.
* 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 [[Computational complexity theory|complexity theory]]

=== 大学院教科書 ===
* {{Citation
  | last1=Andrews
  | first1=Peter B.
  | title=An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof
  | publisher=Kluwer Academic Publishers
  | location=Boston
  | edition=2nd
  | isbn=978-1-4020-0763-7
  | year=2002}}.
* {{Citation
  | editor1-last=Barwise
  | editor1-first=Jon
  | title=Handbook of Mathematical Logic
  | publisher=[[Elsevier|North Holland]]
  | series=Studies in Logic and the Foundations of Mathematics
  | isbn=978-0-444-86388-1
  | year=1989}}.
* {{Citation
  | last1=Hodges
  | first1=Wilfrid
  | author1-link=Wilfrid Hodges
  | title=A shorter model theory
  | publisher=[[Cambridge University Press]]
  | location=Cambridge | isbn=978-0-521-58713-6 | year=1997}}.
* {{Citation
  | last1=Jech
  | first1=Thomas
  | author1-link=:en:Thomas Jech
  | title=Set Theory: Millennium Edition
  | publisher=[[Springer-Verlag]]
  | location=Berlin, New York
  | series=Springer Monographs in Mathematics
  | isbn=978-3-540-44085-7
  | year=2003}}.
* {{Citation
  | last1=Shoenfield
  | first1=Joseph R.
  | title=Mathematical Logic
  | origyear=1967
  | publisher=[[A K Peters]]
  | edition=2nd
  | isbn=978-1-56881-135-2
  | year=2001}}.
* {{Citation
  | last1=Troelstra
  | first1=Anne Sjerp
  | author1-link=:en:A. S. Troelstra
  | last2=Schwichtenberg
  | first2=Helmut
  | title=Basic Proof Theory
  | publisher=Cambridge University Press
  | location=Cambridge
  | edition=2nd
  | series=Cambridge Tracts in Theoretical Computer Science
  | isbn=978-0-521-77911-1
  | year=2000}}.

=== 研究論文、モノグラフ、教科書、サーベイ ===
* {{Citation
  | last1=Cohen
  | first1=P. J.
  | title=Set Theory and the Continuum Hypothesis
  | publisher=W. A. Benjamin
  | location=Menlo Park, CA
  | year=1966}}.
* {{cite book|ref=harv|last1=Cohen|first1=Paul Joseph|author1-link=Paul Cohen (mathematician)|title=Set theory and the continuum hypothesis|year=2008|origyear=1966|publisher=Dover Publications|location=Mineola, New York|isbn=978-0-486-46921-8}}.
* {{Citation
  | last1=Davis
  | first1=Martin
  | author1-link=Martin Davis
  | title=Hilbert's tenth problem is unsolvable
  | year=1973
  | journal=[[American Mathematical Monthly|The American Mathematical Monthly]]
  | volume=80
  | pages=233–269
  | doi=10.2307/2318447
  | issue=3
  | publisher=The American Mathematical Monthly, Vol. 80, No. 3
  | jstor=2318447}}, reprinted as an appendix in Martin Davis, Computability and Unsolvability, Dover reprint 1982. [http://links.jstor.org/sici?sici=0002-9890%28197303%2980%3A3%3C233%3AHTPIU%3E2.0.CO%3B2-E JStor]
*{{Citation
 | title=Bolzano, Cauchy, Epsilon, Delta
 | first1=Walter
 | last1=Felscher
 |journal=The American Mathematical Monthly
 | volume = 107
 | year = 2000
 | pages = 844&ndash;862
 | doi=10.2307/2695743
 | issue = 9
 | publisher=The American Mathematical Monthly, Vol. 107, No. 9
 | jstor=2695743}}. [http://links.jstor.org/sici?sici=0002-9890(200011)107%3A9%3C844%3ABCED%3E2.0.CO%3B2-L JSTOR]
*{{Citation
  | last1=Ferreirós
  | first1=José
  | title=The Road to Modern Logic-An Interpretation
  |journal=Bulletin of Symbolic Logic
  |volume=7
  |year=2001
  |pages=441&ndash;484
  | doi=10.2307/2687794
  |issue=4
  | publisher=The Bulletin of Symbolic Logic, Vol. 7, No. 4
  | jstor=2687794}}. [http://links.jstor.org/sici?sici=1079-8986%28200112%297%3A4%3C441%3ATRTMLI%3E2.0.CO%3B2-O  JStor]
* {{Citation
 | last1 = Hamkins
 | first1 = Joel David
 | first2 =
 | last2 = [[Benedikt Löwe]]
 | title =  The modal logic of forcing
 | journal = Transactions of the American Mathematical Society}}, to appear. [http://www.ams.org/tran/0000-000-00/S0002-9947-07-04297-3/home.html Electronic posting by the journal]
* {{Citation
  | last1=Katz
  | first1=Victor J.
  | title = A History of Mathematics
  | year = 1998
  | publisher = Addison–Wesley
  | isbn = 0-321-01618-1}}.
* {{Citation
  | last1=Morley
  | first1=Michael
  | author1-link=Michael D. Morley
  | title=Categoricity in Power
  | doi=10.2307/1994188
  | year=1965
  | journal=[[Transactions of the American Mathematical Society]]
  | volume=114
  | issue=2
  | pages=514–538
  | publisher=Transactions of the American Mathematical Society, Vol. 114, No. 2
  | jstor=1994188}}.
*{{Citation
  | last1 = Soare
  | first1 = Robert I.
  | title = Computability and recursion
  | journal = Bulletin of Symbolic Logic
  | volume = 2
  | pages = 284–321
  | doi = 10.2307/420992
  | year = 1996
  | issue = 3
  | publisher = The Bulletin of Symbolic Logic, Vol. 2, No. 3
  | jstor = 420992}}.
*{{Citation
  | last1=Solovay
  | first1= Robert M.
  | author-link = Robert M. Solovay
  | title = Provability Interpretations of Modal Logic
  | journal = Israel Journal of Mathematics
  | volume = 25
  | year = 1976
  | pages=287&ndash;304
  | doi=10.1007/BF02757006
  | issue=3–4}}.
*{{Citation
  | last1=Woodin
  | first1=W. Hugh
  | author1-link=W. Hugh Woodin
  | title=The Continuum Hypothesis, Part I
  |journal=Notices of the American Mathematical Society
  |volume=48
  |year=2001
  |issue=6}}. [http://www.ams.org/notices/200106/fea-woodin.pdf PDF]

=== 古典的な論文、教科書、論文集 ===
*{{Citation
  | first1=Cesare
  | last1=Burali-Forti
  | year=1897|title = A question on transfinite numbers}}, reprinted in van Heijenoort 1976, pp.&nbsp;104&ndash;111.
*{{citation
  | first1=Richard
  | last1=Dedekind
  | year=1872
  | title=Stetigkeit und irrationale Zahlen}}. English translation of title: "Consistency and irrational numbers".
*{{Citation
  | first1=Richard
  | last1=Dedekind
  | year=1888
  | title=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.
*{{citation
  | first1=Abraham A.
  | last1=Fraenkel
  | year=1922
  | contribution=Der Begriff 'definit' und die Unabhängigkeit des Auswahlsaxioms
  | title=Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-mathematische Klasse
  | pages=253&ndash;257}} (German), reprinted in English translation as "The notion of 'definite' and the independence of the axiom of choice", van Heijenoort 1976, pp.&nbsp;284&ndash;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.
* {{citation
  | author-link=Gerhard Gentzen
  | first1=Gerhard
  | last1=Gentzen
  | year=1936
  | title=Die Widerspruchsfreiheit der reinen Zahlentheorie
  | journal=Mathematische Annalen
  | volume=112
  | pages=132&ndash;213
  | doi=10.1007/BF01565428}}, reprinted in English translation in Gentzen's ''Collected works'', M. E. Szabo, ed., North-Holland, Amsterdam, 1969.{{Specify|date=September 2009}}
*{{Citation
  | last1=Gödel
  | first1=Kurt
  | year = 1929
  | title = Über die Vollständigkeit des Logikkalküls
  | series = doctoral dissertation
  | publisher = University Of Vienna}}. English translation of title: "Completeness of the logical calculus".
* {{Citation
  | last1=Gödel
  | first1=Kurt
  | year = 1930
  | title = Die Vollständigkeit der Axiome des logischen Funktionen-kalküls
  | journal =  Monatshefte für Mathematik und Physik
  | volume = 37
  | pages = 349&ndash;360
  | doi=10.1007/BF01696781}}. English translation of title: "The completeness of the axioms of the calculus of logical functions".
* {{Citation
  | last1=Gödel
  | first1=Kurt
  | title=Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
  | year=1931
  | journal=Monatshefte für Mathematik und Physik
  | volume=38
  | issue=1
  | pages=173–198
  | doi=10.1007/BF01700692}}, see [[On Formally Undecidable Propositions of Principia Mathematica and Related Systems]] for details on English translations.
*{{Citation
  | last1=Gödel
  | first1=Kurt
  | title=Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes
  | year=1958
  | journal=Dialectica. International Journal of Philosophy
  | volume=12
  | pages=280–287
  | doi=10.1111/j.1746-8361.1958.tb01464.x
  | issue=3–4}}, reprinted in English translation in Gödel's ''Collected Works'', vol II, Soloman Feferman et al., eds. Oxford University Press, 1990.{{Specify|date=September 2009}}
*{{citation
  | editor-first=Jean
  | editor-last=van Heijenoort
  | editor-link=Jean van Heijenoort
  | title = From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931
  | edition = 3rd
  | publisher = Harvard University Press
  | location = Cambridge, Mass
  | year = 1967, 1976 3rd printing with corrections
  | id = (pbk.)
  | isbn=0-674-32449-8}}
*{{citation
  | last1=Hilbert
  | first1=David
  | year = 1899
  | title = Grundlagen der Geometrie
  | publisher = Teubner
  | location = Leipzig}}, English 1902 edition (''The Foundations of Geometry'') republished 1980, Open Court, Chicago.
*{{Citation
  |first1=Hilbert
  |last1=David
  |year=1929
  |title=Probleme der Grundlegung der Mathematik
  |journal=Mathematische Annalen|volume=102|pages=1&ndash;9
  |url=http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=GDZPPN002273500&L=1
  |doi=10.1007/BF01782335}}. 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.&nbsp;266&ndash;273.
* {{Citation
  | last1=Kleene
  | first1=Stephen Cole
  | author1-link=:en:Stephen Kleene
  | title=Recursive Predicates and Quantifiers
  | year=1943
  | journal=American Mathematical Society Transactions
  | volume=54
  | issue=1
  | pages=41–73
  | doi=10.2307/1990131
  | publisher=Transactions of the American Mathematical Society, Vol. 53, No. 1
  | jstor=1990131}}.
* {{Citation
  | first1 = Nikolai
  | last1 = Lobachevsky
  | authorlink = Nikolai Lobachevsky
  | title = Geometrishe Untersuchungen zur Theorie der Parellellinien
  | year = 1840}} (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
* {{Citation
  | last1=Löwenheim
  | first1=Leopold
  | author1-link=:en:Leopold Löwenheim
  | title=Über Möglichkeiten im Relativkalkül
  | year=1915
  | journal=Mathematische Annalen
  | issn=0025-5831
  | volume=76
  | pages=447–470
  | url=http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=GDZPPN002266121&L=1
  | doi=10.1007/BF01458217
  | issue=4}} (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.
*{{Citation
  |editor-last=Mancosu
  |editor-first=Paolo
  |editor-link=Paolo Mancosu
  |year=1998
  |title=From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in   the 1920s
  |publisher=Oxford University Press|publication-place=Oxford}}.
*{{citation
  |last1=Pasch
  |first1=Moritz
  |title=Vorlesungen über neuere Geometrie
  |year=1882}}.
*{{citation
  |first1=Giuseppe
  |last1=Peano
  |year=1889
  |title=[[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.&nbsp;83&nbsp;97.
* {{Citation
  |first1=Jules
  |last1=Richard
  |year=1905
  |title=Les principes des mathématiques et le problème des ensembles
  |journal=Revue générale des sciences pures et appliquées
  |volume=16
  |pages=541}} (French), reprinted in English translation as "The principles of mathematics and the problems of sets", van Heijenoort 1976, pp.&nbsp;142&ndash;144.
* {{Citation
  | last1=Skolem
  | first1=Thoralf
  | author1-link=Thoralf Skolem
  | title=Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen
  | year=1920
  | journal=Videnskapsselskapet Skrifter, I. Matematisk-naturvidenskabelig Klasse
  | volume=6
  | pages=1–36}}.
* {{Citation
  | last1=Tarski
  | first1=Alfred
  | author1-link=Alfred Tarski
  | title=A decision method for elementary algebra and geometry
  | publisher=[[RAND Corporation]]
  | location=Santa Monica, California
  | year=1948}}
*{{Citation
  | last1=Turing
  | first1=Alan M.
  | author1-link=A. M. Turing
  | title=Systems of Logic Based on Ordinals
  | year=1939
  | journal=[[Proceedings of the London Mathematical Society]]
  | volume=45
  | issue=2
  | pages=161–228
  | doi=10.1112/plms/s2-45.1.161}}
* {{Citation
  |first1=Ernst
  |last1=Zermelo
  |year=1904
  |title=Beweis, daß jede Menge wohlgeordnet werden kann
  |journal=Mathematische Annalen|volume=59|pages=514&ndash;516
  |url=http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=GDZPPN002260018&L=1
  |doi=10.1007/BF01445300
  |issue=4}} (German), reprinted in English translation as "Proof that every set can be well-ordered", van Heijenoort 1976, pp.&nbsp;139&ndash;141.
* {{Citation
  |first1=Ernst
  |last1=Zermelo
  |year=1908a
  |title=Neuer Beweis für die Möglichkeit einer Wohlordnung
  |journal=[[Mathematische Annalen]]
  |volume=65
  |pages=107–128
  |url=http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=GDZPPN002261952&L=1
  |doi=10.1007/BF01450054
  |issn=0025-5831}} (German), reprinted in English translation as "A new proof of the possibility of a well-ordering", van Heijenoort 1976, pp.&nbsp;183&ndash;198.
* {{Citation
  | last1=Zermelo
  | first1=Ernst
  | year=1908b
  | title=Untersuchungen über die Grundlagen der Mengenlehre
  | journal=Mathematische Annalen
  | volume=65
  | pages=261–281
  | url=http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=PPN235181684_0065&DMDID=DMDLOG_0018&L=1
  | doi=10.1007/BF01449999
  | issue=2}}.

== 外部リンク ==
* {{SpringerEOM|title=Mathematical logic|urlname=Mathematical_logic}}{{en icon}}
* [http://www.quantrelog.se/pvlmatrix/index_main.htm Polyvalued logic and Quantity Relation Logic]{{en icon}}
* ''[http://www.fecundity.com/logic/ forall x: an introduction to formal logic]''{{en icon}}, a free textbook by {{nowrap|P. D. Magnus}}.
* ''[http://euclid.trentu.ca/math/sb/pcml/ A Problem Course in Mathematical Logic]''{{en icon}}, a free textbook by Stefan Bilaniuk.
* Detlovs, Vilnis, and Podnieks, Karlis (University of Latvia), ''[http://www.ltn.lv/~podnieks/mlog/ml.htm Introduction to Mathematical Logic.]''{{en icon}} (hyper-textbook).
* In the [[Stanford Encyclopedia of Philosophy]]:
*: [http://plato.stanford.edu/entries/logic-classical/ Classical Logic]{{en icon}} by [[Stewart Shapiro]].
*: [http://plato.stanford.edu/entries/modeltheory-fo/ First-order Model Theory]{{en icon}} by [[Wilfrid Hodges]].
* In the [http://www.ucl.ac.uk/philosophy/LPSG/ London Philosophy Study Guide]{{リンク切れ|date=2021年10月}}:
*: [http://www.ucl.ac.uk/philosophy/LPSG/MathLogic.htm Mathematical Logic]{{リンク切れ|date=2021年10月}}
*: [http://www.ucl.ac.uk/philosophy/LPSG/SetTheory.htm Set Theory & Further Logic]{{リンク切れ|date=2021年10月}}
*: [http://www.ucl.ac.uk/philosophy/LPSG/PhilMath.htm Philosophy of Mathematics]{{リンク切れ|date=2021年10月}}

{{Mathematical logic}}
{{数学}}
{{Logic}}
{{Normdaten}}
{{DEFAULTSORT:すうりろんりかく}}
[[Category:数理論理学|*]]
[[Category:数学基礎論]]
[[Category:アルゴリズム]]
[[Category:計算機科学]]
[[Category:理論計算機科学]]
[[Category:論理学]]
[[Category:数学に関する記事]]