数理論理学の参考書

ここでは数理論理学に関する標準的な教科書を紹介する。数理論理学は主に基礎を学んだあと、計算理論やモデル理論、公理的集合論、証明論などの分野や非古典論理や算術の理論などに分化する。それらの教科書もまとめて紹介しよう。また書評には鴨浩靖先生の 一般書の書評や 教科書の書評、 仙台ロジックグループの書評が存在する。

読み物

著者名・タイトル	内容	書評
結城「数学ガール/ゲーデルの不完全性定理	数学ガールシリーズの一冊であり、ゲーデルの不完全性定理を目標にペアノの公理や $\epsilon$ ・ $\delta$-論法、対角線論法などのさまざまな数学の話題に触れている。	一見不完全性定理に関して無関係な話題などが多いように思われるが、実は不完全性定理のステートメントを理解するための伏線になっており、とても分かりやすく解説されている。また単純に物語としても面白いと思う。参考にしているのがゲーデルの原論文なので現代的に見れば、余分な仮定などはあるが、読み物としてはとても良く書かれている。
田中「山の上のロジック学園」	命題論理や一階述語論理などの入門的な話題から不完全性定理とその発展について書かれている。	これを読んで数理論理学を学ぶのは難しいと思うが、数理論理学にどんな話題があるのか、というのを知るには一見の価値がある本であると思う。また細かなトリビアなどが書かれていて読んでいて面白い本である。
照井「コンピュータは数学者になれるのか？」	再帰理論、不完全性定理、$\mathsf{P}$ vs $\mathsf{NP}$、カリー・ハワード対応など、コンピューターサイエンスよりの数理論理学の話題が書かれている。	最初に読む人が全てを理解するのは難しいところはあるが、数理論理学にどのような話題があるか、数理論理学の中での分野どうしの繋がりなどを知ることができる。もちろん、この本のみで数理論理学を学ぶことはできないが、どういう話題があるかということを理解するためには向いている。
スティルウェル「逆数学、定理から公理を『証明』する」	上述の本と比較してこれは逆数学という数理論理学の一分野に注目した本である。そのため数理論理学の一般的な話題についてはあまり書かれていない。	逆数学の本であるが、この本は数理論理学をあまり知らない人にも読める、具体的には簡単な微分積分を知っていれば十分に分かるようになっている。逆数学に興味があるのなら眺めてみるのも良いだろう

入門書(和書)

著者名・タイトル	難易度	内容	書評
前原「記号論理入門」	0	数理論理学を本格的に勉強する前に、論理学の基礎的な話などを学びたい場合に読むべき本。	非常にわかりやすく書かれている印象である。
戸次「数理論理学	2	命題論理、一階述語論理の基礎的な知識を丁寧に解説している。完全性定理やカット除去定理などの話題に触れている。	一般的な数理論理学のノーテーションが異なることや、意味論、特に理論のモデルなどの説明が分かりにくいと感じた。また演習問題に一切の解答がないことも難しさに拍車をかけているように感じる。しかし証明論の章はさまざまな証明体系をとても鮮やかに、分かりやすく解説していて、カット除去定理までの導入もとても丁寧に行っている。またこの本の前半の解説は著者の youtubeチャンネル にて公開されている。適宜参考にすると良いだろう。
鹿島「数理論理学」	1	数理論理学の基礎的な定理、完全性定理、不完全性定理、カット除去定理などや、非古典論理の意味論などにも触れていて基礎的な内容は全て抑えている。	とても分かりやすく、簡単な集合の話なども付録に書いているため数理論理学に入門する場合この本がおすすめである。しかしその分第二不完全性定理などのテクニカルに難しい議論は証明の概略に留めているため、そこを詳しく知りたい場合は他の教科書を参考にすべきである。
小野「情報科学における論理」	1	命題論理、一階述語論理に加えて様相論理、直観主義論理などの非古典論理、ラムダ計算などを扱っている。	とても分かりやすい。特に非古典論理に興味がある場合これを最初に手にとってみるのが良いのではないのだろうか。その代わり一階述語論理の完全性定理などは省略されている。
菊池「不完全性定理」	2	名前の通り不完全性定理を中心として書かれた本である。不完全性定理や、その応用、発展から理解するための基礎知識が書かれている。	不完全性定理の証明で省かれがちなコード化などが詳細に扱われているため、不完全性定理を学びたい人におすすめしたい。また不完全性定理に関する哲学的話題もあつかっている。
キューネン「数学基礎論講義」	2	公理的集合論を学ぶ前の基本的な知識、再帰的関数の理論、完全性定理などを扱っている。	公理的集合論を学ぶ前に読むのをおすすめしたい本である。その分証明論や不完全性定理などには殆ど触れていない。
田中「数学基礎論序説」	3	等式論理、一階述語論理、完全性定理、モデル理論、不完全性定理、Presburger算術や実閉体の決定可能性、算術のモデル理論、そして逆数学の様々な話題に触れている。	たくさんの話題が載っていて読んでいてとても面白い本である。しかし、その分証明は省略されているところも少なくはなく、また単純に難しい。算術のモデル理論や逆数学の本格的な話はこの本ほど丁寧書いてある和書は少ないように感じる。
新井「数学基礎論」	3	一階述語論理の基礎、完全性定理からモデル理論、再帰理論、集合論、証明論を全て網羅している。	基礎的なことを全て網羅をしていて、これほどたくさんのことが書かれている数理論理学の本はないと思われる。しかし紙面の問題から省略された証明や、モチベーションなどが殆ど書かれていなく、軽く入門しようという気持ちで読めるものではない。真剣に他の文献などの読み比べながらしっかりと読んでいかなければ難しいであろう。しかし、この一冊を押さえていれば、各分野の本格的話題に入っていけるほど書かれているので辞書としての使い方などもできるであろう。しかし非古典論理に関しては一切触れていない。
坪井明人「数理論理学の基礎・基本」	1		モデル理論に必要な数理論理学の初歩がコンパクトにまとまっている。
田中俊一「位相と論理」	1	命題論理と束論・モデル理論の初歩・Stone双対性	Boole代数を中心とする束論の基礎から入って、束論と命題論理との関わりやStoneの表現定理がわかりやすく書かれている。少し発展的な事項として、一階述語論理（特にモデル理論）の初歩やフレーム理論、圏論による双対性にも触れることができる。
Enderton「論理学への数学的手引き」		後述するEndetonの本の和訳である。

入門書(洋書)

著者名・タイトル	難易度	内容	書評
Enderton「A Mathematical Introduction to Logic」	2	一階述語論理の完全性定理や再帰理論、不完全性定理、二階述語論理などのことが書かれている。	海外ではポピュラーな教科書なんじゃないんだろうか。けっこう丁寧に一階述語論理が解説されていて二階述語論理について触れているところも魅力ですが証明論や集合論、モデル理論については殆ど触れていません。
Shoenfield「Mathematical Logic」	3	一階述語論理の基礎からモデル理論、集合論、再帰理論などの話題が書いてあります。	良くまとまっている教科書であり、証明の飛躍も少ない。しかし一昔前の教科書であるから現代的ではないところもある。証明論に関する記述はほとんどない。
Hils & Loeser「A First Journey through Logic」

計算理論

以下では有名な計算理論の教科書を紹介する。計算理論の書評に関しては木原先生による書評が詳しい

集合論

	内容	書評
キューネン「集合論―独立性証明への案内」	公理的集合論、無限組合せ論、構成可能集合、強制法などについて書かれている。	公理的集合論や強制法の入門書。公理的集合論、特に強制法などがわかりやすく、詳細になされている。一方、順序数や基数などの基本的な事実を知らないは仮定されているため、同著者の数学基礎論講義などで補う必要がある。また二章の無限組合せ論は位相や測度の基本的な事実は知っていることが仮定されている。また少し退屈に感じることもあるかもしれない。そういうときは3,4章などの先を読んでから、読み返しても良いだろう。ただ数理論理学をあまり知らない人も対象として意識しているためか、完全性定理、不完全性定理やモデルの定義などは概略に留められている。特に集合論の相対化によるクラスモデルと通常のモデル理論的なモデルの違いや関係性などのことが詳細ではなく、(特に数理論理学を中途半端に知っていると逆に)混乱しやすいように思う。この点は同著者の新しい集合論の教科書で改善されているが、和訳はなされていない。
Kunen「Set Theory」
Jech「Set Theory」
Drake「Set Theory, An introduction to large cardinals.」
Kanamori「The Higher Infinite」
Foremann&Kanamori ed「Handbook of Set Theory 1,2,3」
Schindler「Set Theory, Exploring Independence and Truth」
Moschovakis 「Descriptive Set Theory」
Krzysztof Ciesielski「Set Theory for the Working Mathematician (London Mathematical Society Student Texts)」

モデル理論

古典モデル理論

分野としてのモデル理論は、Shelahによる安定性理論を境にして様変わりした。数理論理学の初歩を学んだあとすぐに、Marker本などの安定性理論への入門を意図したテキストを読むのもよいが、古典モデル理論にも興味深い話題が多いのでぜひ学んでみてほしい。

著者名・タイトル	内容	書評
Chang & Keisler「Model Theory」		古典 of 古典その1, 1973年初版出版。下記のHodgesの本が出るまでの間、長らく古典モデル理論の辞書として愛用されてきた。飽和モデル・超積周辺の話題については今でも引用されることがままある。
Bell & Slomson「Models and Ultraproducts: An Introduction」		古典 of 古典その2, 1969年出版
Sacks「Saturated Model Theory」		古典 of 古典その3, 1972年初版出版
Hodges「Model Theory」	古典モデル理論の辞書。安定な理論に関わるトピックも多少記述あり。特に正則基数に対するnon-structure (many-model) theoremの証明が書かれている。	演習問題や章末の文献案内まで含めれば、1980年代までに知られていた古典モデル理論の結果を網羅的に取り扱っている。証明もそれなりに丁寧に書かれている。本の構成上かなり前の命題を参照することも多く、大著なので教科書として通読するのには向いていない。
Hodges「A Shorter Model Theory」		↑の本の内容から抜粋+αして入門書として再構成したもの。2020年時点で古典モデル理論を深く学ぶのに最も適した本。
Hodges「Building Models by Games」	モデル理論におけるゲーム的な構成（タイプ排除、Robinson強制など）
Prestel & Delzell「Mathematical Logic and Model Theory: A Brief Introduction」

入門から安定性理論の初歩まで

難易度も長さも様々だが、数理論理学の予備知識なしにモデル理論の初歩から安定性理論に入門することを目標にどの本も書かれている。各個人の興味や代数の知識に応じてMarkerかTent-Zieglerのどちらかを選ぶのが標準的。

	内容	書評
Marker「Model Theory, An introduction」	モデル理論の数学への応用、Morley の範疇性定理、安定性理論（$ \omega $-安定な場合に限る）。終盤7,8章では幾何的安定性理論にも触れられる。	3章を中心に代数的な具体例の記述が豊富で、随所で数学（特に古典代数幾何）への応用に触れられるのが特色。反面、仮想元・Ehrenfeucht–Fraïssé ゲーム・可算モデルに関する Morley の定理・many-model theoremなど、モデル理論のトピックとしては重要だが本書の以降の章ではほとんどor全く使われない脱線的話題も多く、若干構成に難がある。なお、上述の新井敏康著「数学基礎論」のモデル理論の章は本書を参考にして書かれているようで、Morley の範疇性定理まで一直線に進みたいのであれば新井本か後述の Tent-Ziegler を参照するとよい。著者による誤植訂正一覧
Tent & Ziegler「A Course in Model Theory」	前半1-5章はスタンダードな構成でモデル理論の初歩から Baldwin-Lachlan の定理・Morley の範疇性定理まで。後半6-10章は単純性理論および安定性理論の入門。	Marker と比較して、純粋モデル理論寄りで代数的具体例や応用的な話題は少ない。本書の後半では歴史的な順番にとらわれずに、安定性の一般化である単純性から導入するという大胆な構成が取られている。7章の単純性の記述は組合せ論的で難しい部分があるものの、従来のテキストよりも見通しよく安定性理論に入門することができる。また6.3節は証明のギャップが大きく注意が必要である。著者による誤植訂正一覧
Poizat「A Course in Model Theory」	前半1-10章は安定性理論に踏み込まない範囲の基礎的な内容。具体例の記述も多い。後半11-20章は安定性理論の入門。17章までで基礎的な道具立てをがっつり準備してから、18章で素モデル拡大の一意性やBaldwin-Lachlanの定理を示す。	入門書としては骨太なテキスト。ある程度モデル理論の基礎に慣れ親しんだ後に読むと、往復論法・タイプ排除・ランクなどの記述において違った視点が得られてよい。また上記2冊とは異なり、Lascar と Poizat による fundamental order を用いる流儀で forking を扱う（"Parisian approach to stability"）。諸々の技術的な道具立てをなるべく一般化して書く傾向があり、特に12章は難しいが、この章は論理式のindependence propertyを扱う際によく参照される。また基礎的な概念はほぼ網羅しているが、例外的に論理式のdividing/forkingは扱われていない。
Marcja and Toffalori「A Guide to Classical and Modern Model Theory」
坪井明人「モデルの理論」

その他のトピック

	内容	書評
van den Dries「Tame Topology and O-minimal Structures」

証明論

入門書

	内容	書評
Troelstra&Schwichtenberg「Basic Proof Theory」	証明論の基礎的な内容から派生の分野の導入まで広範に述べられている。前半の５章まではさまざまな証明体系のの同値性や各証明体系の比較などの基本的な内容、また証明論の基本定理たるカット除去定理とその応用について述べられている。６章は自然演繹の正規化定理、７章で導出原理、８章で圏論的論理、９章で非様相論理、線形論理、１０章で算術の証明論、１１章で直観主義二階命題論理の正規化などの発展的話題の基礎について書かれている。	５章までの内容を読んだら各自興味があるところを読み、参考文献などから先に進む、また全て読むことで証明論全体を鳥瞰することに向く本であろう。文章もとても平易で簡単であり、丁寧に書かれている。基本的なことはだいたい書いてあるが、発展する内容は基礎の基礎しかかかれていないため別個他の文献を読む必要がある。
Girard「Proof Theory and Logical complexity」	タイトルの通り論理的複雑性、算術的階層や解析的階層などから証明論を見る本となり不完全性定理からカット除去定理、竹内の基本予想、順序数解析の基礎などについて歴史とともに解説している。	順序数解析や算術の証明論を勉強したい人が読むと面白いと思う。またところどころに話題からそれて小咄が入ったり、著者の考えが入っていたりするがそこを含めて私は面白いと思うが人を選ぶかもしれない。非可述的な理論に対する順序数解析については一切書かれていないため、そこは別の本で補う必要がある。
Negri「Structual Proof Theory」

順序数解析

	内容	書評
Pohlers「Proof Theory, the first step into impredicativity」	非可述的体系の順序数解析の入門書	順序数解析の前の順序数や計算可能性理論からの準備に始まり、Peano算術の順序数解析、可述性について、帰納的定義の順序数解析、Peano 算術の局所的可述性を用いた可証再帰関数の分類、Kripke–Platek集合論の順序数解析などの現代的な順序数解析への入門書として一番適切であると思う。章立てや証明の本質を分かりやすくするための工夫などがしっかりされていて、議論が単調で辛いところは多々あったが面白い本である。
Pohlers「Proof Theory, An Introduction」	Peano算術の順序数解析、可述性について、帰納的定義の順序数解析など	前述のPohlersの本の元になった本。いま読むなら上記の新しいものを読もう。
Takeuti「Proof Theory」	古典。カット除去、算術の無矛盾性証明、竹内の基本予想、無限論理の証明論、二階算術の部分体系の無矛盾性、順序数解析など。	証明論、及び順序数解析の入門書であるが、順序数解析パートに限って言えば証明の手法が有限証明図に対して順序数を割り当てて証明図を変形するというGentzenとTakeutiの手法を用いていて現代的な局所可述性や $\Omega_\mu$-規則を用いた証明と比べて組合せ論的に複雑で分かりづらいと思う。また使用している順序数表記も順序数図形というもので、現代的には証明論的順序数の下限証明とでも言うべき到達可能性証明のパートはとても難しいと思う。しかし竹内外史の研究やBuchholzなどによる有限証明図の変換は無限の証明図のコードとなっているという事実、新井による有限的手法による順序数解析などの話題などに発展するため、興味があるなら読んで視るのも良いかもしれない。
Buchholz & Schütte 「Proof theory of impredicative subsystems of analysis」
Schütte「Proof Theory」
Jäger「Theories for admissible sets」
Arai「Ordinal Analysis with an Introduction to Proof Theory」	順序数解析や算術の証明論の教科書。色々な証明体系のカット除去定理、そしてその応用から始まり、Peano算術と超限帰納法の公理系の順序数解析、Turingジャンプの反復による体系の順序数解析と整列性原理、帰納的定義と集合論と二階算術の翻訳、非可述的体系の順序数解析など、算術や集合論などの理論に対する証明論さまざまな話題、最近の研究を含む、などが載っている。	基礎的な数理論理学の基礎は既知のものとして、話が展開されるため、予め同著者の「数学基礎論」などを読まれると良いだろう。最近の研究を含む多様な結果が華麗に展開されているが、紙面の問題かペースがとても早く展開されていく。特に証明の行間が少ないわけではなく、モチベーションの説明も少ない。よってこの本を読むのと並行に、章末に記載されてる出典の論文などを読むと分かりやすいと思う。順序数解析の入門書としては前述のPohlersを読んだほうが分かりやすい。しかし内容が被るところは少なく、Pohlersを読んだ後にこの本を読めば理解は広がるのではないかと思う。
Girard「Proof Theory and Logical complexity2」	未出版である幻の二巻目、Girard の研究についてまとまっている。	図式の矢印が表示されない、参考文献リストがない、証明が正しいか確かめられていないなど数学書として致命的であるが、それを考慮しても独創的かつ他の教科書では取り上げられないトピックが挙げられている。
Buchholz, Feferman, Pohlers and Sieg「Iterated Inductive Definitions and Subsystems of Analysis」

型理論、ラムダ計算

	内容	書評
Girard「Proofs and Types」
Barendregt「Lambda Calculus with Types」
「Homotopy Type Theory」
Pierce「型システム入門」	プログラム言語理論のための型理論の教科書．OCaml による実装が書いてある章もいくつかある．第I部では型なしλ計算を扱っている．第II部においては単純型の理論を扱っている．第III部では部分型付けの理論を扱っている．第IV部においては再帰型の理論を扱っている．第V部においては多相型を扱っている．第VI部においては高階型を扱っている．	実装寄りの型理論の本として定評のある本．日本語版も出版されている．日本語版はいくつかの誤植や演習問題の出題ミスなどが訂正されており，今から新しく買うのであれば，日本語版の購入をオススメする．
龍田真「型理論 (レクチャーノート／ソフトウェア学　１) 」

線形論理

	内容	書評
Troelstra「Lectures on Linear Logic」
Girard「The Blind Spot」

限定算術

	内容	書評
Buss「Bounded Arithmetic」
Krajíček「Bounded Arithmetic, Propositional Logic and Complexity Theory」
Krajíček「Proof Complexity」

ハンドブック

	内容	書評
Buss ed.「Handbook of Proof Theory」

算術の理論

	内容	書評
Hájek & Pudlák「Metamathematics of First Order Arithmetic」
Kaye「Models of Peano Arithmetic」
Kossak & Schmerl「The Structure of Models of Peano Arithmetic」

その他の話題

	内容	書評
Kohlenbach「Applied Proof Theory」
Ono「Proof Theory and Algebra in Logic」

逆数学

	内容	書評
Simpson「Subsystems of Second Order Arithmetic」
Hirschfeldt「Slicing the Truth」
Reverse Mathematics Zoo	逆数学動物園