予備知識パートです．完全性定理や再帰的関数について知っていることが求められています．おそらくこの記事を読んでいる人には不要かもしれませんが，それぞれの文献を紹介します．完全性定理を中心としたロジックの基礎知識は例えばエンダートン，嘉田勝[訳]``論理学への数学的手引き''の2章や，菊池誠``不完全性定理''の3章などが良いかと思います．再帰的関数については当分この0章の知識だけで十分な気もしますが，篠田寿一``帰納的関数と述語''や，新井敏康``数学基礎論増補版''2,6章を読むというのはありだと思います． 一点注意です．Models of Peano Arithmeticにおいてrecursive functionの定義に全域性が含まれていますが．おそらく現代での一般的なrecursive functionの定義は，0章にある花文字のCの方です． また，以下はこの本に限らず，ロジックを学ぶ上で必須だと思います．
イントロダクションパートです．超準モデルのコンパクト性定理による構成は今後もよく使うので慣れておくと良いと思います．
PA^-という離散全順序間の非負部の公理系がΣ_1完全性を持つこと（系2.9）がゴールです． その他系2.8や定理2.7も以降よく使います．構造の同型など，0章に載っていない定義については先ほど挙げた和書か，田中一之[編],``ゲーデルと20世紀の論理学②完全性定理とモデル理論'' などにあります．
再帰的（部分）関数とΣ_1論理式の対応を3.1節で扱い，3.2節で第一不完全性定理を示します． 3.1節は丁寧に証明も書かれていて分かりやすかった記憶があります．特に，3.1節の定理3.5はポストの定理とよばれ，再帰理論の重要な定理であり，（二階算術上の）逆数学などを学ぶ上でも必須となりますのでここで証明を丁寧に追っておくとよいと思います．3.2節では本格的に不完全性定理について議論する，というよりは，以降で道具として使うために示したという趣があるので，詳しく不完全性定理について知りたいなら他の文献を読んだ方がよいと思います．もっとも，超準モデルを構成するための道具として以降で使う分には3.2節の内容で支障ないと思います． 一点，ここのゲーデル数の説明は個人的には謎でした．大分後ですが，9章において体系内でゲーデル数を定義するので，ここで分からなくとも後の9章で明瞭な定義が与えられるので一旦飲み込んで先に進むとよいと思います．
4.1節は帰納法公理とそのバリエーションで，4.2節が関数・関係記号の追加についてです． 4.1節は若干証明が回りくどい気がします．そこまで難しくも長くもないので，後ですっきりした証明を自分で付けてみるのはよい演習になると思います，4.2節は少し変な箇所があるように思います．ここの修正として，こちらの補題2.4でよいと思います．このPDFは筆者の卒論の一部を切り抜いて修正したものであり，self-containedではありませんのでその点はご了承ください．
（体系内で）有限列をコードするゲーデルのβ関数を手に入れるのが目標です．難しいというより，単調でやや面倒くさかったです．ただ汎用性は高く今後も結構使います．なにより，（一階or二階）算術や計算可能性を学ぶ上で有限列のコーディングは避けて通れないので，まだ一度もコーディングの関数を扱ったことがないならここで片してしまうことを推奨します． また以降で便利だと思いますので，原子再帰法や最小化を用いて定義される関数を言語に追加する方法を補足資料という形でおいておきます． ゲーデルのβ関数と言語の追加について
ペアノ算術の（超準）モデルの構造についてです． 6.1節で示すoverspillが個人的に好きです．汎用性が高く，都合のよい性質を持つ超準元を作りたいときによく使います．6.2節はPAの超準モデルの順序型を調べます．ここで往復論法（back-and-forth method）が出てきますが，モデル理論でよく使われる証明方法であり，12章でも使うので慣れておくとよいと思います．
採集公理と共終拡大です． 7.1節は有界量化がPAのもとで論理式の階層に影響を及ぼさないことを学びます． 7.2節は恥ずかしながら正直あまり記憶にないです．問7.8は*は付いていませんが，補題14.14のn=1で使える（p.213ではcollection axiomsといってこの問7.8の論理式を指している（？））ので示しておくとよいです．明示はされていませんが，この問7.8の論理式を無限鳩ノ巣（っぽいもの）だと考えれば証明の方針が立つとおもいます．
8.1節が素モデルとタイプの話で，8.2節のメインは「任意のPAのモデルは真の保存的終拡大をもつ」を示すことです． 8.1節のタイプの定義は普通のモデル理論のそれと多少異なっているので注意が必要です． 素モデルの構成手法はあとでも使います． 8.2節は個人的にかなり苦しみました．特に補題8.7が難しかったと記憶しています．というわけでこちらが行間を埋めたものです．
PA内部でのゲーデル数の取り扱いについてです．いろいろ上手くいかない定義があり，証明も後半かなり省略されているので補足PDFを作りました．9章の行間埋め
PAの部分体系，主にBΣ_nについてです．ここは証明も分かりやすく，結構面白かった気がします．ただ，p.135で定義した「wの二進展開のx桁目が1である」を表す論理式について細かい議論をしようとすると面倒くさかったのでPDFで補足します．[TO DO]
再帰的飽和構造の基礎とテンネンバウムの定理についてです． まずSSy(M)の定義において(x)_y=zとしている箇所は[x]_y=zが妥当だと思います．たとえば標準構造におけるSSy(N)を考えてみてください． p.148で定義した再帰的言語ですが，それに関連したp.149の10行目For exampe におけるSの説明はよく分かりませんでした．またExercise 11.9は多分成り立たないような気がしますし，少なくとも14章までは解かなくとも問題ありませんでした． 命題11.4は（算術ではない）モデル理論の命題で，証明に選択公理を何度か使うのでこれまでとのギャップに驚きましたが，細かな添え字に気をつければなんとかなりました．
ここではフリードマンの埋め込み定理とその周辺です． 往復論法を使います．これは筆者も後で気づきましたが， 田中 一之, ``数学基礎論序説 数の体系への論理的アプローチ''にも（細部は見ていませんが）同じような証明が載っていましたので，そちらを読むという手もあります．問12.2は定理14.7で使いましたが，少なくともここでは問題文にある「short-Π_{n+1}再帰的飽和」の条件は「再帰的飽和」で考えて問題ないです（15章で問の形ママで使っていたらすみません）． 12.2節はそのバリエーションで，再帰的タイプの実現などの細かい議論が少し退屈でしたが，定理12.7はなかなか驚く結果で面白いと思います．ただ，証明の英語が若干分かりにくいので，覚えていたらPDFの補足資料をアップロードします．
スコット集合とよばれる計算論的に興味深い自然数の集合族についての章です．これは二階算術を学んでいる，または今後学ぶ予定の方へのコメントですが，スコット集合とはつまりWKL_0のωモデルのことです． この章の前半部分の木のコード化などは若干面倒ですが，個人的には先に退屈な部分は全部済ませておきたかったので，λやρはPA^-の再帰的関数の表現可能性で考えるのではなく，ダイレクトにIΣ_1で可証再帰性を証明して言語に追加して考えました．おそらくこちらの方が使い勝手もよく快適かと思います．ただ，その場合細かい証明が面倒くさいのでPDFをおいておきます．もっとも，木のコード化などは退屈なわりに得られるものが少ないので飛ばして先を読んだ方がよいとは思います． この章全体を通して証明が少し分かりにく（いと感じるか否かは似たような議論に慣れているかに依存します）く感じました．特に定理13.6は言語L_{∞}の構成がよく分からず難しかったです（解説のPDF[TO DO]）．またこの定理の最後でMがX-飽和であるのを示す際，この本の完全タイプの定義では上手くいかなかった記憶があります．そのため完全タイプの定義は標準的なものを採用して考えた方がよいと思います． 算術化された完全性定理（定理13.13）はよく分かりませんでした．
パリス・ハーリントン原理と金森・マカルーン原理を，indicatorを用いてPAから独立であることを示します． 14.1節は証明不可能性のアイデアです．14.2節は特に定理14.7（なぜか11.7とタイポされています）のp.202,it is straightforward to check that M' satisfies the following for all e \in N.が理解できませんでした（が，14.3節を読む分には支障はありません）．14.3節はコード化が完全に読者に投げられていますので少し苦労しましたが，たとえば汎用性も考えて素朴集合論を体系内でそれらしく展開するのが楽かと思います．
またY_{PH}の定義はテキストのものでは上手くいくと思えず，少し改変した定義で示しました． そこで14.1,14.3節の内容を再構成したのが次です．パリス・ハーリントン原理と金森・マカルーン原理がPAから独立であることのモデル理論を用いた証明．
未読です．ぜひあなたが解説を作って下さい．そしてもしよければ見せてください．
ホームへ戻る