2023-12-01

命題論理のカット除去について

一階述語論理におけるカット除去定理のアルゴリズムがカルマールの意味で非初等再帰的であることは有名であるが，命題論理ではどうだろうか？実は命題論理に関しては、証明体系を工夫することにより初等再帰的なアルゴリズムを得ることができる。これから従う簡単な帰結として命題論理の無矛盾性は $\mathsf{I}\Delta_0(\mathrm{exp})$ というとても弱い算術で証明可能であるということが挙げられる。

drive.google.com

2020-06-16

順序数解析の文献紹介

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

日本語で読めるもの
教科書
論文

日本語で読めるもの

新井敏康．数学基礎論．岩波書店．2016．

しっかりと証明が書かれているのはこれだけだと思います．内容としては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$ -規則に詳しい．あと竹内予想周辺の話題も豊富である．

Jean-Yves Girard. Proof Theory and Logical Complexity, Volume 2. unpublished. Archives de Jean-Yves Girard (4)

幻の二巻目．本人がサイトで言及している通り，証明のチェックがなされていない，可換図式の矢が表示されない，文献一覧がない，など本としては致命的な欠陥があるが，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$ -規則が導入された最初の論文．実は私はまともに読んだことはない．タイプライターﾂﾗｽｷﾞ……．

Buchholz, Wilfried. "An independence result for (Π^1_1-CA)+ BI." Annals of Pure and Applied Logic (1987): 131-155. https://doi.org/10.1016/0168-0072(87)90078-9

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

Jäger, Gerhard, and Thomas Studer. "A Buchholz rule for modal fixed point logics." Logica universalis 5.1 (2011): 1-19. https://doi.org/10.1007/s11787-010-0022-1

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

Terui, Kazushige. "MacNeille Completion and Buchholz’Omega Rule for Parameter-Free Second Order Logics." Computer Science Logic. 2018.https://doi.org/10.4230/LIPIcs.CSL.2018.37

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

作用素に統御された証明

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

Buchholz, Wilfried. "A simplified version of local predicativity." (1992): 117-147. https://doi.org/10.1017/CBO9780511896262.006

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

順序数解析の概説

Rathjen, Michael. "The realm of ordinal analysis." London Mathematical Society Lecture Note Series (1999): 219-280.

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

Rathjen, Michael, and Wilfried Sieg. "Proof theory." (2018). https://plato.stanford.edu/entries/proof-theory/

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

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

いつか書く

2019-12-31

ω-無矛盾性と1-無矛盾性について

tex:\omega

第一不完全性定理でGödelは $\omega$ -無矛盾性を仮定していたが $1$ -無矛盾性で十分であることが知られている．ここでどのくらい $\omega$ -無矛盾性と $1$ -無矛盾性に差があるのか考察した．

drive.google.com

2019-12-25

一階算術の部分体系の順序数解析

数学

f:id:Alwe:20191225232625p:plain この記事はMathematical Logic Advent Calendar 最終日の記事です. adventar.org

　この記事では書いたpdfの解説を行いたいと思います．pdfの方ではモチベーションとかそういうものを省いたのでそういうことを中心に話していきたいと思います．

　まずまだ未完成なのですがpdfの方はこちらになります． drive.google.com self-containedにしたかったんですがまだ前提知識の章を書き終えてません. とくに順序数について全く書いていません．

順序数解析とはなにか？
- 数理論理学とは
- Gentzenの定理と証明論的順序数
制限された帰納法の順序数解析
Mathematical Logic Advent Calendarについて

順序数解析とはなにか？

数理論理学とは

　多分ほとんどの人が知らないと思うので順序数解析という分野のお話をします．数学に於いて私達は「証明」をして定理を示していくと思います．そこで「どんな定理なら証明できるだろうか」という疑問が当然湧くと思います．そこで数理論理学(mathematical logic)と呼ばれる数学に於ける分野が活躍します．数理論理学という分野では普段扱っている数学そのものを形式化して，それを研究するというのがしばしば行われます．特に数学に於ける「証明」そのものを形式化して，研究する分野を証明論(proof theory)と言います．順序数解析(ordinal analysis)は，その証明論の一分野なのですが順序数解析では主に公理系の強さを順序数を用いて調べます．

　ところで公理系とはなんなんでしょうか．有名な例としては集合の公理系 $\mathsf{ZFC}$ などが存在します，が今は自然数が扱える程度の弱い公理系を考えてみます．以下の公理系を $\mathsf{Q}$ とします*1．

$x+1\neq 0$
$x+1=y+1\to x=y$
$x+0=x$
$x+(y+1)=(x+y)+1$
$x\times 0=x$
$x\times (y+1)=(x\times y)+x$

ただしこの式の中の $\to$ は「ならば」という意味を持ちます．ここで $2:=1+1,\ 3:=(1+1)+1,\ 4:=( (1+1 )+1 )+1,\ldots$ といつもの自然数を定義しましょう． $\mathsf{Q}$ では小学校１，２年生くらいの簡単な足し算，掛け算ができます．例えば $2+3=5$ は以下のように計算できます．

$\begin{aligned} 2+3 &=( 1+1 )+( (1+1 )+1 ) \\ &=( (1+1 )+ (1+1 ) )+1 \\ &=( ( (1+1 )+1 )+1 )+1 \\ &=5 \end{aligned}$

では以下の足し算は交換法則を満たす，すなわち

$(\forall x)(\forall y)[x+y=y+x$ ]

は示すことが可能でしょうか．ここでの $\forall$ は「任意の」という意味を持ちます．実は $\mathsf{Q}$ からは証明できないことが知られています．では $\mathsf{Q}$ にどんな公理があれば示せるでしょうか．皆さんも高校で習ったことがあると思う，あの証明方法が足りないのです．そう，数学的帰納法です．数学的帰納法は以下のように表せます．

$\varphi(0)\land (\forall x)[\varphi(x)\to\varphi(x+1) ] \to \forall x \varphi(x)$

ただしすべての論理式 $\varphi$ に対して仮定します*2．この数学的帰納法があれば交換法則などの様々な命題を示すことができます． $\mathsf{Q}$ に帰納法を加えた公理系を $\mathsf{PA}$ と言いましょう. この $\mathsf{PA}$ という公理系はそれなりに強いことが知られています．実際，似たような少し拡張した公理系である $\mathsf{ACA}_0$ では古典的な解析学の定理をほとんど示せることが知られています．ここで $\mathsf{Q}$ と $\mathsf{PA}$ の違いは帰納法にあったことを覚えておきましょう．

Gentzenの定理と証明論的順序数

　ところで順序数というものを知っているでしょうか．順序数は大雑把に言うならば，整列順序の代表みたいなものです．整列性には「任意の部分集合が極小元を持つ」という整礎性と呼ばれる性質が仮定されます．実は整礎性はある種の帰納法と見做せることが知られています*3．この超限帰納法は順序数が大きくなるに連れて複雑になっていきます．ドイツの証明論の研究者であったGerhard Gentzenは1936年に以下の定理を証明しました．

$\mathsf{PA} + \mathsf{TI}(\varepsilon_0) \vdash \mathsf{Con}( \mathsf{PA} )$

これは簡単にいうと「 $\varepsilon_0$ と呼ばれるそれなりに大きな順序数までの帰納法を用いて $\mathsf{PA}$ の無矛盾性が証明できる」という定理です．この定理とGödelの第二不完全性定理から $\varepsilon_0$ までの帰納法は $\mathsf{PA}$ で示せないことが分かります．またGentzenは $\varepsilon_0$ より小さな順序数までの帰納法は $\mathsf{PA}$ で示せることも示しました．このことから $\varepsilon_0$ は $\mathsf{PA}$ の限界を測っているということが予想できそうです．この観察から一般の公理系 $T$ の証明論的順序数というのを以下のように定義します*4．

順序数 $\alpha$ が公理系 $T$ の証明論的順序数であるとは $\alpha$ までの帰納法が $T$ から証明できない最小の順序数であることである．

このように定義された証明論的順序数を求める分野が順序数解析です．

制限された帰納法の順序数解析

　この記事で順序数解析をした公理系は $\mathsf{Q}$ より強く $\mathsf{PA}$ より弱い $\mathsf{I} \Sigma^0_n$ と呼ばれる公理系たちです．この公理系は $\mathsf{PA}$ の帰納法の公理を $\Sigma^0_n$ に制限したものになります．ではどうやって順序数解析をするのでしょうか．簡単に言えば上下から抑え込んではさみうちの原理を使うみたいに示します．Boundedness Theoremという定理から証明論的順序数は無限の長さを持つ体系の正規形である証明の長さで抑えられることが知られています．まず $\mathsf{I} \Sigma^0_n$ を無限の長さを持つ体系に埋め込んでそこで証明を正規形に変形する，カット除去をすることでBoundedness Theoremを使えるようにします．簡単なカット除去は以下にあります． alwe-logic.hatenablog.com 下から抑えるのは頑張って帰納法を示すことでやります． $\mathsf{PA}$ の順序数解析とは違い，繊細な証明図の操作をしなくてはならないところが難しかったです．

Mathematical Logic Advent Calendarについて

今年，私はこのような企画をたちあげたのですが，まさかのカレンダーが全部埋まってとても驚きました． f:id:Alwe:20191225233720p:plain しかもみなさんしっかりと書いてくれたので毎日新しい記事を楽しみに待ってました．

頭川るいさん
カワイシンさん
ジタさん
でぃぐさん
p進大好きbotさん
名前OSさん
ウッ鵜さん
Xさん
y.さん
飛車丸さん
しらそらさん
kbisさん
tomoさん
hexirpさん
はかりさん
Yasuda_Yasutomoさん
七果さん
そくらてすさん
YukihiroMasuokaさん
i.e.さん

本当にありがとうございました！！

*1:厳密には等号に関する公理も必要となります

*2:これを公理図式と言います．

*3:超限帰納法と言います．

*4:厳密な定義はもっと面倒です．

2019-12-05

「帰納的に定義する」とはなにか？

数学

この記事は日曜数学 Advent Calendar 2019 5日目のものです.

adventar.org

数学に於いて帰納的に定義することはなんどかありえる. そこで帰納的に定義することそのものを抽象化しその性質を調べることは重要であるように思える. 今回は帰納的定義の理論の初等的な結果を紹介する.

drive.google.com

2019-12-02

高校の代数学について

数学

この記事は受験生Advent Calendar二日目の記事です.

adventar.org みなさん、高校の代数学をおろそかにしてませんか？問題です！以下の恒等式を証明してください！

$\displaystyle{ \left\{(1+x)^y+(1+x+x^2)^y\right\}^x \times \\ \left\{(1+x^3)^x+(1+x^2+x^4)^x\right\}^y=\\ \left\{(1+x)^x+(1+x+x^2)^x\right\}^y\times \\ \left\{(1+x^3)^y+(1+x^2+x^4)^y\right\}^x }$

この恒等式をWilkieの恒等式といいます. 受験勉強で高校の代数学を勉強したのでノートにまとめました. ぜひ見てください.

drive.google.com

また明日の記事は補集合さん(id:complement_real, 日記の補集合)です. お楽しみに.

Alwe’s blog

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

おすすめのケーキ屋さん

Pâttiserie K. Vincent

Amer 80

ブラムリーリンゴのタルトタタン

タルト・オ・フリュイ

タトル明大前洋菓子店

Aigre Douce

命題論理のカット除去について