Alwe’s blog

Alwe(https://twitter.com/Alwe_Alwe)のブログ

順序数解析の文献紹介

順序数解析の文献について纏める.殆ど私の備忘録.

日本語で読めるもの

しっかりと証明が書かれているのはこれだけだと思います.内容としては8章の証明論の章で \mathsf{PA} \mathsf{ID}_1の順序数解析を行っている.しかし \mathsf{ID}_1の順序数解析の方法は工夫されているが,モチベーションなどの説明はほとんど書いてないので,そこは他の文献を参照しながらのほうが良いと思う.モチベーションに関しては同じく新井先生の

  • 新井敏康.Gentzenから始まる証明論50年.2018. researchmap.jp

が分かりやすかった.歴史的経緯や文献一覧もとても良く纏まってて参考になる.

教科書

  • Pohlers, Wolfram. Proof theory: The first step into impredicativity. Springer Science & Business Media, 2008.

多分これが一番新しい教科書だと思う.内容は基本的な可述的な \mathsf{PA}の順序数解析, \mathsf{ID}_1の順序数解析 \mathsf{KP}\omegaの順序数解析を行っていてとても導入に適した教科書だと思う. \mathsf{PA}の可証全域関数を求めたり,可述性の上限を求めたりしてはいるが,基本的な目的は順序数解析にあり,順序数解析の応用や関連する話題には詳しくない.

  • Troelstra, Anne Sjerp, and Helmut Schwichtenberg. Basic proof theory. No. 43. Cambridge University Press, 2000.

順序数解析というより,証明論の教科書.それゆえに, \mathsf{PA}の順序数解析程度しか話してない.しかし証明論の基本的な話題を網羅しているという点がおすすめできる.

  • Jean-Yves Girard. Proof Theory and Logical Complexity, Volume 1 of Studies in proof theory. Elsevier, 1987.

同じく順序数解析というよりは証明論の教科書だが,内容はTroelstra&Schwichtenbergより順序数解析,というより,伝統的な証明論よりと言える.Troelstra&Schwichtenbergと被る部分は殆どないので両方読むのも良いと思う.Schütteの \omega-規則に詳しい.あと竹内予想周辺の話題も豊富である.

幻の二巻目.本人がサイトで言及している通り,証明のチェックがなされていない,可換図式の矢が表示されない,文献一覧がない,など本としては致命的な欠陥があるが,Girardの研究について色々なことが載っている. \omega-完全性定理や, \Pi^1_2-logic,そしてDilatorとPtykesなどのGirardの研究したトピックに関して書かれている.が,私は読んでいない.

  • Takeuti, Gaisi. Proof theory. Vol. 81. Courier Corporation, 2013.

竹内外史の教科書.基本的な話題から,Gentzenによる \mathsf{PA}の無矛盾性証明などの基本的な話題から,竹内予想,無限論理の証明論, \Pi^1_1\text{-}\mathsf{CA}の順序数解析などの話題が書いてある.しかし順序数解析の証明は一番古い竹内の有限的手法であり,一番一般的な手法を学ぶのには向かない.逆に言えばその手法を学ぶのには最適である.が,私は半分くらいしか読んだことがない.なおDover Booksから出ているのは2000円で安いので良い.

  • Buchholz, Wilfried, and Kurt Schütte. Proof theory of impredicative subsystems of analysis. Vol. 2. Humanities Pr, 1988.

非可述的な二階算術の順序数解析.読んでないのでなにもわからないのですが,モチベーションが書いて無くて読みにくいと聞く.

  • Schütte, Kurt. Proof theory. Vol. 225. Springer Science & Business Media, 2012.

Schütteの古典的な教科書らしい.読んだことないです.

  • Jäger, Gerhard. Theories for admissible sets: A unifying approach to proof theory. Bibliopolis, 1986.

集合論の順序数解析や \mathsf{ATR}_0 \mathsf{KPi}_0の関係や \mathsf{KPi}の順序数解析について書いてある.ほとんど読んでいない.

  • Pohlers, Wolfram. Subsystems of set theory and second order number theory. Handbook of proof theory 137 (1998): 209-335.

PohlersのHandbook of Proof Theoryの項.内容としては順序数解析のモノグラフで証明も書いてあるところは書いてある.一通り順序数解析の初歩を学んだあとに読むと得られるものが多そう.しかしその証明や命題には間違いがあるのでそこらへんは新井先生の書評

  • Toshiyasu, Arai. "Book review: Wolfram Pohlers. Subsystems of set theory and second-order number theory. Handbook of Proof Theory, edited by Samuel R. Buss, Studies in Logic and the Foundations of Mathematics, vol. 137, Elsevier, Amsterdam etc., 1998, pp. 209–335 Bull". Symbolic Logic, 6 (2000), pp. 467-469.

  • Fujimoto, Kentaro. "Notes on some second-order systems of iterated inductive definitions and Π11-comprehensions and relevant subsystems of set theory." Annals of Pure and Applied Logic 166.4 (2015): 409-463. https://doi.org/10.1016/j.apal.2014.11.001

を並行して読むといい.が,私は後半を最近知ったのでまだ読み終わっていない.

  • Toshiyasu, Arai. Ordinal Analysis.

まだ未完成の新井先生の教科書.早く出版して欲しい.

論文

Buchholzの \Omega_\mu-規則

 \Omega_\mu-規則は教科書で書いてあるものが少ない(Buchholz&Schütte本には書いてあったと思う).よって適宜論文を読む必要がある.

  • Buchholz, Wilfried. "The Ωμ+1-rule." Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies. Springer, Berlin, Heidelberg, 1981. 188-233. https://doi.org/10.1007/BFb0091898

 \Omega_\mu-規則が導入された最初の論文.実は私はまともに読んだことはない.タイプライターツラスギ…….

 \Omega_\mu-規則を用いて \mathsf{ID}_\mu \Pi^0_2, \Pi^1_1-順序数解析を行い,ある種のヒドラゲームの停止性の独立性証明を行っている.特徴的なのは順序数を用いず,木の支配性による順序を用いている点.

Buchholzの規則を様相 \mu-計算に対する応用らしい.未読.

Buchholzの規則を代数的証明論の文脈で考えて,束のMacNeile完備化との関係を用いて \mathsf{ID}_\muに対する竹内対応を証明した論文.未読.

作用素に統御された証明

作用素に統御された証明は最近の順序数解析の主要な手法であるが,それなりに新しい手法なので古い教科書には書いていない場合がある.

作用素に統御された証明が最初に導入された論文.作用素に統御された証明を用いて \mathsf{KPi}の証明論的順序数の上限を示している.ノーテーションは最近の文献ともほとんどかわっておらず,説明も分かりやすいためおすすめ.

順序数解析の概説
  • Rathjen, Michael. "The realm of ordinal analysis." London Mathematical Society Lecture Note Series (1999): 219-280.

証明論的順序数の基本的性質から,順序数解析の応用までしっかり書かれている論文.とても参考になる.

証明論の概説と言いながら順序数解析に偏りがち.歴史や周辺の結果が色々と書かれている.

 \mathsf{KPi}以降の順序数解析

いつか書く