数理論理学（）は数学の分野であって、形式論理の数学への応用の探求ないしは形式論理の数学的な解析を主たる目的とする。局所的には数理論理学は超数学、数学基礎論、理論計算機科学などと密接に関係している。数理論理学の共通な課題としては形式体系の表現力や形式証明系の演繹の能力の研究が含まれる。数理論理学はしばしば集合論、モデル理論、再帰理論、証明論の4つの領域に分類される。これらの領域はロジックのとくに一階述語論理や定義可能性に関する結果を共有している。計算機科学（とくに）における数理論理学の役割の詳細はこの記事には含まれていない。詳細はを参照。この分野が始まって以来、数理論理学は数学基礎論の研究に貢献し、また逆に動機付けられてきた。数学基礎論は幾何学、算術、解析学に対する公理的は枠組みの開発とともに19世紀末に始まった。20世紀初頭、数学基礎論は、ヒルベルトのプログラムによって、数学の基礎理論の無矛盾性を証明するものとして形成された。クルト・ゲーデルとゲルハルト・ゲンツェンによる結果やその他は、プログラムの部分的な解決を提供しつつ、無矛盾性の証明に伴う問題点を明らかにした。集合論における仕事は殆ど全ての通常の数学を集合の言葉で形式化できることを示した。しかしながら、集合論に共通の公理からは証明することができない幾つかの命題が存在することも知られた。むしろ現代の数学基礎論では、全ての数学を展開できる公理系を見つけるよりも、数学の一部がどのような特定の形式的体系で形式化することが可能であるか（逆数学のように）ということに焦点を当てている。"Handbook of Mathematical Logic" は数理論理学を大まかに次の4つの領域に分類している：それぞれの領域は異なる焦点を持っているものの、多くの技法や結果はそれら複数の領域の間で共有されている。これらの領域を分かつ境界線や、数理論理学と他の数学の分野とを分かつ境界線は、必ずしも明確ではない。ゲーデルの不完全性定理は再帰理論と証明論のマイルストーンであるだけではなく、様相論理におけるを導く。また集合論や逆数学における独立性証明の基本的な道具とされる。強制法の手法は集合論、モデル理論、再帰理論のほか直観主義的数学の研究などでも用いられる。圏論の分野では多くの形式公理的方法を用いる。それにはの研究も含まれる。しかし圏論は普通は数理論理学の下位分野とは見做されない。圏論の応用性は多様な数学の分野に亙っているため、ソーンダース・マックレーンを含む数学者らは、集合論とは独立な数学のための基礎体系としての圏論を提案している。これはトポスと呼ばれる古典または非古典論理に基づく集合論の成す圏に類似の性質を持つ圏を基礎に置く方法である。言葉を、代数学におけると同様に文字や記号の列で表して、その変換について研究するいわゆる記号論理学、数理論理学の発祥は、19世紀のジョージ・ブールによる「論理代数」、ゴットロープ・フレーゲの書『概念記法』に見ることができる。前者は命題論理、後者は述語論理の原型である。数学自体を数学によって研究する数学基礎論は、数理論理学なしにはあり得ないものである。たとえば数理論理学の一分科である命題論理では、「風が吹いた」という観念を文字 "A" で表し「桶屋が儲かる」という観念を 文字 "B" で表したとき、「風が吹いたならば桶屋が儲かる（風が吹けば桶屋が儲かる）」という観念を "A" ⇒ "B" などと表す。ここに、記号 ⇒ は「前の概念が正しければ後ろの概念も正しい」ということを表し、"A" ⇒ "B" を「"A" ならば "B"」と読む。数理論理学の体系は、論理式を構成する文法及び推論規則によって構成される。上記文法及び推論規則の違いにより、命題論理・述語論理・様相論理等々の体系が存在する。命題論理と述語論理を古典論理とし、その他の論理を非古典論理とすることがある。命題論理では、論理式は原子論理式およびによって定められる。具体的には、論理式 "A

出典:wikipedia