二階算術

二階算術 (Second-order arithmetic) (Z₂ あるいは \(\Pi_\infty^1\text{-CA}\) としても知られる)は、自然数だけではなく自然数の「集合」を表す変数の量化を許容する1階述語論理である。

言語

二階算術は一階多領域論理上で公理化される。二階算術は２つの領域 (domain) 型 typeを持つ。 一つは自然数に対する領域でもう一つは自然数の集合を走る領域である。二階算術の言語\(\mathscr{L}_2\)は以下からなる。

• 無限の数字変数 \(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 は逆数学というプロジェクトを立ち上げた。逆数学とは、ある定理を証明するためにはどの公理が必要であるか、またどの公理系ではその定理を証明するためには不十分か、といった問いに答えるためのものである。

逆数学は二階算術のサブシステムに焦点をおいているが、それは定理の強さを計るために広く研究されてきた。「ビッグファイブ」とはRCA₀、WKL₀、ACA₀、 ATR₀、そして \(\Pi_1^1\text{-CA}_0\) である。それぞれのビッグファイブの要素はひとつ前にある要素の真の拡張となっている。専門的な数学に見られる自然数、実数、複素数に関するすべての定理は、ごく一部の例外を除いて、それらを証明するのに必要な最も弱いビッグファイブの要素に基づいて「強さ」を割り当てることができる。それらの多くはRCA₀だけで証明されうる。

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

RCA₀

RCA₀ の名称の由来は再帰的内包公理 (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\)-論理式

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

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

RCA₀ の証明論的順序数は \(\omega^\omega\) である。

WKL₀

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

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.

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

多くの自然な命題が（RCA₀の基本理論の元で）WKL₀ と同値であることを示すことができる。たとえば、閉区間におけるハイネ・ボレルの被覆定理や、連続関数のリーマン積分可能性などである。もっとも重要な同値な命題の1つは、次の \(\Sigma^0_1\) separation である。Given two \(\Sigma^0_1\) sentences with a 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.

WKL₀ の証明論的順序数は \(\omega^\omega\) であり、RCA₀ と同じ consistency strength を持つ。すなわち equiconsistent である。

ACA₀

算術的内包公理 (Arithmetical comprehension axiom)。 We get this by adjoining to RCA₀ axiom schema of comprehension for all arithmetical formulas (ones contained in \(\Sigma_n^0\) for some \(n\in\Bbb N\)). It can be shown that formulas provable in ACA₀ which can be expressed in first-order arithmetic are precisely the formulas provable by Peano arithmetic (one says that ACA₀ is conservative over Peano arithmetic for arithmetical sentences). Like before, it can be shown that ACA₀ is a proper extension of WKL₀, although the proof in this case is not as simple.

ACA₀ 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, ACA₀ is provably equivalent to these two statements).

ACA₀ has a proof-theoretic ordinal of ε₀.

ATR₀

This one stands for "arithmetical transfinite recursion". This system is ACA₀ 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 ACA₀, which means that it is significantly stronger than ACA₀ (see ゲーデルの不完全性定理).

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

Another important schema equivalent to ATR₀ 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 ATR₀ is the フェファーマン・シュッテの順序数.

\(\Pi_1^1\text{-CA}_0\)

The last, and the strongest system in the big five is RCA₀ 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 ACA₀, and it can be shown that it also proves all instances of ATR₀ 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 Ψ₀(Ω_ω).

その他のサブシステム

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

• RCA, WKL, etc. - these are extensions of corresponding systems RCA₀, WKL₀, 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 Z₂.
• 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.