ACA_0とATR_0の間の体系について

この記事は Mathematical Logic Advent Calendar2020(https://adventar.org/calendars/5002)の6日目の記事です．

概要

二階算術の部分体系では，ビッグ5と呼ばれる五つの体系( $\text{RCA}_0,\text{WKL}_0,\text{ACA}_0,\text{ATR}_0,\Pi^1_1\text{-CA}_0$ )がよく扱われます．昨年の記事二階算術の諸体系のモデル - お勉強の記録ではこれらについて述べたので，本記事ではビッグ5以外の体系について述べたいと思います．その中でも特に $\text{ACA}_0$ と $\text{ATR}_0$ の間にある二つの体系， $\text{ACA}_0'$ と $\text{ACA}_0^+$ について解説します．

$\text{ACA}_0$ と $\text{ATR}_0$

$\text{ACA}_0$ は，任意の(集合パラメータありの)算術的論理式 $\varphi(n)$ に対して，集合 $\{n: \varphi(n)\}$ が存在する(算術的内包公理)という体系でした．一方 $\text{ATR}_0$ は，この操作を任意の(可算)順序数に沿って行える，というものでした．もう少しフォーマルに述べると， $\text{ATR}_0$ では任意の順序数 $\alpha$ と任意の算術的論理式 $\varphi(n,X)$ に対して，次のようにして集合族 $\{A_\beta:\beta \lt \alpha\}$ を定義することができます：

$A_0 = \{n:\varphi(n,\varnothing)\}$

$A_\beta = \{n:\varphi(n,A_{\lt \beta})\}$

ここで， $A_{\lt \beta}$ は $\{(n,\gamma) : \gamma \lt \beta, n \in A_\gamma\}$ という集合で，今まで定義された $A_\gamma$ たちの情報をすべて持っているような集合になります．

$\text{ACA}_0'$ と $\text{ACA}_0^+$

$\text{ATR}_0$ の例からもわかるように，算術的内包公理を繰り返すことでより複雑な集合を作ることができるようになります．そこで算術的内包公理の繰り返しにより体系を複雑化させることを考えたいのですが，まず $\text{ACA}_0$ でどの程度の繰り返しができるかを考えてみましょう．すると，任意の標準自然数 $k \in \omega$ に対しては $k$ 回の繰り返しができることがわかります(つまり，上の $\text{ATR}_0$ の説明で $\alpha = k$ の場合は $\text{ACA}_0$ でも証明できます)．ところが，これより少し複雑な，「任意の有限順序数 $k \in \mathbb{N}$ に対して $k$ 回の繰り返し」は $\text{ACA}_0$ では一般にできません．この $\text{ACA}_0$ に「任意の有限順序数 $k \in \mathbb{N}$ に対して $k$ 回算術的内包公理を繰り返せる」という公理を付け加えた体系を $\text{ACA}_0'$ と呼びます．そして， $\text{ACA}_0'$ より強い体系として，「最小の無限順序数( $\mathbb{N}$ の順序型)回」の繰り返し」を認める体系を $\text{ACA}_0^+$ と言います．

体系たちの強さ

定義から明らかに $\text{ACA}_0 \leq \text{ACA}_0' \leq \text{ACA}_0^+ \leq \text{ATR}_0$ となることがわかりますが，これらの不等号はすべて真の不等号になります．

定理： $\text{ACA}_0 \lt \text{ACA}_0'$

(証明) 任意にPAの超準モデル $M$ を取る． $\text{ARITH}^M$ を $M$ で集合パラメータなしの算術的論理式で定義できる集合全体とすると， $(M,\text{ARITH}^M)$ は $\text{ACA}_0$ のモデルだが $\text{ACA}_0'$ のモデルではない．

系： $\text{ACA}_0 \not \vdash \Sigma^1_1帰納法$

(証明) $\text{ACA}_0 + \Sigma^1_1帰納法 \vdash \text{ACA}_0'$ より明らか．

定理： $\text{ACA}_0' \lt \text{ACA}_0^+$

(証明) 明らかに $\omega$ モデルにおいては $\text{ACA}_0'$ と $\text{ACA}_0$ に違いはなく，したがって $\omega$ 上で算術的パラメータなしで定義できる集合の全体ARITHは $\text{ACA}_0'$ のモデルである．一方でこれは $\text{ACA}_0^+$ のモデルではない．

定理： $\text{ACA}_0^+ \lt \text{ATR}_0$

(証明) $\{ A \subseteq \omega: A \leq_T \emptyset^{(\omega\cdot n)} \text{ for some } n\}$ は $:\text{ACA}_0'^+$ のモデルだが $\text{ATR}_0$ のモデルでない．

おまけ

以上のように，算術的内包公理の繰り返し回数を適当に制限することによって $\text{ACA}_0$ と $\text{ATR}_0$ の間に様々な体系を作ることができます．このような形で作られる体系は，他にもあり，例えば繰り返しの回数を原始再帰的順序数に制限した $\text{ATR}_0^J$ などが知られています．

お勉強の記録

勉強したことを書いたりする予定

ACA_0とATR_0の間の体系について

概要

$\text{ACA}_0$ と $\text{ATR}_0$

$\text{ACA}_0'$ と $\text{ACA}_0^+$

体系たちの強さ

関連する定理

おまけ