逆数学

逆数学

逆数学 (reverse mathematics) は数学の定理の強さ、すなわちその定理を証明するためにどのくらいの仮定、すなわち公理が必要なのか分析する分野である。逆数学の「逆」は定理と公理の同値性を示すために、「定理から公理を証明する」訳であるが、これが通常の数学での「公理から定理を証明する」の逆であることにちなむ。

二階算術

通常の数学の定理の強さを分析するためにはZermelo–Fraenkelの集合論、$\mathsf{ZF},\mathsf{ZFC}$などは強すぎる。もちろん、「 $\mathsf{ZF}$ 上でZornの補題と選択公理が同値」や 「$\mathsf{ZF}$ 上でBoole素イデアル定理と完全性定理の同値」、「$\mathsf{ZF}$ 上で $\mathbf{\Sigma}^1_1$ の決定性と任意の集合に対してそのシャープが存在することは同値」などの逆数学的な結果は多く知られているが、多くの定理は $\mathsf{ZF},\mathsf{ZFC}$ で証明可能であるが故に繊細な分析は難しい。よって $\mathsf{ZF}$ などと比べて遥かに弱い二階算術 (second order arithmetic) $\mathsf{Z}_2$ の部分体系のもとに分析する。このアプローチは以下のようなメリットがある。

• 計算理論や計算可能解析学などの結果を応用しやすい。
• 算術のモデルを考えることで定理の分析を繊細に行うことができる((集合論的な強制法による推移モデルの構成は推移的であるが故にShoenfield–Lévyの結果 $\Sigma^1_2\cup\Pi^1_2$ に対して絶対的であることから独立性などを導くことができない。))。

一方以下のようなデメリットもある。

• 二階算術では可算より大きい無限に対する表現能力が少ない。
• 繊細なGödel数化を必要とする場合がある。

二階算術は(形式化の違いなどはあるが)Hilbertの数学の基礎づけにて現れたものであり、古典的な解析学が展開できることから古い文献などでは単に解析 (analysis) と言われることもある。後述する述べるビッグ・ファイブなどは(帰納法の制限がないなどの違いはあるが)Friedmanの1974年の講演がベースとなっている[H.Friedman75, H.Friedman76]。 逆数学、及び二階算術の歴史、形成については[Simpson09]や[Dean–Walsh16]などを参照せよ。

二階算術の定義

二階算術はとても大雑把に言えば、自然数 $\mathbb{N}$ と、その部分集合について扱う理論である。よって自然数とその部分集合((ここでの自然数及び集合は $\mathsf{Z}_2$ に於ける対象としてのものであることに注意すべきである。))、一つずつに型を持つ一階述語論理で定式化される((二階述語論理にて定式化されることもあるが、Henkin意味論の上で同値である。))。以下自然数の変数を小文字で表し集合変数を大文字で表すとする。言語 $\mathscr{L}_{\mathsf{Z}_2}:=\{\overline{0},\overline{1},+,\mathrel{\cdot},<,=,\in \}$ とし、$\in$ は自然数と集合を一つずつ取る二項関係であり、$x\in X$ で $x$ は集合 $X$ に帰属することを表す。また集合同士の等号 $X=Y$ は $(\forall x)[x\in X\leftrightarrow x\in Y]$ の略記とする。二階算術 $\mathsf{Z}_2$ は以下の公理からなる。また $x\neq y,x\nless y,X\neq Y$ は $x=y,x<y,X=Y$ の否定とする。

定義（二階算術 $\mathsf{Z}_2$）

1. 算術の公理
   1. $(\forall x)[x+\overline{1}\neq\overline{0}]$ 。
   2. $(\forall x)(\forall y)[x+\overline{1}=y+\overline{1}\to x=y]$ 。
   3. $(\forall x)[x+\overline{0}=x]$ 。
   4. $(\forall x)(\forall y)[x+(y+\overline{1})=(x+y)+\overline{1}]$ 。
   5. $(\forall x)[x\mathrel{\cdot}\overline{0}=\overline{0}]$ 。
   6. $(\forall x)(\forall y)[x\mathrel{\cdot}(y+\overline{1})=x\mathrel{\cdot}y+x]$ 。
   7. $(\forall x)[x\nless \overline{0}]$ 。
   8. $(\forall x)(\forall y)[x<y+\overline{1}\leftrightarrow x<y\lor x=y]$ 。
2. 数学的帰納法の公理図式 (axiom schema of mathematical induction)
   1. $\varphi(\overline{0})\land(\forall x)[\varphi(x)\to\varphi(x+\overline{1})]\to\forall x\varphi(x)$ 。ここで $\varphi$ は $\mathsf{Z}_2$ の論理式とする。
3. 内包公理図式 (axiom schema of comprehension)
   1. $(\exists X)(\forall x)[\varphi(x)\leftrightarrow x\in X]$ 。ここで $\varphi$ は $\mathsf{Z}_2$ の変数 $X$ を含まない論理式とする。

二階算術の部分体系

さて、この $\mathsf{Z}_2$ でも分析をするには強すぎるため、その部分体系を考える必要がある。以下では数学的帰納法と内包性の公理図式を制限する部分体系を考える。制限するためには論理式の階層、算術的階層 (arithmetical hierarchy) と解析的階層 (analytical hierarchy) を導入する。

定義（算術的階層）

$\Delta^0_0$ を有界論理式 (bounded formula) 、すなわち $(\forall x<t)\varphi(x),(\exists x<t)\varphi(x)$ のような形の量化以外を含まないような論理式の集合とする。$\Sigma^0_n,\Pi^0_n$ を $n$ に関して帰納的に定義する。

1. $\Sigma^0_0:=\Pi^0_0:=\Delta^0_0$ とする。
2. $\Sigma^0_{n+1}$ を、$\Pi^0_n$-論理式 $\varphi$ に対して $\exists x\varphi(x)$ と表されるような論理式の集合とする。
3. $\Pi^0_{n+1}$ を、$\Sigma^0_n$-論理式 $\varphi$ に対して $\forall x\varphi(x)$ と表されるような論理式の集合とする。

要するに $\Delta^0_0$-論理式を母式とした冠頭標準形を考えたとき、$\Sigma^0_n$-論理式は $\exists$ を先頭として量化子が $n$ 個交代して現れている論理式で、$\Pi^0_n$-論理式は $\exists$ を先頭として量化子が $n$ 個交代して現れている論理式である。

また、ある $n$ に対して $\Sigma^0_n\cup\Pi^0_n$ に含まれる論理式を算術的 (arithmetical, arithmetic) という。また二階の自由変数を含まない論理式に制限したものを $\Sigma^{0-}_n,\Pi^{0-}_n$ と表す。

定義（解析的階層）

算術的階層と同様に $n$ に関して帰納的に解析的階層 $\Sigma^1_n,\Pi^1_n$ を定義する。

1. $\Sigma^1_0,\Delta^1_0,\Pi^1_0$ を算術的論理式の集合とする。
2. $\Sigma^1_{n+1}$ を、$\Pi^1_n$-論理式 $\varphi$ に対して $\exists X\varphi(X)$ と表されるような論理式の集合とする。
3. $\Pi^1_{n+1}$ を、$\Sigma^1_n$-論理式 $\varphi$ に対して $\forall X\varphi(X)$ と表されるような論理式の集合とする。また二階の自由変数を含まない論理式に制限したものを $\Sigma^{1-}_n,\Pi^{1-}_n$ と表す。

定義（数学的帰納法図式、内包性図式、分離性図式）

$\Gamma$ を論理式の集合とする。以下の公理図式を定義する。

• $\Gamma$-帰納法公理図式 (axiom schema of $\Gamma$-induction) $(\Gamma\text{-}\mathsf{IND})$

$$\varphi(\overline{0})\land(\forall x)[\varphi(x)\to\varphi(x+\overline{1})]\to\forall x\varphi(x).$$ ここで $\varphi\in\Gamma$ とする。

• $\Gamma$-内包公理図式 (axiom schema of $\Gamma$-comprehension) $(\Gamma\text{-}\mathsf{CA})$ 。

$$(\exists X)(\forall x)[\varphi(x)\leftrightarrow x\in X].$$ ここで $\varphi\in\Gamma$ で変数 $X$ を含まないとする。

• $\Delta^i_j$-内包公理図式 (axiom schema of $\Delta^i_j$-comprehension) $(\Delta^i_j\text{-}\mathsf{CA})$ 。

$$(\forall x)[\varphi(x)\leftrightarrow\psi(x)]\to(\exists X)(\forall x)[\varphi(x)\leftrightarrow x\in X].$$ ここで $\varphi\in\Sigma^i_j,\psi\in\Pi^i_j$ で変数 $X$ を含まないとする。

• $\Gamma$-分離公理図式 (axiom schema of $\Gamma$-separation) $(\Gamma\text{-}\mathsf{SP})$ 。

$$(\forall x)[\varphi(x)\to\lnot\psi(x)]\to(\exists X)(\forall x)[(\varphi(x)\to x\in X)\land(x\in X\to\lnot\psi(x))].$$ ここで $\varphi,\psi\in\Gamma$ で変数 $X$ を含まないとする。

ビッグ・ファイブ

算術の公理に $(\Sigma^0_1\text{-}\mathsf{IND})$ を加えた体系を $\mathsf{I}\Sigma^0_1$ とする。このとき以下のように体系を定める。

1. 再帰的内包公理 (recursive comprehension axiom) $$\mathsf{RCA}_0:=\mathsf{I}\Sigma^0_1+(\Delta^0_1\text{-}\mathsf{CA}).$$
2. 弱Kőnigの補題 (weak Kőnig lemma)

$$\mathsf{WKL}_0:=\mathsf{I}\Sigma^0_1+(\Sigma^0_1\text{-}\mathsf{SP}).$$

1. 算術的内包公理 (arithmetical comprehension axiom)

$$\mathsf{ACA}_0:=\mathsf{I}\Sigma^0_1+(\Sigma^0_1\text{-}\mathsf{CA}).$$

1. 算術的超限再帰 (arithmetical transfinite recursion)

$$\mathsf{ATR}_0:=\mathsf{I}\Sigma^0_1+(\Sigma^1_1\text{-}\mathsf{SP}).$$

1. $\Pi^1_1$-内包公理 ($\Pi^1_1$-comprehension axiom)

$$\Pi^1_1\text{-}\mathsf{CA}_0:=\mathsf{I}\Sigma^0_1+(\Sigma^1_1\text{-}\mathsf{CA}).$$

これらの公理系をビッグ・ファイブ (big five) といい、逆数学に於いて主要な役割を持つ。これらの理論は順に強くなる、すなわち $$\mathrm{Th}(\mathsf{RCA}_0)\subsetneq\mathrm{Th}(\mathsf{WKL}_0)\subsetneq\mathrm{Th}(\mathsf{ACA}_0)\subsetneq\mathrm{Th}(\mathsf{ATR}_0)\subsetneq\mathrm{Th}(\Pi^1_1\text{-}\mathsf{CA}_0)$$ が成り立つ。

逆数学現象

Friedmanは[H.Friedman75]にて以下のように述べた。

When the theorem is proved from the rights axioms, the axioms can be proved from the theorem. [H.Friedman75].

多くの数学の定理は $\mathsf{RCA}_0$ 上で証明可能であるか、あるいは $\mathsf{RCA}_0$ 上で他のビッグ・ファイブとの同値性が証明可能であることが知られている。この事実を逆数学現象 (reverse mathematics phenomenon) という。実際の研究では、むしろ逆数学現象が当て嵌まらない例に着目されることもある。以下には逆数学現象の例を挙げよう。ここに挙げる殆どの結果、特に出典を明記していない結果は[Simpson09]に記載されてある。

$\mathsf{RCA}_0$

以下の定理は $\mathsf{RCA}_0$ で証明可能である。

• $(\Pi^0_1\text{-}\mathsf{IND})$ 。
• 全域関数全体は原始再帰法に閉じている。
• $\mathbb{R}$ の不可算性。任意の実数の可算列 $\{x_n\}_{n\in\mathbb{N}}$ に対し、ある実数 $y$ が存在し、任意の $n\in\mathbb{N}$ に対し $x_n\neq y$ である。
• $\mathbb{R}$ はArchimedes的順序実閉体である。
• [田中02]、代数学の基本定理。$\mathbb{C}$ は代数閉体である。
• Baireの範疇性定理。$X$ を完備可分距離空間とし、$\{U_n\}_{n\in\mathbb{N}}$ を稠密開集合の可算列とする。このとき $\cap_{n\in\mathbb{N}}U_k$ は稠密である。
• 完備可分距離空間はパラコンパクトである。
• Urysohnの補題。$X$ を完備可分距離空間とし、$C_0,C_1$ を交わらない $X$ の閉集合とする。このとき連続写像 $f\colon X\to[0,1]$ で、任意の $x\in X,i\in\{0,1\}$ に対し $x\in C_i$ と $f(x)=i$ が同値になるようなものが構成できる。
• Tietzの拡張定理。$X$ を完備可分距離空間とし、$C\subseteq X$ を閉集合、$f\colon C\to[-1,1]$ を連続写像とする。このとき、$g\colon X\to[-1,1]$ で $f$ の拡張となる、すなわち $x\in C$ に対し $f(x)=g(x)$ となるようなものが構成できる。
• Spernerの補題。$S$ を $k$-単体、$S_0,\ldots,S_m$ を $S$ の単体的細分とする。$S_0,\ldots,S_m$ の頂点が許容的にラベルされているとき、ある $i\leq m$ に対し $S_i$ ラベルの集合 $\{0,\ldots,k\}$ から写される。
• 区間縮小法。可算実数列 $\{x_n\}_{n\in\mathbb{N}},\{y_n\}_{n\in\mathbb{N}}$ が $x_n\leq x_{n+1}\leq y_{n+1}\leq y_n$ かつ $\lim_{n\to\infty}|x_n-y_n|=0$ を満たすとする。このとき $z=\lim_{n\to\infty}x_n=\lim_{n\to\infty}y_n$ となる $z\in\mathbb{R}$ が存在する。
• 中間値の定理。$f\colon\mathbb{R}\to\mathbb{R}$ が区間 $[0,1]$ 上連続であるとする。このとき $f(0)<0<f(1)$ ならば、ある $x\in(0,1)$ が存在し、$f(x)=0$ である。
• Weierstrassの近似定理 $f$ を $[0,1]$ 上の一様連続関数とするとき、任意の $x\in[0,1], \epsilon>0$ に対して、ある多項式 $g(x)\in\mathbb{Q}[x]$ が存在して $|f(x)-g(x)|<\epsilon$ となる。
• [Simpson84]。Cauchy–Picard–Lindelöfの一意存在定理。$a,b,M$ を正の実数、$f\colon[-a,a]\times[-b,b]\to\mathbb{R}$ をLipschitz連続関数で $|f(x,y)|\leq M$ を満たすとする。このとき初期値問題 $dy/dx=f(x,y),y(0)=0$ は一様連続な $[-\alpha,\alpha]$ 上での局所解 $y=\phi(x)$ を持つ。ここで $\alpha:=\min\{a,b/M\}$ とする。
• 任意の可算な体に対し、その代数閉包が存在する。
• 任意の可算な順序体に対し、その実閉包が一意に存在する。
• Banach–Steinhausの定理。$A,B$ を可分Banach空間、$\{F_n\}_{n\in\mathbb{N}}$ を $A$ から $B$ への有界線形作用素の列とする。このとき、任意の $x\in A$ に対し、ある $M$ が存在し $\|F_n(x)\|<M$ が全ての $n\in\mathbb{N}$ に対して成り立つとき、任意の $x\in A,n\in\mathbb{N}$ に対し $\|F_n(x)\|\leq \alpha\cdot\|x\|$ となる $\alpha$ が存在する。
• 弱い完全性定理。可算言語上の可算理論 $T$ が無矛盾かつ演繹に閉じているとする。このとき $T$ の可算モデル $\mathcal{M}$ が存在する。
• 健全性定理。可算言語上の可算理論 $T$ が弱可算モデルを持つとする。このとき $T$ は無矛盾である。
• カット除去定理。可算言語の一階述語論理が証明可能ならカット規則なしで証明可能である。
• [Tanaka–Yamazaki05]]順序実閉体の理論 $\mathsf{ROCF}$ は量化記号消去可能である。
• 初等再帰算術 $\mathsf{EA}$ は無矛盾である。
• 不完全性定理 。最弱算術 $\mathsf{R}$ を含む帰納的可算理論 $T$ が無矛盾なら $T$ で証明も反証もできない命題が存在する。また帰納的可算理論 $T$ が初等再帰算術 $\mathsf{EA}$ を含むなら、Löbの可導性条件を満たす可証性述語から定義される $T$ の無矛盾性は $T$ にて証明できない。
• $\mathsf{ZF}$ が無矛盾なら $\mathsf{ZF}+V=L$ も無矛盾である。従って $\mathsf{ZF}$ が無矛盾なら $\mathsf{ZFC},\mathsf{ZFC}+\mathsf{GCH}$ も無矛盾である。

$\mathsf{WKL}_0$

以下の定理は $\mathsf{RCA}_0$ 上で $\mathsf{WKL}_0$ と同値であることが証明可能である。

• 弱Kőnigの補題、$(\mathsf{WKL})$ 。任意の可算無限二分木は可算無限枝を持つ。
• [Simpson–Yokoyama13]。任意のPeanoシステムは標準システム $\mathbb{N}$ に同型である。
• Heine–Borelの定理。$X$ をコンパクト距離空間とする。$\{U_i\}_{i\in\mathbb{N}}$ を $X$ の開被覆とするとき、ある $i\in\mathbb{N}$ が存在して $\{U_j\}_{j\leq i}$ は有限部分被覆となる。
• [Kihara20]。開集合 $U\subseteq\mathbb{R}^m$ 、単射連続写像 $f\colon U\to\mathbb{R}^m$ に対し $f[U]$ は開集合である。
• [Kihara20]。$m>n$ であるとき $\mathbb{R}^m$ から $\mathbb{R}^n$ への単射連続写像は存在しない。
• [Kihara20]。$m>n$ であるとき $\mathbb{R}^m$ から $\mathbb{R}^n$ への位相空間論に於ける埋め込みは存在しない。
• $f$ を $[0,1]$ 上の連続関数とするとき、任意の $x\in[0,1]$ に対して、ある多項式 $g(x)\in\mathbb{Q}[x]$ が存在して $|f(x)-g(x)|<1$ となる。
• $[0,1]$ 上連続な関数は $[0,1]$ 上一様連続である。
• $[0,1]$ 上連続な関数は $[0,1]$ 上有界である。
• $[0,1]$ 上有界かつ一様連続な関数は上限を持つ。
• $[0,1]$ 上有界かつ一様連続な関数は上限を持つならば最大値を取る。
• 閉有界区間 $[a,b]$ 上連続な関数 $f$ は有限のRieman積分の値 $\int^a_b f(x)dx$ を持つ。
• [Shioji–Tanaka90]。Brouwerの不動点定理。$C$ を $\mathbb{R}^n$ の点の非空有限集合の凸包とする。このとき連続関数 $f\colon C\to C$ は不動点を持つ。
• [Shioji–Tanaka90]。弱いBrouwerの不動点定理。連続関数 $f\colon [0,1]^2\to [0,1]^2$ は不動点を持つ。
• [Shioji–Tanaka90]。Schauderの不動点定理。$C\subseteq[-1,1]^\mathbb{N}$ を非空閉凸集合とする。このとき連続関数 $f\colon C\to C$ は不動点を持つ。
• [Simpson84]。Cauchy–Peanoの存在定理。$a,b>0$ 、$f\colon [-a,a]\times[-b,b]\to\mathbb{R}$ を連続関数とする。このとき初期値問題 $dy/dx=f(x,y),y(0)=0$ は連続で微分可能な $[-\alpha,\alpha]$ 上での局所解 $y=\phi(x)$ を持つ。ここで $\alpha:=\min\{a,b/\max\{|x|\mid x\in \mathrm{ran}(f)\}\}$ とする。
• [Brown–Simpson86]。Hahn–Banachの定理。 $A$ を可分Banach空間 $S$ を $A$ の部分空間、$\alpha$ を正の実数とする。$f\colon S\to\mathbb{R}$ を $\|f\|\leq\alpha$ を満たす有界線形汎関数とする。このとき $f$ の拡大 $f'\colon A\to\mathbb{R}$ で $\|f'\|\leq\alpha$ を満たすものが存在する。
• [Sakamoto–Yokoyama07]。Jordanの閉曲線定理。
• [Sakamoto–Yokoyama07]。Jordan–Schönfliesの定理。
• [Friedman–Simpson–Smith83]。任意の可算形式的実体は順序付け可能である。
• [Friedman–Simpson–Smith83]。任意の可算形式的実体は実閉包を持つ。
• [Friedman–Simpson–Smith83]。任意の可算な体は代数閉包を一意に持つ。
• [Friedman–Simpson–Smith83]。任意の可算可換環は素イデアルを持つ。
• [Friedman–Simpson–Smith83]。任意の可算可換環は根基イデアルを持つ。
• [Hatzikiriakou–Simpson90]。任意の可算で無捻アーベル群は順序付け可能である。
• [Hatzikiriakou–Simpson89]。可算な体 $K_0,K_1$ 、単射 $f\colon K_0\to K_1$ 、$K_0$ の付値環 $V_0$ に対し、$K_1$ の付値環 $V_2$ で $V_0=f^{-1}[V_1]$ となるものが存在する。
• [Tanaka–Yamazaki00]。任意のコンパクト群はHaar測度を持つ。
• Lindenbaumの補題。任意の可算理論は無矛盾完全拡大を持つ。
• 完全性定理。任意の無矛盾な理論はモデルを持つ。
• コンパクト性定理。可算理論 $T$ の全ての有限部分理論がモデルを持つなら、$T$ もモデルを持つ。
• 可算命題論理の完全性定理。
• 可算命題論理のコンパクト性定理。

$\mathsf{ACA}_0$

以下の定理は $\mathsf{RCA}_0$ 上で $\mathsf{ACA}_0$ と同値であることが証明可能である。

• 算術的内包公理、$(\Sigma^1_0\text{-}\mathsf{CA})$ 。
• 任意の単射 $f\colon\mathbb{N}\to\mathbb{N}$ に対し値域 $\mathrm{ran}(f)$ が存在する。
• [H.Friedman76]。Bolzano–Weierstrassの定理。任意の有界な可算実数列は収束する部分列を持つ。
• [H.Friedman76]。任意のCauchy列は収束する。
• [H.Friedman76]。任意の有界な可算実数列は最小上界を持つ。
• [H.Friedman76]。単調収束定理。任意の有界な単調増加可算実数列は収束する。
• コンパクト距離空間は点列コンパクトである。
• 完備可分距離空間上のCauchy列は収束する。
• Ascoli–Arzelàの補題。コンパクト距離空間 $A,B$ に対して $\{f_n\}_{n\in\mathbb{N}}$ を $A$ から $B$ への同程度連続な連続関数の列とする。このとき、一様連続な $\{f_n\}_{n\in\mathbb{N}}$ の部分列が存在する。
• [Yokoyama07]。Riemanの写像定理。空でない単連結開集合 $U\subseteq\mathbb{C}$ に対し単位円 $D$ への等角写像 $f\colon U\to D$ が存在する。
• [Friedman–Simpson–Smith83]。任意の可算な体は埋め込みを伴う代数閉包を持つ。
• [Friedman–Simpson–Smith83]。任意の可算な体はある可算代数閉体に埋め込まれる。
• [Friedman–Simpson–Smith83]。任意の可算順序体は埋め込みを伴う実閉包を持つ。
• [Friedman–Simpson–Smith83]。任意の可算順序体はある可算実閉体に埋め込まれる。
• [Friedman–Simpson–Smith83]。可算な体上の可算ベクトル空間は基底を持つ。
• [Friedman–Simpson–Smith83]。$\mathbb{Q}$ 上の可算ベクトル空間は基底を持つ。
• [Friedman–Simpson–Smith83]。任意の $\mathbb{Q}$ 上の可算ベクトル空間は有限次元であるか、線形独立な無限集合を持つ。
• [Friedman–Simpson–Smith83]。任意の可算体 $K\subseteq L$ に対して $L$ に対する $K$ 上の超越基底が存在する。
• [Friedman–Simpson–Smith83]。$K$ を標数 $0$ で有限の超越基底を持たない体とするとき、$L$ は代数的独立な無限集合を含む。
• [Friedman–Simpson–Smith83]。任意の可算可換環は極大イデアルを持つ。
• [Friedman–Simpson–Smith83]。任意の可算整域は極大イデアルを持つ。
• [Friedman–Simpson–Smith83]。任意の可算可除アーベル群は移入群である。
• [Friedman–Simpson–Smith83]。可算アーベル群の可除閉包は一意である。
• [H.Friedman76]。Kőnigの補題。任意の可算無限有限分岐木は可算無限枝を持つ。
• Ramseyの定理。与えられた標準自然数 $k\geq 3,l\geq 2$ に対して $\mathsf{RT}^k_l$ 。ここで $\mathsf{RT}^k_l$ は「全ての $f\colon [\mathbb{N}]^k\to l:=\{0,\ldots,l-1\}$ に対して、ある無限集合 $X\subseteq \mathbb{N}$ が存在し $f$ は $[X]^k$ 上で定数関数となる」という命題である。
• Ramseyの定理。与えられた標準自然数 $k\geq 3$ に対して $\mathsf{RT}^k$ 。ここで $\mathsf{RT}^k$ は「全ての $l>1$ 、全ての $f\colon [\mathbb{N}]^k\to l:=\{0,\ldots,l-1\}$ に対して、ある無限集合 $X\subseteq \mathbb{N}$ が存在し $f$ は $[X]^k$ 上で定数関数となる」という命題である。
• [Girard87]。整列原理、$\mathsf{WOP}(\lambda \xi.\omega^\xi)$ 。$\xi$ が整列順序であるとき、その冪 $\omega^\xi$ も整列順序である。

$\mathsf{ATR}_0$

以下の定理は $\mathsf{RCA}_0$ 上で $\mathsf{ATR}_0$ と同値であることが証明可能である。

• 算術的超限再帰図式 $(\mathsf{ATR})$ 。与えられた算術的論理式 $\varphi(x,X)$ 、任意の集合 $A$ 、整列順序 $\prec$ に対し以下を満たすような集合 $H$ が存在する。以下で $0$ は $\prec$ の最小元、$\mathrm{field}(\prec)$ は $\prec$ の台集合、$\alpha+1$ は $\alpha$ の後者、$(X)_\alpha:=\{x\mid(x,a)\in X\}$ とする。
  • $(H)_0=A$ 。
  • 任意の $\alpha\in\mathrm{field}(\prec)$ 、任意の $x\in\mathbb{N}$ に対し $x\in (H)_{\alpha+1}\leftrightarrow\varphi(x,(H)_\alpha)$ である。
  • 任意の極限となる $\lambda\in\mathrm{field}(\prec)$ 、任意の $\alpha\prec\lambda$ 、任意の $x\in\mathbb{N}$ に対し $x\in((H)_\lambda)_\alpha\leftrightarrow x\in H_\alpha$ 。
• [H.Friedman76]。可算整列順序の比較可能定理。可算整列順序 $\prec_0,\prec_1$ に対し $\prec_0$ は $\prec_1$ の始切片と同型であるか、あるいは $\prec_1$ は $\prec_0$ の始切片と同型である。
• 完全集合定理。完備可分距離空間の任意の非可算閉部分集合は完全閉集合を部分集合として持つ。
• Ulmの定理。任意の可算被約アーベル $p$-群はUlm分解を持つ。
• $G,H$ をfatなアーベル $p$-群とする。このとき $G$ は $H$ の直和因子であるか、$H$ は $G$ の直和因子である。
• $\mathbf{\Sigma}^0_1$-ゲームは決定的である。
• $\mathbf{\Delta}^0_1$-ゲームは決定的である。
• 開Ramseyの定理。$\mathbf{\Sigma}^0_1\text{-}\mathsf{RT}$ 。
• 開閉Ramseyの定理。$\mathbf{\Delta}^0_1\text{-}\mathsf{RT}$ 。
• [Afshari–Rathjen09]。整列原理、$\mathsf{WOP}(\lambda \xi.\varphi_\xi(0))$ 。$\xi$ が整列順序であるとき、$\varphi_\xi(0)$ も整列順序である。

$\Pi^1_1\text{-}\mathsf{CA}_0$

以下の定理は $\mathsf{RCA}_0$ 上で $\Pi^1_1\text{-}\mathsf{CA}_0$ と同値であることが証明可能である。

• $\Pi^1_1$-内包性公理。$(\Pi^1_1\text{-}\mathsf{CA})$ 。
• 任意の木 $T\subseteq\mathbb{N}^{<\mathbb{N}}$ は完全核を持つ。
• Cantor–Bendixsonの定理。任意の $\mathbb{N}^\mathbb{N}$ の部分閉集合は完全閉集合と可算集合の和で書ける。
• Cantor–Bendixsonの定理。任意の可分完備距離空間の部分閉集合は完全閉集合と可算集合の和で表せる。
• Silverの定理。余解析的同値関係 $\equiv$ に対して以下のいずれかが成り立つ。
  • ある完全集合 $P$ が存在し任意の $X,Y$ に対し $X,Y\in P$ かつ $X\neq Y$ ならば $X\not\equiv Y$ である。
  • ある点列 $\{Y_n\}_{n\in\mathbb{N}}$ が存在し、任意の $X$ に対し、ある $n$ が存在し $X\equiv Y_n$ である。
• [Friedman–Simpson–Smith83]。任意の可算アーベル群は可除群と被約群の直和で表せる。
• $\mathbf{\Sigma}^0_1\lor\mathbf{\Pi}^0_1$-ゲームは決定的である。
• $\mathbf{\Delta}^0_2\text{-}\mathsf{RT}$ 。
• $\mathbf{\Sigma}^1_0\text{-}\mathsf{RT}$ 。

二階算術での数学の定式化

二階算術に於いて数学の定義や命題などを定式化するのは自明ではない。例えば実数体や複素数体などの非可算な対象は集合として存在しないため、論理式、すなわちクラスとして扱う必要がある。 これは集合論 $\mathsf{ZFC}$ に於いて「全ての集合の集まり」や「全ての群」などがクラスとなることと同様の理由である。以下では一例として $\mathsf{RCA}_0$ にて $\mathbb{R}$ を定義しよう。 まず $\mathbb{N}$ を $(\forall x)[x\in X]$ を満たす唯一の集合とする。以下 $\langle{-}\rangle$ を有限列を符号化する原始再帰関数で復号や列の結合などの操作が全て原始再帰的にできるものとしよう。$\vec{X}\subseteq\mathbb{N}$ に対して直積 $X_0\times\cdots X_{n-1}$ を $\{\langle \vec{X}\rangle\mid (\forall i<n)[x_i\in X_i]\}$ と置く。これらの集合は $(\Delta^0_1\text{-}\mathsf{CA})$ によって存在することが分かる。関数 $f\colon X\to Y$ は $X\times Y$ の部分集合で右全域かつ左一意なものとされる。 同値関係 $\equiv_\mathbb{Z}\subseteq(\mathbb{N}\times\mathbb{N})^2$ を $$\langle m,n\rangle\equiv_\mathbb{Z}\langle i,j\rangle:\Leftrightarrow m+j=n+i$$ と定める。$\mathbb{Z}\subseteq\mathbb{N}^2$ を $=_\mathbb{Z}$ による同値類から最小の符号を持つものを代表元とした集合とする。$\mathbb{Z}$ 上の演算 $+_\mathbb{Z},\times_\mathbb{Z}$ などは以下のように定義される。 $$\langle m,n\rangle+_\mathbb{Z}\langle i,j\rangle:=\langle m+i,n+j\rangle'$$ $$\langle m,n\rangle+_\mathbb{Z}\langle i,j\rangle:=\langle m\cdot i+n\cdot j,m\cdot j+n\cdot i\rangle'$$ ここで $'$ は $\equiv_\mathbb{Z}$ の同値類の最小のものを取っていることを表す。 有理数 $\mathbb{Q}$ は同値関係 $\equiv_\mathbb{Q}\subseteq(\mathbb{Z}\times\mathbb{Z}^+)^2$ 、 $$\langle m,n\rangle\equiv_\mathbb{Q}\langle i,j\rangle:\Leftrightarrow m\times_\mathbb{Z} j=_\mathbb{Z} n\times_\mathbb{Z} i$$ によって整数と同様に定義される。ここで $\mathbb{Z}^+$ は正整数全体である。$\mathbb{Q}$ 上の演算 $+_\mathbb{Q},\times_\mathbb{Q}$ なども $$\langle m,n\rangle+_\mathbb{Q}\langle i,j\rangle:=\langle m\times_\mathbb{Z} j+_\mathbb{Z}n\times_\mathbb{Z} i,n\times_\mathbb{Z} j\rangle'$$ $$\langle m,n\rangle+_\mathbb{Q}\langle i,j\rangle:=\langle m\times_\mathbb{Z} i+_\mathbb{Z} n\times_\mathbb{Z} j,m\times_\mathbb{Z} j+_\mathbb{Z}n\times_\mathbb{Z} i\rangle'$$ と定義できる。実数はCauchy列やDedekind切断による構成が知られているがどちらも $\mathsf{RCA}_0$ では定義できない。よってCauchy列による実数の定義を少し修正して用いる。$\mathbb{R}$ は有理数列 $f\colon\mathbb{N}\to\mathbb{Q}$ で $(\forall n\in\mathbb{N})(\forall i\in\mathbb{N})[|f(n)-f(n+i)|\leq 2^{-n}]$ を満たすものとされる。注意すべきこととして $\mathbb{R}$ は集合とはならないことである。同様に以下で $\mathbb{R}$ 上の関係、演算も定義されるが集合にはならない。また実数の同値類なども定義できないため、同値関係そのものを実数の等号として扱うことも注意しよう。 $$f=_\mathbb{R}g:\Leftrightarrow(\forall n\in\mathbb{N})[|f(n)-g(n)|\leq 2^{-n+1}]$$ $$f<_\mathbb{R}g:\Leftrightarrow(\exists n\in\mathbb{N})[|g(n)-f(n)|> 2^{-n+1}]$$ とし、$f+_\mathbb{R}g$ を $n\mapsto f(n+1)+g(n+1)$ の関数、$f\times_\mathbb{R}g$ を $n\mapsto f(n+m_{f,g})\times g(n+m_{f,g})$ の関数とする。ここで $m_{f,g}:=\min\{i\in\mathbb{N}\mid\max\{|f(0)|,|g(0)|\}+1\leq 2^{i-1}\}$ とする。もちろんこれらが実数になることは証明しなければならないことである。

二階算術の基本的性質と二階算術のモデル

二階算術の基本的な性質を確認する。

定義（二階算術のモデル）

二階算術の言語の構造 $\mathcal{M}$ は一階の対象の領域 $M$ 、二階の対象の領域 $N$ と $\overline{0}^\mathcal{M},\overline{1}^\mathcal{M}\in M,+^\mathcal{M},{\cdot^\mathcal{M}}\colon M^2\to M,=^\mathcal{M},<^\mathcal{M}\subseteq M^2,\in^\mathcal{M}\subseteq M\times N$ からなる組である。 特に通常の自然数 $\omega$ とその冪集合 $\mathcal{P}(\omega)$ 上に通常の演算や関係を考えた構造を標準モデル (standard model) といい $\mathcal{N}$ と表す。また一階の対象の領域が $\omega$ であり、通常の演算と関係を考えた構造を $\omega$-モデル ($\omega$-model) といい、$\omega$-モデル $\mathcal{M}$ で任意の $\mathcal{M}$ によるパラメータを含む $\Pi^1_1$-論理式 $\varphi$ に対し $\mathcal{N}\models\varphi$ と $\mathcal{M}\models\varphi$ が同値になるようなものを$\beta$-モデル ($beta$-model) という。 $\omega$-モデル、$\beta$-モデルに関しては一階の領域 $\omega$ が明らかなので二階の領域 $S$ のみを明示して表すこともある。またモデル $\mathcal{M}$ 上で $\Gamma$-論理式によって定義可能な $N$ の部分集合全体を $\Gamma^\mathcal{M}$ と表し、$\mathcal{M}$ の部分構造 $\mathcal{M}'$ からのパラメータを持って定義可能なとき $\Gamma^\mathcal{M}(\mathcal{M}')$ と表す。 特に $\Gamma^\mathcal{M}(\mathcal{M})$ を $\mathbf{\Gamma}^\mathcal{M}$ と表す。

命題（ビッグ・ファイブの包含関係）

以下が成り立つ。 $$\mathrm{Th}(\mathsf{RCA}_0)\subseteq\mathrm{Th}(\mathsf{WKL}_0)\subseteq\mathrm{Th}(\mathsf{ACA}_0)\subseteq\mathrm{Th}(\mathsf{ATR}_0)\subseteq\mathrm{Th}(\Pi^1_1\text{-}\mathsf{CA}_0)$$ 証明　より一般に $(\Sigma^i_j\text{-}\mathsf{SP})$ から $(\Delta^i_j\text{-}\mathsf{CA})$ が、$(\Sigma^i_j\text{-}\mathsf{CA})$ から $(\Sigma^i_j\text{-}\mathsf{SP})$ が導かれることを見る。 $(\Delta^i_j\text{-}\mathsf{CA})$ は $$(\forall x)[\varphi(x)\leftrightarrow\psi(x)]\to(\exists X)(\forall x)[\varphi(x)\leftrightarrow x\in X].$$ と表わせ、$(\Sigma^i_j\text{-}\mathsf{SP})$ は $$(\forall x)[\varphi(x)\to\psi(x)]\to(\exists X)(\forall x)[(\varphi(x)\to x\in X)\land(x\in X\to\psi(x))].$$ と表せることに注意する。ここで $\varphi\in\Sigma^i_j,\psi\in\Pi^i_j$ で変数 $X$ を含まないとする。 $\mathsf{I}\Sigma^0_1\vdash(\forall x)[\varphi(x)\leftrightarrow\psi(x)]$ であるときに $(\Sigma^i_j\text{-}\mathsf{SP})$ を適用すれば $(\exists X)(\forall x)[(\varphi(x)\to x\in X)\land(x\in X\to\psi(x))]$ であり、$\varphi,\psi$ は同値であることから $(\exists X)(\forall x)[\varphi(x)\leftrightarrow x\in X]$ となり $(\Delta^i_j\text{-}\mathsf{CA})$ が証明できる。

$(\Sigma^i_j\text{-}\mathsf{CA})$ から $(\Sigma^i_j\text{-}\mathsf{SP})$ が導かれることは $(\Sigma^i_j\text{-}\mathsf{CA})$ によって $\varphi(x)\leftrightarrow x\in X$ なる集合 $X$ 取れば明らかに $x\in X\to\psi(x)$ が成り立つので良い。□

命題（ $\mathsf{RCA}_0$ の最小のモデル）

$S$ を $\omega$-モデルとする。このとき ${\mathbf{\Delta}^0_1}^S:={\mathbf{\Sigma}^0_1}^S\cap{\mathbf{\Pi}^0_1}^S$ は $S$ を含む $\mathsf{RCA}_0$ の包含関係に於いて最小の $\omega$-モデルである。

証明　まず $S\subseteq{\mathbf{\Delta}^0_1}^S$ であることを見る $S$ の元 $X$ はパラメータと見做して $x\in X$ は $\Delta^0_0$-論理式であり、従って $\Sigma^0_1$ とも $\Pi^0_1$ とも見做せる。よって$X=\{x\mid S\models x\in X\}\in{\mathbf{\Delta}^0_1}^S$ となり良い。

次に ${\mathbf{\Delta}^0_1}^S$ が $\mathsf{RCA}_0$ のモデルになることを確かめよう。$\omega$-モデルであることから $\mathsf{I}\Sigma^0_1$ のモデルになることは良い。 よって $(\Delta^0_1\text{-}\mathsf{CA})$ を満たすことを確認すれば良い。

まず ${\mathbf{\Delta}^0_1}^S$ によるパラメータを含む論理式 $\varphi$ に対して $S$ からのパラメータを含む論理式 $\varphi'$ を以下のように帰納的に定義する。

1. $(s=t)':\Leftrightarrow s=t$ 。
2. $(s<t)':\Leftrightarrow s<t$ 。
3. $(s\in X)':\Leftrightarrow s\in X$ 。ここで $X$ は自由変数とする。
4. $(s\in C)':\Leftrightarrow \chi(s)$ 。ここで $C$ は $C:=\{n\in\omega\mid S\models \chi(n)\}$ と定義される ${\mathbf{\Delta}^0_1}^S$ の元とする。
5. $(\varphi\circ\psi)':\Leftrightarrow\varphi'\circ\psi'$ とする。ここで $\circ\in\{\land,\lor,\to\}$ とする。
6. $(\lnot\varphi)':\Leftrightarrow\lnot\varphi'$ 。
7. $( (\mathsf{Q} x)\varphi(x) )':\Leftrightarrow(\mathsf{Q}x)\varphi'(x)$ とする。ここで $\mathsf{Q}\in\{\forall,\exists\}$ とする。
8. $( (\mathsf{Q} X)\varphi(X) )':\Leftrightarrow(\mathsf{Q}X)\varphi'(X)$ とする。ここで $\mathsf{Q}\in\{\forall,\exists\}$ とする。

このとき論理式の構成に関する帰納法から以下は互いに同値であることが分かる。

• $S\models\varphi'$ 。
• ${\mathbf{\Delta}^0_1}^S\models\varphi'$ 。
• ${\mathbf{\Delta}^0_1}^S\models\varphi$ 。

またパラメータが ${\mathbf{\Delta}^0_1}^S$ の元であるから、$\varphi$ が $\Sigma^0_1$ 論理式なら $\varphi'$ は $\Sigma^0_1$ 論理式であり、$\varphi$ が $\Pi^0_1$ 論理式なら $\varphi'$ も $\Pi^0_1$ 論理式である。

論理式の $(\Delta^0_1\text{-}\mathsf{CA})$ は $\Sigma^0_1$-論理式 $\varphi(x,\vec{x},\vec{X})$ 、$\Pi^0_1$-論理式 $\psi(x,\vec{x},\vec{X})$ に対して $$(\forall \vec{X})(\forall \vec{x})[(\forall x)[\varphi(x,\vec{x},\vec{X})\leftrightarrow\psi(x,\vec{x},\vec{X})]\to(\exists X)(\forall x)[\varphi(x,\vec{x},\vec{X})\leftrightarrow x\in X]]$$ という形をした論理式の図式であった。よって、任意の $\vec{c}\in{\mathbf{\Delta}^0_1}^S,\vec{c}\in \omega$ に対し、 $${\mathbf{\Delta}^0_1}^S\models(\forall x)[\varphi(x,\vec{c},\vec{X})\leftrightarrow\psi(x,\vec{c},\vec{X})]\to(\exists X)(\forall x)[\varphi(x,\vec{c},\vec{X})\leftrightarrow x\in X]$$ であることを見れば良い。まず ${\mathbf{\Delta}^0_1}^S\models(\forall x)[\varphi(x,\vec{c},\vec{X})\leftrightarrow\psi(x,\vec{c},\vec{X})]$ であると仮定する。 このとき $c\in\omega$ に対し以下は同値である。

• ${\mathbf{\Delta}^0_1}^S\models\varphi(c,\vec{c},\vec{C})$ 。
• ${\mathbf{\Delta}^0_1}^S\models\psi(c,\vec{c},\vec{C})$ 。
• $S\models\varphi'(c,\vec{c})$ 。
• $S\models\psi'(c,\vec{c})$ 。

よって $$\{x\in\omega\mid{\mathbf{\Delta}^0_1}^S\models\varphi(x,\vec{c},\vec{C})\}=\{x\in\omega\mid S\models \varphi'(x)\}=\{x\in\omega\mid S\models\psi'(x)\}$$ である。また ${\mathbf{\Delta^0_1}}^S:={\mathbf{\Sigma^0_1}}^S\cap{\mathbf{\Pi^0_1}}^S$ であるから、以下は同値である。

• $X\in{\mathbf{\Delta^0_1}}^S$ である。
• $S$ からのパラメータを持つ $\Sigma^0_1$-論理式 $\varphi$ と $S$ からのパラメータを持つ $\Pi^0_1$-論理式 $\psi$ が存在し $X=\{x\in\omega\mid S\models \varphi(x)\}=\{x\in\omega\mid S\models\psi(x)\}$ となる。

以上の議論から ${\mathbf{\Delta}^0_1}^S\models(\exists X)(\forall x)[\varphi(x)\leftrightarrow x\in X]$ である。

最小性、すなわち $S\subseteq S'$ となる $S'$ が $\mathsf{RCA}_0$ の $\omega$-モデルであるとき、${\mathbf{\Delta}^0_1}^S\subseteq S'$ であることを確かめる。 $X\in {\mathbf{\Delta}^0_1}^S$ は $S$ からのパラメータを持つ $\Sigma^0_1$-論理式 $\varphi$ と $S$ からのパラメータを持つ $\Pi^0_1$-論理式 $\psi$ に対し $X=\{x\in\omega\mid S\models \varphi(x)\}=\{x\in\omega\mid S\models\psi(x)\}$ と表せる。 よって $S\subseteq S'$ から $$X=\{x\in\omega\mid S\models \varphi(x)\}=\{x\in\omega\mid S\models\psi(x)\}=\{x\in\omega\mid S'\models \varphi(x)\}=\{x\in\omega\mid S'\models\psi(x)\}$$ であり、$S'$ が $\mathsf{RCA}_0$ の $\omega$-モデルであることから $$X=\{x\in\omega\mid S'\models \varphi(x)\}=\{x\in\omega\mid S'\models\psi(x)\}\in S'$$ となる。□

系

$\mathrm{REC}:=\Delta^0_1:=\Sigma^0_1\cap\Pi^0_1$ は $\mathsf{RCA}_0$ の最小の $\omega$-モデルである。

命題（ $\mathsf{ACA}_0$ の最小のモデル）

$S$ を $\omega$-モデルとする。このとき ${\mathbf{\Delta}^1_0}^S$ は $S$ を含む $\mathsf{ACA}_0$ の包含関係に於いて最小の $\omega$-モデルである。

証明　$\varphi$ が算術的なとき $\varphi'$ も適当な算術的論理式と同値になることと $\mathsf{RCA}_0$ 上で $(\Sigma^0_1\text{-}\mathsf{CA})$ と $(\mathsf{ACA})$ が同値であることに気をつけて $\mathsf{RCA}_0$ の最小のモデルの場合と同じような証明をすれば良い。□

系

$\mathrm{ARITH}:=\Delta^1_0$ は $\mathsf{ACA}_0$ の最小の $\omega$-モデルである。

出典

• [Afshari–Rathjen09] B. Afshari, M. Rathjen, Reverse mathematics and well-ordering principles: A pilot study, Annals of Pure and Applied Logic, 160(3):231–237, 2009.
• [Brown–Simpson86] D.K. Brown, S.G. Simpson, Which set existence axioms are needed to prove the separable Hahn–Banach theorem ?, Annals of Pure and Applied Logic, vol. 31, pp. 123–144, 1986.
• [Dean–Walsh16] W. Dean, and S. Walsh, The prehistory of the subsystems of second-order arithmetic. arXiv preprint arXiv:1612.06219:https://arxiv.org/abs/1612.06219 2016.
• [H.Friedman75] H. Friedman, Some systems of second order arithmetic and their use, Proceedings of International Congress of Mathematician, Vancouver 1974, vol. 1, Canadian Mathematical Congress, pp. 235–242, 1975.
• [H.Friedman76] H. Friedman, Some systems of second order arithmetic with restricted induction, I, II (abstracts), The Jounal of Symbolic Logic, vol. 47, pp. 557–559, 1976.
• [Friedman–Simpson–Smith83] H. Friedman, S.G. Simpson, R.L. Smith, Countable algebra and sets existence axioms, Annals of Pure and Applied Logic, vol. 25, pp. 141–181, 1983.
• [Girard87] J.-Y. Girard, Proof theory and logical complexity, Bibliopolis, Naples, 1987.
• [Harington78] L. Harington, Analytic determinacy and $0^\#$, The Journal of Symbolic Logic, vol. 43, pp. 685–693, 1978.
• [Hatzikiriakou–Simpson89] K. Hatzikiriakou, S.G. Simpson, Countable valued fields in weak subsystems of second order arithmetic, Annals of Pure and Applied Logic, vol. 41, pp. 27–32, 1989.
• [Hatzikiriakou–Simpson90] K. Hatzikiriakou, S.G. Simpson, $\mathsf{WKL}_0$ and ordering of countable Abelian groups, in [Sieg90], pp. 177–180, 1990.
• [Kihara20] T. Kihara, The Brouwer invariance theorems in reverse mathematics, arXiv preprint, arXiv:2002.10715:https://arxiv.org/abs/2002.10715, 2020.
• [Sakamoto–Yokoyama07] N. Sakamoto, and K. Yokoyama, The Jordan curve theorem and the Schönflies theorem in weak second-order arithmetic, Archive for Mathematical Logic 46.5–6, 465, 2007.
• [Shioji–Tanaka90] N. Shioji, K. Tanaka. Fixed point theory in weak second-order arithmetic. Annals of Pure and Applied Logic, 47.2, 167–188, 1990.
• [Sieg90] W. Sieg ed., Logic and Computation, Contemporary Mathematics, American Mathematical Society, 1990.
• [Simpson84] S.G. Simpson, Which set existence axioms are needed to prove the Cauchy/Peano theorem for ordinary differential equation ?, The Journal of Symbolic Logic, vol. 49, pp. 783–802, 1984
• [Simpson05] S.G. Simpson ed., Reverse Mathematics 2001, Lecture Notes in Logic, vol. 21, Association for Symbolic Logic, 2005.
• [Simpson09] S.G. Simpson, Subsystems of Second Order Arithmetic, Perspectives in Logic, 2nd edn. Cambridge UP, Cambridge 2009.
• [Simpson–Yokoyama13] S.G. Simpson, K. Yokoyama, Reverse mathematics and Peano categoricity, Annals of Pure and Applied Logic 164.3, 284–293, 2013.
• [田中02] 田中一之。数の体系と超準モデル。裳華房。2002。
• [Tanaka–Yamazaki00] K. Tanaka, T. Yamazaki, A non-standard construction of Haar measure and weak König's lemma, The Journal of Symbolic Logic 65.1, 173–186, 2000.
• [Tanaka–Yamazaki05] K. Tanaka, T. Yamazaki, Manipulating the reals in $\mathsf{RCA}_0$. in [Simpson05], pp. 379–393, 2005.
• [Yokoyama07] K. Yokoyama, Non‐standard analysis in $\mathsf{ACA}_0$ and Riemann mapping theorem, Mathematical Logic Quarterly 53.2, 132–146, 2007.