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

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}$ の順序数解析とは違い，繊細な証明図の操作をしなくてはならないところが難しかったです．