逆数学

逆数学とは、数学の定理の証明に必要な公理を決定しようとする数理論理学のプログラムである。簡単に言えば、通常の数学が公理から定理を導くのとは逆に、「定理から公理を証明する」手法を用いることが特徴である。「選択公理とツォルンの補題はZF上で同値である」、というような集合論の古典的定理は、逆数学プログラムの予兆となるものだった。しかし、実際の逆数学では主に、集合論の公理ではなく、通常の数学の定理を研究するのを目的とする。

逆数学は大抵の場合、2階算術について実行され、定理が構成的解析と証明論に動機付けられた2階算術の部分体系のうち、どれに対応するのかを研究する。 2階算術を使うことで、再帰理論からの多くの技術も利用できる。実際、逆数学の結果の多くは、計算可能性解析の結果を反映している。

逆数学は、テンプレート:Harvsによってはじめて言及された。基本文献は{{#invoke:Footnotes | harvard_citation }}を参照。

一般的な原理

逆数学は、フレームとなる言語と基本的な公理からはじめる。例えば、“すべての実数の有界な列は上限をもつ”という定理の研究には、実数と実数の列を定義する公理が必要となる。

基本体系において証明できない定理からはじめて、定理を証明するのに必要な(基本体系よりも強い)公理を決定することを目標とする。定理[math]T \, [/math]とそれを証明可能な場合の体系[math]S \, [/math]との関係を示す2つの証明がある。1つ目は、[math]S \, [/math]から[math]T \, [/math]が証明可能であることの証明である。このとき普通の数学の定理は体系[math]S \, [/math]で成り立つ。2つ目は*逆方向*、すなわち[math]T \, [/math]が[math]S \, [/math]と同値であることであることの基本体系における証明である。逆方向の証明ができれば、[math]S \, [/math]より弱い体系[math]S^\prime \, [/math]であって[math]T \, [/math]を証明できるようなものは存在しないことが分かる。

2階算術の使用

逆数学は2階算術の部分体系において研究されることが多い。その場合、数学的対象を自然数と自然数の集合によって形式化しなければならない。例えば、自然数のペアを1つの自然数として表現することができ、自然数のペアによって有理数を表現する。有理数の集合（これは結局、自然数の集合として表現される）によって有理数の列を表現し、有理数の列のうちコーシー列であるようなものによって実数を表現することができる。逆数学の研究においては、弱い部分体系であって数学的対象を形式化できる程度には強い体系を基本体系として用いる。

逆数学が集合論ではなく2階算術を用いるのは、弱い部分体系であって数学的対象を形式化できる程度には強い体系を2階算術では自然に定義することができるからである。

2階算術を使う場合、数学の定理を制限しなければならない。例えば、2階算術では一般のベクトル空間は表現できない。そのため"すべてのベクトル空間は基底をもつ"という一般的な原理は表現できないが、"すべての可算なベクトル空間は基底をもつ"という原理は表現することができる。同様に、代数の定理の対象は可算な群や環や体についてのものになる。また、距離空間を対象とする解析や位相の定理は、実数を有理数のコーシー列によって表現したのと同様の手法により、可分な距離空間について考察することができる。なお、定理を可算なものに制限した場合、本来の定理とその強さが全く異なる場合がある。例えば、"すべての体は代数的閉体をもつ"はZF集合論では証明できないが、"すべての可算な体は代数的閉体をもつ"と制限すれば、非常に弱い弱い形式体系である[math]\mbox{RCA}_0 \, [/math]でも証明することができる。

2階算術の5つの基本的部分体系(Big Five)

2階算術の部分体系 [math]\mbox{RCA}_0 \, [/math]、[math]\mbox{WKL}_0 \, [/math]、[math]\mbox{ACA}_0 \, [/math]、[math]\mbox{ATR}_0 \, [/math]、[math]\Pi^1_1\mbox{-CA}_0 \, [/math]は, Big Fiveと呼ばれ、逆数学において頻繁に扱われるものである。

次は"big five"の特徴である。Simpson (2009, p.42)参照。

部分体系	名称の由来	証明論的順序数	対応する哲学的原理	備考
[math]\mbox{RCA}_0 \, [/math]	Recursive comprehension axiom(再帰的内包公理)	[math]\omega^\omega \, [/math]	構成的数学 (Bishop)	逆数学の基本体系
[math]\mbox{WKL}_0 \, [/math]	Weak König's lemma(弱ケーニッヒの補題)	[math]\omega^\omega \, [/math]	有限還元 (Hilbert)	PRA上で[math]\Pi^0_2 \, [/math]文を、[math]\mbox{RCA}_0 \, [/math]上で[math]\Pi^1_1 \, [/math]文を保存する。
[math]\mbox{ACA}_0 \, [/math]	Arithmetical comprehension axiom(算術的内包公理)	[math]\epsilon_0 \, [/math]	可述主義 (Weyl, Feferman)	ペアノ算術上で算術的文を保存する。
[math]\mbox{ATR}_0 \, [/math]	Arithmetical transfinite recursion(算術的超限再帰)	[math]\Gamma_0 \, [/math]	可述的還元主義 (Friedman, Simpson)	フィッファーマン体系IR上で[math]\Pi^1_1 \, [/math]文を保存する。
[math]\Pi^1_1\mbox{-CA}_0 \, [/math]	[math]\Pi^1_1 \, [/math] comprehension axiom ([math]\Pi^1_1 \, [/math]内包公理)	[math]\Psi_0 \, [/math]([math]\Omega_\omega \, [/math])	非可述主義

なお, Big Fiveの名前についている [math]{}_0 \, [/math]は帰納法の図式が制限されていることを意味する。例えば、[math]\mbox{ACA}_0 \, [/math]は算術的論理式についての帰納法しか持たない。帰納法を制限した体系は、一般の2階算術の論理式についての帰納法をもつ体系に比べ、大幅に小さい証明論的順序数を持つ。

再帰的内包公理 [math]\mbox{RCA}_0 \, [/math]

[math]\mbox{RCA}_0 \, [/math]は、「ロビンソン算術の公理」＋「[math]\Sigma^0_1 \, [/math]論理式に対する帰納法の公理」＋「[math]\Delta^0_1 \, [/math]論理式に対する内包公理」からなる部分体系である。

[math]\mbox{RCA}_0 \, [/math]は逆数学で最も多用される体系である。[math]\mbox{RCA}_0 \, [/math]は"再帰的内包公理"と呼ばれ、"再帰的"とは"計算可能"を意味している。この名称は[math]\mbox{RCA}_0 \, [/math]が"計算可能性数学"に類似しているからである。[math]\mbox{RCA}_0 \, [/math]で存在が証明可能な自然数の集合は計算可能である、よって計算不可能な集合の存在は[math]\mbox{RCA}_0 \, [/math]で証明できない。

[math]\mbox{RCA}_0 \, [/math]はBig Fiveで最弱だが、古典的数学の対象を形式化できる。また、以下の定理が証明可能である。

自然数全体、整数全体、有理数全体の成す集合の基本性質(例えば、有理数全体が順序体を成すこと)。
実数全体の成す集合の基本性質(実数全体がアルキメデス順序体であること、長さが0に近付く任意の包含閉区間列の交叉が1点のみからなること、実数は非可算であること)。
完備可分距離空間におけるベールの範疇定理。
実連続関数における中間値の定理。
可分バナッハ空間における連続線形演算子の列に関するバナッハ–シュタインハウスの定理。
弱いゲーデルの完全性定理。
可算な体での代数的閉体の存在(一意性は除く)。
可算な順序体の実閉体の存在と一意性。

[math]\mbox{RCA}_0 \, [/math]の1階部分は、[math]\mbox{I}\Sigma_1 \, [/math]（ペアノ算術の帰納法を[math]\Sigma_1 \, [/math]論理式に制限した体系）と一致する。

弱ケーニッヒの補題 [math]\mbox{WKL}_0 \, [/math]

[math]\mbox{WKL}_0 \, [/math]は、[math]\mbox{RCA}_0 \, [/math]に弱ケーニッヒの補題（すべての無限二分木は無限路をもつ）を付け加えた体系である。

弱ケーニッヒの補題は選択公理に近く、実際[math]\text{RCA}_0 \, [/math]において、[math]\Pi^1_1 \, [/math]選択公理と[math]\text{WKL}_0 \, [/math]が同値であることを示せる。また、[math]\Sigma^0_1 \, [/math]分離原理とも同値になる。

[math]\mbox{WKL}_0 \, [/math]は、[math]\mbox{RCA}_0 \, [/math]よりも証明能力が高く、[math]\mbox{WKL}_0 \, [/math]では非計算可能集合の存在を示せる。

[math]\mbox{RCA}_0 \, [/math]と[math]\mbox{WKL}_0 \, [/math]の1階部分は同じ、つまり算術的な定理については証明能力は同じである。しかし、[math]\mbox{WKL}_0 \, [/math]で証明可能で、[math]\mbox{RCA}_0 \, [/math]では証明不可能な古典的数学の定理もある。これらの結果は2階部分の証明能力の違いを示している。

[math]\mbox{RCA}_0 \, [/math]上で、[math]\mbox{WKL}_0 \, [/math]と以下の定理が同値であることが示せる。

実数からなる単位閉区間に対する（開区間による任意の被覆が有限部分被覆を持つという意味での）ハイネ＝ボレルの定理。
完備全有界可分距離空間に対する（開球体列による被覆についての）ハイネ＝ボレルの定理。
単位閉区間（もしくは任意のコンパクト可分距離空間）上の連続実函数が有界であること（もしくは有界かつその境界値を実現する点が存在すること）。
単位閉区間上の連続実函数が有理係数多項式で一様に近似できること。
単位閉区間上の連続実函数が一様連続であること。
単位閉区間上の連続実函数がリーマン積分可能であること。
単位閉区間の有限個のコピーの直積上の連続函数に対するブラウワーの不動点定理。
可分バナッハ空間の部分空間上の有界線型形式が全体空間上の有界線型形式に拡張できるという形での可分ハーン＝バナッハの定理。
ジョルダンの閉曲線定理
可算言語に対するゲーデルの完全性定理。
任意の可算可換環が素イデアルを持つこと。
任意の可算形式的実体を順序体にできること。
可算体に対する代数閉包の一意性。

算術的内包公理 [math]\mbox{ACA}_0 \, [/math]

[math]\mbox{ACA}_0 \, [/math]は、[math]\mbox{RCA}_0 \, [/math]に算術的内包公理を付け加えた体系である。[math]\mbox{ACA}_0 \, [/math]は、任意の算術的論理式を満たす自然数の集合の存在を示す。実際、算術的内包公理を得るために、[math]\mbox{RCA}_0 \, [/math]にΣ₁論理式の内包公理を追加したものである。

[math]\mbox{ACA}_0 \, [/math]の1階部分はペアノ算術と同じである。つまり[math]\mbox{ACA}_0 \, [/math]は算術的な定理についてはにペアノ算術と証明能力は同じである。また、両者は無矛盾性については等価である。

[math]\mbox{ACA}_0 \, [/math]は、可述的数学のほとんどを展開することができ、古典的数学の基本的な定理の多くを証明することができる。

算術的集合を含まない[math]\mbox{WKL}_0 \, [/math]のモデルが存在するので、[math]\mbox{ACA}_0 \, [/math]は[math]\mbox{WKL}_0 \, [/math]よりも強いことが示される。実際、低基底定理を使った低集合を含むような[math]\mbox{WKL}_0 \, [/math]のモデルは構成不可能。

[math]\mbox{RCA}_0 \, [/math]上で次と[math]\mbox{ACA}_0 \, [/math]は同値。

実数全体の集合の点列コンパクト性（有界で単調増加な任意の実数列は極限を持つ）。
ボルツァーノ＝ワイエルシュトラスの定理。
アスコリの定理: 単位閉区間上の任意の有界で同程度連続な実関数列は一様収束する部分列を持つ。
任意の可算可換環は極大イデアルを持つ。
有理数体（もしくは任意の可算体）上の任意の可算ベクトル空間は基底を持つ。
任意の可算体は超越基底を持つ。
（任意の有限分岐木に対する、弱でない）ケーニヒの補題。
ラムゼーの定理の一形態などを例とする組合せ論の諸定理。

算術的超限再帰 [math]\mbox{ATR}_0 \, [/math]

[math]\mbox{ATR}_0 \, [/math]は、[math]\mbox{ACA}_0 \, [/math]に算術的超限再帰を追加した体系である。

[math]\mbox{ATR}_0 \, [/math]は[math]\mbox{ACA}_0 \, [/math]上で、Σ¹₁分離原理と同値である。

[math]\mbox{ATR}_0 \, [/math]は、[math]\mbox{ACA}_0 \, [/math]の無矛盾性を証明可能なのでゲーデルの不完全性定理より、[math]\mbox{ACA}_0 \, [/math]より強い。

[math]\mbox{RCA}_0 \, [/math]で次が[math]\mbox{ATR}_0 \, [/math]と同値。

任意の二つの可算整列順序は比較可能（一方が他方または他方の始片に同型）である。
可算被約アーベル群に対するウルムの定理。
完備可分距離空間の任意の非可算閉部分集合が完全閉集合を含むことを述べた完全集合定理。
ルージンの分離定理（essentially [math]\Sigma^1_1 \, [/math]分離）。
ベール空間における開集合の決定性。

[math]\Pi^1_1 \, [/math]内包公理 [math]\Pi^1_1\mbox{-CA}_0 \, [/math]

[math]\Pi^1_1\text{-CA}_0 \, [/math]は、[math]\mbox{RCA}_0 \, [/math]に[math]\Pi^1_1 \, [/math]論理式に関する内包公理を追加した体系である。[math]\Pi^1_1\text{-CA}_0 \, [/math]は非可述的な体系である。

[math]\Pi^1_1\text{-CA}_0 \, [/math]と[math]\text{ATR}_0 \, [/math]の関係は、[math]\text{ACA}_0 \, [/math]と[math]\text{WKL}_0 \, [/math]の関係に似ている。

[math]\Pi^1_1\text{-CA}_0 \, [/math]は、記述的集合論における強い非可述的論法によって証明される定理と同値になる。この同値性はこれらの非可述的論法が取り除けないことを示している。

[math]\mbox{RCA}_0 \, [/math]で、[math]\Pi^1_1\mbox{-CA}_0 \, [/math]と次の定理が同値であることが証明できる。

カントール＝ベンディクソンの定理（実数から成る任意の閉集合は完全集合と可算集合の和集合として書ける）。
任意の可算アーベル群は可除群と被約群の直和として書ける。

Big Five以外の体系

逆数学においては、Big Five以外の体系も研究されている。それらはAfter Fiveとも呼ばれる。

再帰的内包公理よりも弱い体系が定義できる。[math]\mbox{RCA}^\ast_0 \, [/math]は、初等関数算術EFA(算術の基本公理 + [math]\Delta^0_0 \, [/math]帰納法)に[math]\Delta^0_1 \, [/math]内包公理を付け加えた体系である。[math]\mbox{RCA}^\ast_0 \, [/math]上で、[math]\mbox{RCA}_0 \, [/math]は、可算な体の上で多項式が高々有限の根しかもたないことや、有限アーベル群の分類定理などと同値である。

[math]\mbox{RCA}_0^\ast \, [/math]は[math]\mbox{EFA} \, [/math]と同じ証明論的順序数 [math]\omega^3 \, [/math]をもち、[math]\mbox{EFA} \, [/math]上[math]\Pi^0_2 \, [/math]文について保存的な拡大になっている。

[math]\mbox{WWKL}_0 \, [/math]は、[math]\mbox{RCA}_0 \, [/math]に弱弱ケーニッヒの補題「無限路を持たない無限2進木のある部分木は、長さ[math]n \, [/math]の葉がどれだけ存在するかを一様に推定できる」を追加した公理系である。[math]\mbox{WWKL}_0 \, [/math]は、[math]\mbox{RCA}_0 \, [/math]上で「任意のコンパクト距離空間における任意のボレル測度は可算加法的である」等の測度論の定理と同値になる。[math]\mbox{WWKL}_0 \, [/math]のモデル理論は、アルゴリズム的ランダム列の理論と関連する。実際、[math]\mbox{RCA}_0 \, [/math]の[math]\omega \, [/math]-モデル[math]M \, [/math]に対し, [math]M \, [/math]が[math]\mbox{WWKL}_0 \, [/math]のモデルであることと, [math]M \, [/math]に含まれる任意の集合[math]X \, [/math]について、[math]X \, [/math]に対し相対的に1-randomなある[math]Y \, [/math]が存在して[math]Y \, [/math]が[math]M \, [/math]に含まれることは同値である。
DNR("diagonally non-recursive"の略)は、[math]\mbox{RCA}_0 \, [/math]に「任意の集合に対し対角的非再帰な関数が存在する」を追加した公理系である。[math]\mbox{DNR} \, [/math]とはつまり「任意の集合[math]A \, [/math]に対して、ある全域的関数[math]f \, [/math]が存在して、fは[math]A \, [/math]から計算可能などんな部分関数とも等しくない」が成り立つということである。[math]\mbox{DNR} \, [/math]は、[math]\mbox{WWKL}_0 \, [/math]よりも真に弱い。(Lempp et al., 2004).
「超算術的な集合全体からなる構造の上で成り立つ」「極小[math]\omega \, [/math]モデルは超算術的な集合全体である」という性質を満たす公理系はTheory of hyperarithmetic analysisと呼ばれる。

Theory of hyperarithmetic analysisの例として、[math]\mbox{weak-}\Sigma^1_1\mbox{-AC}_0 \, [/math]、[math]\Delta^1_1\mbox{-CA}_0 \, [/math]、[math]\Pi^1_1\mbox{-SEP}_0 \, [/math]、[math]\Sigma^1_1\mbox{-AC}_0 \, [/math]はTheory of hyperarithmetic analysisがあり、それぞれ[math]\mbox{ACA}_0 \, [/math]に弱[math]\Sigma^1_1 \, [/math]選択公理、[math]\Delta^1_1 \, [/math]内包公理、[math]\Pi^1_1 \, [/math]分離公理、[math]\Sigma^1_1 \, [/math]選択公理を追加した公理系である。

[math]\omega \, [/math]-モデルと[math]\beta \, [/math]-モデル

「[math]\omega \, [/math]-モデル」の[math]\omega \, [/math]は非負整数全体の集合を意味する。

その1階部分が1階ペアノ算術の標準モデルになっているような、2階算術の部分体系のモデルを[math]\omega \, [/math]-モデルと呼ぶ。ただし、2階部分は非標準であっても良い。すなわち、[math]\omega \, [/math]-モデルは[math]S \subseteq \mathcal{P}(\omega) \, [/math]（[math]\mathcal{P}(\omega) \, [/math]は[math]\omega \, [/math]の部分集合全体のクラス）によって与えられる。数変数は [math]\omega \, [/math]の元として解釈され、定数記号[math]0, 1 \, [/math]や関数記号[math]+, \times \, [/math]は標準的に解釈される。一方、集合変数は [math]S \, [/math]の元として解釈される。[math]S = \mathcal{P}(\omega) \, [/math]とする[math]\omega \, [/math]-モデルを2階算術の標準モデルと呼ぶ。しかし、標準モデル以外にも[math]\omega \, [/math]-モデルは存在する。たとえば、[math]\mbox{RCA}_0 \, [/math]は[math]S \, [/math]として計算可能な[math]\omega \, [/math]の部分集合全体をとった[math]\omega \, [/math]-モデルをもつ。

[math]\omega \, [/math]-モデルであって、[math]\Sigma^1_1 \, [/math]文について、標準モデルと真偽が一致するものを[math]\beta \, [/math]-モデルと呼ぶ。[math]\mbox{ACA}_0 \, [/math]において全ての[math]\beta \, [/math]-モデルが[math]\mbox{ATR}_0 \, [/math]のモデルであることが示せる。また、[math]\mbox{ACA}_0 \, [/math]において、「任意の集合[math]X \, [/math]について[math]X \, [/math]を含む[math]\beta \, [/math]モデルが存在する」は [math]\Pi^1_1\mbox{-CA}_0 \, [/math]と同値である。

一般に、[math]\omega \, [/math]-モデルであって、[math]\Sigma^1_n \, [/math]文について、標準モデルと真偽が一致するものは[math]\beta_n \, [/math]-モデルと呼ばれる。

また、Non-[math]\omega \, [/math]-モデル（1階部分が標準ではないモデル）も、ある公理系が保存的拡大であることの証明にしばしば登場する。

参考文献

Ambos-Spies, K.; Kjos-Hanssen, B.; Lempp, S.; Slaman, T.A. (2004), “Comparing DNR and WWKL”, Journal of Symbolic Logic 69 (4): 1089, doi:10.2178/jsl/1102022212.

Friedman, Harvey (1975), “Some systems of second order arithmetic and their use”, Proceedings of the International Congress of Mathematicians (Vancouver, B. C., 1974), Vol. 1, Canad. Math. Congress, Montreal, Que., pp. 235–242, MR 0429508
Friedman, Harvey (1976), Systems of second order arithmetic with restricted induction, I, II, “Meeting of the Association for Symbolic Logic”, The Journal of Symbolic Logic (Association for Symbolic Logic) 41 (2): 557–559, ISSN 0022-4812
Simpson, Stephen G. (2009), Subsystems of second order arithmetic, Perspectives in Logic (2nd ed.), Cambridge University Press, ISBN 978-0-521-88439-6, MR 2517689
Solomon, Reed (1999), “Ordered groups: a case study in reverse mathematics”, The Bulletin of Symbolic Logic 5 (1): 45–58, doi:10.2307/421140, ISSN 1079-8986, MR 1681895, http://www.jstor.org/stable/421140

外部リンク

逆数学

Contents