数理論理学

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

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

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

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

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

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

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

### 初期の歴史

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

### 19世紀

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

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

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

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

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

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

19世紀中頃、ユークリッドの幾何学の公理の欠陥が世に知られるようになった (Katz 1998, p.&nbsp;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.&nbsp;445)、*プリンキピア・マテマティカ* は20世紀の最も影響力のある研究のひとつと見做されている。

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

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

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

1931年、ゲーデルは**'を出版した。ここでは、十分に強く、実効的な一階理論が不完全（完全性定理のそれとは異なる意味である）であることを示されている。この結果は[[ゲーデルの不完全性定理]]として知られ、数学の公理的基礎の厳密な限界を示すものであり、ヒルベルト・プログラムに大きな打撃を与えた。これは算術の無矛盾性をいかなる算術の形式理論においても証明できないことを示している。しかしながら、ヒルベルトは、不完全性定理の重要性を、あるときまで認めなかった。

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

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

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

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

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


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

=== 一階述語論理 ===

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

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

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

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

最もよく調べられている無限論理は <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>

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

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


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

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

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

== 集合論 ==



== モデル理論 ==

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

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

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

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

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

== 再帰理論 ==

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

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

一般再帰理論は再帰理論の諸概念をもはや有限ではないような計算へと拡張する。そこには高階の型の計算可能性の研究ややなどの分野を同様に含む。

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

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

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

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

== 証明論と構成的数学 ==

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

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

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

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

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

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

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

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

== 数学基礎論 ==



== 関連項目 ==



* [[数学基礎論]]
* [[計算可能性理論]] - [[計算科学]]
** [[計算論]]／計算理論
* [[再帰理論]]
* [[集合論]]
* [[証明論]]
* [[非古典論理]]
* [[モデル理論]]
* [[:Category:研究の計算分野]]
** [[計算言語学]] - [[計算論的哲学]]

== 脚注 ==
=== 注釈 ===

=== 引用 ===


==参考文献==

=== 学部教科書 ===
*
* .
* .
* .
* .
* .
*.
* .
* .
* .
* .
* 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]]

=== 大学院教科書 ===
* .
* .
* .
* .
* .
* .

=== 研究論文、モノグラフ、教科書、サーベイ ===
* .
* .
* , 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]
*. [http://links.jstor.org/sici?sici=0002-9890(200011)107%3A9%3C844%3ABCED%3E2.0.CO%3B2-L JSTOR]
*. [http://links.jstor.org/sici?sici=1079-8986%28200112%297%3A4%3C441%3ATRTMLI%3E2.0.CO%3B2-O  JStor]
* , to appear. [http://www.ams.org/tran/0000-000-00/S0002-9947-07-04297-3/home.html Electronic posting by the journal]
* .
* .
*.
*.
*. [https://www.ams.org/notices/200106/fea-woodin.pdf PDF]

=== 古典的な論文、教科書、論文集 ===
*, reprinted in van Heijenoort 1976, pp.&nbsp;104&ndash;111.
*. English translation of title: "Consistency and irrational numbers".
* 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.
* (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.
* , reprinted in English translation in Gentzen's *Collected works*, M. E. Szabo, ed., North-Holland, Amsterdam, 1969.
*. English translation of title: "Completeness of the logical calculus".
* . English translation of title: "The completeness of the axioms of the calculus of logical functions".
* , see [[On Formally Undecidable Propositions of Principia Mathematica and Related Systems]] for details on English translations.
*, reprinted in English translation in Gödel's *Collected Works*, vol II, Soloman Feferman et al., eds. Oxford University Press, 1990.
*
*, English 1902 edition (*The Foundations of Geometry*) republished 1980, Open Court, Chicago.
*. 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.
* .
*  (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
*  (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.
*.
*.
* (Latin), excerpt reprinted in English stranslation as "The principles of arithmetic, presented by a new method", van Heijenoort 1976, pp.&nbsp;83&nbsp;97.
*  (French), reprinted in English translation as "The principles of mathematics and the problems of sets", van Heijenoort 1976, pp.&nbsp;142&ndash;144.
* .
* 
*
*  (German), reprinted in English translation as "Proof that every set can be well-ordered", van Heijenoort 1976, pp.&nbsp;139&ndash;141.
*  (German), reprinted in English translation as "A new proof of the possibility of a well-ordering", van Heijenoort 1976, pp.&nbsp;183&ndash;198.
* .

== 外部リンク ==
* 
* [https://www.quantrelog.se/pvlmatrix/index_main.htm Polyvalued logic and Quantity Relation Logic]
* *forall x: an introduction to formal logic*, a free textbook by .
* *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