逆数学

同義語：reverse mathematics

概要

逆数学（reverse mathematics）とは、弱い基礎理論の上で数学的定理と集合存在公理の両方向の含意を証明し、その定理に必要な公理の強さを測る研究方法である。本記事では二階算術、ビッグ・ファイブ、RCA0からACA0への包含、ACA0による弱König補題の導出を扱う。通常の解析定理と二階算術内でコード化された版、含意と同値、形式体系とその定理集合、古典的逆数学と構成的数学を区別する。

$$\newcommand{C}[0]{\mathbb{C}} \newcommand{N}[0]{\mathbb{N}} \newcommand{Q}[0]{\mathbb{Q}} \newcommand{R}[0]{\mathbb{R}} \newcommand{Z}[0]{\mathbb{Z}} $$

前提知識: 計算可能関数, 数理論理学

逆数学の考え方

定理から公理を測る方法

逆数学（reverse mathematics）とは、弱い基礎理論 $B$ を固定し、数学的定理 $T$ と公理体系 $S$ について $B+S\vdash T$ かつ $B+T\vdash S$ の両方を証明することで、$T$ に必要な集合存在公理の強さを測る研究方法である。このとき「$T$ は $B$ 上で $S$ と同値である」という。通常は公理から定理を導く（$B+S\vdash T$）のに対し、逆向き $B+T\vdash S$ も証明することが名称の由来である。

ここで「$S$ が $T$ を証明する」という含意と、「$B$ 上で $T$ と $S$ が同値である」という結論は異なる。後者には逆向きの証明が必要であり、一方の含意だけでは公理の必要性は分からない。

二階算術

二階算術

二階算術（second-order arithmetic）は、数変数 $m,n,\ldots$ と、自然数の集合を表す集合変数 $X,Y,\ldots$ を持つ二種類の変数の一階理論である。標準的な言語 $L_2$ は $0,1,+,\cdot,<,\in$ を持ち、$n\in X$ だけが数と集合の間の所属を表す。
完全な二階算術 $\mathsf Z_2$ は、自然数算術の基本公理、数学的帰納法の公理、および $L_2$ の式で定義される自然数集合の存在を主張する内包公理図式を持つ。ここでいう「二階」は集合変数があることを指し、集合変数を標準的な冪集合全体にわたらせる完全二階意味論を採用する、という意味ではない。逆数学では、この形式理論の部分体系を比較する。Sim09

数量化子だけを持ち、集合量化子を持たない $L_2$ の式を算術的という。$\Delta^0_1$ 内包は、$\varphi$ を $\Sigma^0_1$ 式、$\psi$ を $\Pi^0_1$ 式（いずれも $X$ を自由に含まない）として、図式
$$ \forall n\,(\varphi(n)\leftrightarrow\psi(n))\to\exists X\,\forall n\,(n\in X\leftrightarrow\varphi(n)) $$
の各事例を公理とする公理図式である。すなわち、$\Sigma^0_1$ 式と $\Pi^0_1$ 式が同じ述語を定めるとき、その述語の外延を集合として取る。算術的内包は、任意の算術的な式 $\varphi$ について $\exists X\,\forall n\,(n\in X\leftrightarrow\varphi(n))$ を公理とし、算術的な式の外延を集合として取る。

数学的対象のコード化

二階算術の集合対象は自然数の部分集合なので、実数、連続関数、可算距離空間、開集合族などを扱うときは自然数によるコードを用いる。例えば実数は、所定の収束率を持つ有理数の Cauchy列のコードとして表せる。したがって逆数学で解析定理を述べるには、対象のコード、等号、連続性、被覆などの表現を固定しなければならない。同じ日本語名を持つ通常数学の定理と、特定のコード化を施した $L_2$ の文は同一の文ではない。

二階算術のモデル

$L_2$ のモデルは、数の領域と集合の領域を別に持つ。数の領域が標準自然数 $\mathbb N$ であるものを ω-モデル（$\omega$-モデル）という。$\mathsf{RCA}_0$ の最小 $\omega$-モデルの集合領域は計算可能集合全体であり、$\mathsf{ACA}_0$ の最小 $\omega$-モデルの集合領域は算術的集合全体である。これらの記述は、形式体系そのものと、そのモデルの集合領域とを区別した記述である。Sim09

ビッグ・ファイブ

五つの基本体系

逆数学で繰り返し現れる次の五体系をビッグ・ファイブ（Big Five）という。

  • $\mathsf{RCA}_0$（再帰的内包公理系）は、基本算術公理、$\Sigma^0_1$ 帰納法、$\Delta^0_1$ 内包を持つ。多くの議論で基礎理論 $B$ として用いられる。
  • $\mathsf{WKL}_0$ は $\mathsf{RCA}_0$ に弱 König 補題、すなわち「コード化された無限二分木 $T\subseteq 2^{<\mathbb N}$ は無限枝を持つ」を加えた体系である。
  • $\mathsf{ACA}_0$（算術的内包公理系）は、算術的な式についての内包を許す体系である。
  • $\mathsf{ATR}_0$（算術的超限再帰）は、コード化された可算整列順序に沿う算術的な超限再帰を許す体系である。
  • $\Pi^1_1\text{-}\mathsf{CA}_0$ は、$\Pi^1_1$ 式についての内包を許す体系である。
    これらの説明は主公理を示したものである。帰納法や内包・分離図式を使う別の標準的表示は、共通の弱い基礎の上で同値になることを確認してから交換する必要がある。Sim09

共通言語で証明できる文の集合を $\operatorname{Th}(S)$ と書けば、標準的な定式化のもとで
$$ \operatorname{Th}(\mathsf{RCA}_0) \subsetneq \operatorname{Th}(\mathsf{WKL}_0) \subsetneq \operatorname{Th}(\mathsf{ACA}_0) \subsetneq \operatorname{Th}(\mathsf{ATR}_0) \subsetneq \operatorname{Th}(\Pi^1_1\text{-}\mathsf{CA}_0) $$
となる。これは単なる公理列の文字列としての集合包含ではなく、各体系が証明する文の強さの比較である。真の包含の証明には分離するモデルや保存定理を用いる部分があり、本記事では外部結果として採用する。Sim09

基本的な包含

再帰的内包から算術的内包への包含

$\mathsf{RCA}_0$ の各公理は $\mathsf{ACA}_0$ で証明できる。したがって
$$ \operatorname{Th}(\mathsf{RCA}_0)\subseteq \operatorname{Th}(\mathsf{ACA}_0) $$
である。

包含の確認

$\mathsf{ACA}_0$ の算術的内包は、とくに $\Delta^0_1$ 式についての内包を含む。また算術的帰納法は $\Sigma^0_1$ 式についての帰納法を含む。基本算術公理は共通である。ゆえに $\mathsf{RCA}_0$ の各公理図式の各事例が $\mathsf{ACA}_0$ で証明できる。証明の翻訳により、$\mathsf{RCA}_0$ の定理はすべて $\mathsf{ACA}_0$ の定理でもある。

算術的内包から弱König補題を導く

$\mathsf{ACA}_0$ は、任意のコード化された無限二分木 $T\subseteq 2^{<\mathbb N}$ が無限枝を持つことを証明する。したがって
$$ \operatorname{Th}(\mathsf{WKL}_0)\subseteq \operatorname{Th}(\mathsf{ACA}_0) $$
である。

無限に延長できる節点をたどる

$T\subseteq2^{<\mathbb N}$ を無限二分木とする。節点 $\sigma\in T$ について
$$ P(\sigma)\;:\Longleftrightarrow\;(\forall m)(\exists\tau\in T)\bigl(|\tau|\ge m\ \land\ \sigma\preceq\tau\bigr) $$
とおく。これは数についてだけ量化する算術的条件なので、算術的内包により $P(\sigma)$ を満たす節点全体 $T^*$ を集合として取れる。$T$ が無限で木であることから空列は $T^*$ に属する。
$\sigma\in T^*$ なら、$\sigma{}^\frown0$ と $\sigma{}^\frown1$ の少なくとも一方が $T^*$ に属する。実際、両方が無限に延長できないなら、それぞれの延長の長さに上限があり、その二つの上限の大きい方が $\sigma$ の延長の長さの上限となって $P(\sigma)$ に反する。
そこで $f(0)$ を空列とし、$f(n)\in T^*$ から、$f(n){}^\frown0\in T^*$ ならそれを $f(n+1)$ とし、そうでなければ $f(n){}^\frown1$ を $f(n+1)$ とする。この原始再帰で定めた有限列の和は $T$ の無限枝である。以上の構成は算術的内包と数についての再帰の範囲で行えるので、$\mathsf{ACA}_0$ は弱 König 補題を証明する。Sim09

この証明は $\mathsf{WKL}_0$ と $\mathsf{ACA}_0$ の同値を示してはいない。逆向きは成り立たず、両者の間の包含は真である。

解析・代数の定理を測る例

次の各例は通常数学の定理をそのまま文字列として二階算術へ移したものではない。数列、実数、開区間列、体、ベクトル空間を自然数集合でコード化した版についての同値である。

有界実数列の収束部分列

$\mathsf{RCA}_0$ 上で、「コード化された有界実数列は収束部分列を持つ」は $\mathsf{ACA}_0$ と同値である。これは通常の Bolzano-Weierstrassの定理 の逆数学での定式化である。Sim09

Heine-Borel被覆補題

$\mathsf{RCA}_0$ 上で、「閉区間 $[0,1]$ を覆うようにコード化された開区間の列には有限部分被覆がある」は $\mathsf{WKL}_0$ と同値である。任意の開被覆を集合として量化する通常の Heine-Borelの定理 と、開区間列で表された被覆とを一括りにしてはいけない。Sim09

可算ベクトル空間の基底

$\mathsf{RCA}_0$ 上で、「任意の可算体上のコード化された可算ベクトル空間は基底を持つ」は $\mathsf{ACA}_0$ と同値である。ここで対象は集合論的に任意の濃度を持つベクトル空間ではない。Sim09

基礎理論だけで証明できる場合

コード化された連続実関数についての 中間値の定理 は $\mathsf{RCA}_0$ で証明できる。したがって「解析学の定理なら必ず $\mathsf{WKL}_0$ 以上を必要とする」という含意は破れる。この例は、分野名だけで強さを決めず、定理の定式化ごとに両方向を調べる必要を示す。Sim09

構成的数学との区別

古典的逆数学と構成的数学

標準的な逆数学は古典論理を用い、弱い古典的基礎理論の上で定理と集合存在公理の同値を調べる。構成的数学は、証明や存在の意味、採用する論理を構成的に制限する研究を含む。$\mathsf{RCA}_0$ が計算可能数学と近い内容を持つことだけから、逆数学を構成的数学の一種と同一視することはできない。構成的な基礎の上で同様の較正を行う構成的逆数学は、古典的逆数学と区別して扱う。

関連項目

参考文献

Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する

Mathpediaを支援する
逆数学