560 ページ

## 言語

• 無限の数字変数 $$x_0$$, $$x_1$$, ... と無限の集合変数 $$X_0$$, $$X_1$$, ...
• 定数記号ゼロ $$0,1$$
• 等号、不等号、帰属関係と呼ばれる3つの二項関係の記号 $$=,<,\in$$。最初の2つは数の間の関係、最後の1つは数と集合の間の関係である。
• 2組の数を1つの数へ移す、それぞれ加法、乗法と呼ばれる2つの二項関数記号 $$+(a,b),\cdot(a,b)$$ 。 それらはしばし中置記法 $$a+b,a\cdot b$$ と表示される。

## 公理

• 二階帰納公理 $$\forall X (0 \in X \wedge \forall x (x \in X \Rightarrow Sx \in X) \Rightarrow \forall x : x \in X)$$ すなわち、ある集合が0を要素に持ち、その集合のすべての要素の後者がその集合の要素である時に、すべての自然数はその集合の要素である。
• 内包の公理型、 $$X$$ が自由変数でないすべての論理式 $$\phi$$ ごとに : $$\exists X \forall x (x \in X \Leftrightarrow \phi(x))$$ 。すべての自然数に関する述語ごとに自然数の部分集合（すなわち $$\phi$$ を満たすこれらの自然数からなる集合)が定義されることを意味する。

## 部分体系

$$\mathsf{Z}_2$$は（$$\mathsf{ZFC}$$などよりは弱いが）非常に強力な形式体系であり、二階算術で表現できる数学の命題を証明するために、全ての公理を用いる必要がない。そのため、$$\mathsf{Z}_2$$の弱い部分体系を考えたとき数学の命題は証明可能であろうか、という疑問が生ずる。Harvey Friedman逆数学というプロジェクトを立ち上げた。逆数学とは、ある定理を証明するためにはどの公理が必要であるか、またどの公理系ではその定理を証明するためには不十分か、といった問いに答えるためのものである。

これらのサブシステムはなお二階算術の「言語」を使っているが、必ずしもその公理を使うわけではない。これらの定理のいくつかは直観的にペアノ算術より弱いかもしれないが、ペアノ算術とは異なり、それらはすべて実数について記述することができる。

### RCA0

RCA0 の名称の由来は再帰的内包公理 (recursive comprehension axiom）であり、ビッグファイブの中でもっとも弱い。以下で構成される。

• ロビンソン算術
• $$(\forall x)[x+1\neq 0].$$
• $$(\forall x)(\forall y)[x+1=y+1\to x=y].$$
• $$(\forall x)[x+0=x].$$
• $$(\forall x)(\forall y)[x+(y+1)=(x+y)+1].$$
• $$(\forall x)[x\cdot 0=0].$$
• $$(\forall x)(\forall y)[x\cdot(y+1)=x\cdot y+x].$$
• $$(\forall x)[x\nless 0].$$
• $$(\forall x)(\forall y)[x<y+1\leftrightarrow x<y\lor x=y].$$
• $$\Sigma_1^0$$ までの式に制限した帰納法公理図式$$(\Sigma^0_1\text{-}\mathsf{IND})$$ (算術的階層を参照)
• $$\varphi(0)\land(\forall x)[\varphi(x)\to\varphi(x+1)]\to(\forall x)\varphi(x).$$ ここで$$\varphi$$は$$\Sigma^0_1$$-論理式とする。
• $$\Delta^0_1$$ までの式に制限した内包公理図式$$(\Delta^0_1\text{-}\mathsf{CA})$$
• $$(\forall x)[\varphi(x)\leftrightarrow \psi(x)]\to(\exists X)(\forall x)[x\in X\leftrightarrow \varphi(x)]$$ ここで$$\varphi$$は$$\Sigma^0_1$$-論理式、$$\psi$$は$$\Pi^0_1$$-論理式

これはいわゆる「基本体系」であり、他のサブシステムはすべて RCA0 の公理をなにかしたの形で含んでいる。RCA0 は弱い体系であるが、自然数や実数に関する多くの基本的な性質を証明することができる。たとえば、数列の極限が一意に定まることや、中間値の定理などである。RCA0 は、多くの「日常的に使われる」自然数と実数の性質を証明可能である。

RCA0 は再帰的なものの存在しか証明できる強さを持っていない。たとえば、この理論体系における集合存在公理は、計算不可能な関数の存在を証明する強さを持っていない。

RCA0証明論的順序数は $$\omega^\omega$$ である。

### WKL0

WKL0 の名称は弱ケーニヒの補題 (weak König's lemma)に由来する。RCA0 に、次のケーニヒの補題の弱い形式を加えて拡張したものがWKL0 である。

Let $$2^{<\omega}$$ be the tree of all finite binary sequences, and let $$T$$ be one of its infinite subtrees. Then $$T$$ has an infinite branch.

RCA0 はこの補題を証明できない。 無限の計算可能な木 $$T$$ で計算可能な無限の枝を持たないものを作ることができるが、RCA0 は計算不可能な集合の存在を証明できないためである。 したがって、 WKL0 は RCA0 の適切な拡張である。

WKL0証明論的順序数は $$\omega^\omega$$ であり、RCA0 と同じ consistency strength を持つ。すなわち equiconsistent である。

### ACA0

ACA0 is strong enough to prove all the statements required to work well with real (or complex) analysis, including ボルツァーノ＝ワイエルシュトラスの定理 or full König's lemma (for trees on finite sequences of natural numbers) (in fact, ACA0 is provably equivalent to these two statements).

ACA0 has a proof-theoretic ordinal of ε₀.

### ATR0

This one stands for "arithmetical transfinite recursion". This system is ACA0 together with axiom schema stating, intuitively, that if we have countable well-ordering (coded in a certain way) and so called arithmetical functional, we can iterate application of this functional transfinitely by following the mentioned well-ordering. This means that certain set constructions can be accomplished by iterating a simple construction transfinite number of times.

Addition of this axiom schema makes it possible to build a theory of ordinal numbers in second-order arithmetic. An example of strength of this schema is that it's sufficient to prove the consistency of ACA0, which means that it is significantly stronger than ACA0 (see ゲーデルの不完全性定理).

Important single theorem which is equivalent (over RCA0) to ATR0 is that every two countable well-orderings are comparable, so that ordinal numbers form a linear order.

Another important schema equivalent to ATR0 is $$\Sigma^1_1$$ separation: given two $$\Sigma^1_1$$ sentences (see 解析的階層) with free variable $$n$$, never both true, there is a set which contains all $$n$$ which make first formula true, and none which make second one true.

The proof-theoretic ordinal of ATR0 is the フェファーマン・シュッテの順序数.

### $$\Pi_1^1\text{-CA}_0$$

The last, and the strongest system in the big five is RCA0 extended by $$\Pi_1^1$$ comprehension axiom schema, hence the abbreviation. This is so called impredicative system, because it's axioms, in a way, assert existence of objects which depend on the object defined (this is because defining set $$X$$ using $$\Pi_1^1$$ formula involves statement which is supposed to hold for all sets, including $$X$$ itself).

It's clear that $$\Pi_1^1\text{-CA}_0$$ contains all the axioms of ACA0, and it can be shown that it also proves all instances of ATR0 axioms, which shows that $$\Pi_1^1\text{-CA}_0$$ can build basic theory of ordinal numbers. However, as one can show, statement that given order is well-order is a $$\Pi_1^1$$ statement, which means that this last system can show existence of sets definitions of which explicitly use notions of well-ordering, which, in big part, is where the strength of the system comes from.

The proof-theoretic ordinal of $$\Pi_1^1\text{-CA}_0$$ is Ψ0ω).

### その他のサブシステム

Apart from the Big Five, many subsystems of Z2 have been analysed. Below is the list of more noteworthy ones.

• RCA, WKL, etc. - these are extensions of corresponding systems RCA0, WKL0, etc. resulting by addition of first-order induction schema for all formulas in language of second-order arithmetic. Indicator of whether this full axiom schema appears in subsystem or not is 0 in the subscript.
• $$\Sigma_m^n\text{-IND}$$, $$\Pi_m^n\text{-IND}$$, $$\Delta_m^n\text{-IND}$$ - these are schemas of first-order induction limited to $$\Sigma_m^n$$, $$\Pi_m^n$$, $$\Delta_m^n$$ formulas respectively (here and below $$n$$ is 0 or 1). Additionally, $$\Pi_\infty^1\text{-IND}$$ is conjunction of all of these schemas.
• $$\Sigma_m^n\text{-TI}$$, $$\Pi_m^n\text{-TI}$$, $$\Delta_m^n\text{-TI}$$ - these are schemas of transfinite induction limited to formulas in respective classes. This means that for every formula $$\psi(n)$$ of respective complexity and any well-ordering of natural numbers (coded as some set $$X$$) we can prove $$\forall n:\psi(n)$$ by following this well-order. Like above, $$\Pi_\infty^1\text{-TI}$$ is conjunction of the above.
• $$\Sigma_m^n\text{-CA}$$, $$\Pi_m^n\text{-CA}$$, $$\Delta_m^n\text{-CA}$$ - these are schemas of comprehension for respective classes of formulas. Their conjunction, $$\Pi_\infty^1\text{-CA}$$, over a weak base system is equivalent to all of Z2.
• BI - the axiom-schema of bar induction. To state it, we first need a notion of well-founded partial order. We say the ordering $$\prec$$ of natural numbers is well-founded if for every set $$X$$ the following is true: if for all $$((\forall i\prec j:i\in X)\Rightarrow j\in X)\Rightarrow\forall n:n\in X$$. BI states that such an implication is still true if we replace $$n\in X$$ by any formula $$\psi(n)$$, provided $$a\prec b$$ is expressible by arithmetical formula.
• $$\Sigma_m^n\text{-AC}$$, $$\Pi_m^n\text{-AC}$$, $$\Delta_m^n\text{-AC}$$ - these are schemas "adaptating" ZFC's 選択公理 to second-order arithmetic. They say that if for every $$n$$ there is a set $$X$$ such that $$\psi(n,X)$$ (of complexity asserted by the schema), then we can create sequence of sets $$X_n$$ such that $$\psi(n,X_n)$$. A variant of this schema is so called weak axiom of choice, which requires that for every $$n$$ there is precisely one $$X$$ making the formula true.
• $$\Sigma_m^n\text{-DC}$$, $$\Pi_m^n\text{-DC}$$, $$\Delta_m^n\text{-DC}$$ - these schemas adapt to second-order arithmetic a weak form of the axiom of choice named "axiom of dependent choice". They say that if for every $$n,X$$ there is $$Y$$ such that $$\psi(n,X,Y)$$, then we can find sequence $$X_n$$ of sets such that $$\psi(n,X_n,X_{n+1})$$. Slight extension to strong dependent choice tells us that the same can be done if we don't assume that such a $$Y$$ exists always, but $$\psi(n,X_n,X_{n+1})$$ has to hold whenever it exists for $$X_n$$.
• $$\Sigma_m^n\text{-TR}$$, $$\Pi_m^n\text{-TR}$$, $$\Delta_m^n\text{-TR}$$ - these are extensions to arithmetical transfinite recursion to formulas other than arithmetical ones. As before, intuitively, it says that we can iterate certain constructions transfinitely many times.

## 参考文献

1. S.G. Simpson. Subsystems of second order arithmetic. Vol. 1. Cambridge University Press, 2009.