逆数学

逆数学は、数学の定理を証明するためにどの公理が必要かを決定する数理論理学のプログラムです。その定義方法は、公理から定理を導き出す通常の数学的実践とは対照的に、「定理から公理へ逆方向に進む」と簡単に説明できます。これは、十分な条件から必要な条件を彫り出すこととして概念化できます。

逆数学プログラムは、選択公理とツォルンの補題がZF 集合論上で同値であるという古典的な定理などの集合論の結果によって予兆されていました。しかし、逆数学の目標は、集合論の可能な公理ではなく、数学の通常の定理の可能な公理を研究することです。

逆数学は通常、 2階算術のサブシステムを使用して実行されます。^[1]その定義と方法の多くは、構成的解析と証明理論の以前の研究に触発されています。2階算術を使用すると、再帰理論の多くの手法を使用することもできます。逆数学の多くの結果は、計算可能解析の対応する結果を持っています。高階逆数学では、高階算術のサブシステムと、関連するより豊富な言語に焦点が当てられています。 ^{[説明が必要]}

このプログラムはハーヴェイ・フリードマン （1975、1976）^[2]によって創設され、スティーブ・シンプソンによって推進された。この分野の標準的な参考文献はシンプソン（2009）であり、非専門家向けの入門書はスティルウェル（2018）である。高階逆数学の入門書であり、創始論文でもあるのはコーレンバッハ（2005）である。主要な結果と方法を網羅した包括的な入門書はジャファロフとムメルト（2022）^{[3]である。} harvtxt error: no target: CITEREFDzhafarov_and_Mummert2022 (help)

逆数学では、フレームワーク言語と基本理論（コア公理システム）から始めます。これらの基本理論は、興味のある定理のほとんどを証明するには弱すぎますが、これらの定理を述べるために必要な定義を展開するには十分強力です。たとえば、「すべての有界実数列には上限がある」という定理を研究するには、実数と実数列について話すことができる基本システムを使用する必要があります。

基本システムで述べることはできるが、基本システムでは証明できない各定理について、その定理を証明するために必要な特定の公理システム（基本システムよりも強い）を決定することが目標です。システムS が定理T を証明するために必要であることを示すには、2つの証明が必要です。最初の証明は、 TがSから証明可能であることを示します。これは、システムSで実行できることの正当化を伴う通常の数学的証明です。反転と呼ばれる2番目の証明は、 T自体がS を意味することを示します。この証明は基本システムで実行されます。^[1]反転により、基本システムを拡張する公理システムS′は、 Tを証明しながら Sよりも弱くなることはできないことが確立されます。

逆数学の研究のほとんどは、 2 階算術のサブシステムに焦点を当てています。逆数学の研究の全体は、2 階算術の弱いサブシステムでほぼすべての学部レベルの数学を形式化するのに十分であることを証明しました。2 階算術では、すべてのオブジェクトを自然数または自然数の集合として表すことができます。たとえば、実数に関する定理を証明するために、実数は有理数のコーシー列として表すことができ、各列は自然数の集合として表すことができます。

逆数学で最も頻繁に考慮される公理系は、理解スキームと呼ばれる公理スキームを使用して定義されます。このようなスキームは、与えられた複雑さの式によって定義可能な自然数の集合が存在することを述べています。この文脈では、式の複雑さは算術階層と解析階層を使用して測定されます。

逆数学が集合論を基本システムとして使用して実行されない理由は、集合論の言語が表現力が豊かすぎるためです。自然数の極めて複雑な集合は、集合論の言語 (任意の集合を定量化できる) の簡単な式で定義できます。2 階算術のコンテキストでは、ポストの定理などの結果により、式の複雑さと、それが定義する集合の (非) 計算可能性との間に密接な関係が確立されます。

2 階算術を使用するもう 1 つの効果は、一般的な数学の定理を算術内で表現できる形式に制限する必要があることです。たとえば、2 階算術では、「すべての可算ベクトル空間には基底がある」という原理を表現できますが、「すべてのベクトル空間には基底がある」という原理は表現できません。実際的には、代数と組合せ論の定理は可算構造に制限され、解析と位相の定理は可分空間に制限されることを意味します。一般的な形式で選択公理を意味する多くの原理(「すべてのベクトル空間には基底がある」など) は、制限されると 2 階算術の弱いサブシステムで証明可能になります。たとえば、「すべての体には代数的閉包がある」は ZF 集合論では証明できませんが、制限された形式「すべての可算体には代数的閉包がある」は、逆数学で一般的に使用される最も弱いシステムである RCA ₀で証明できます。

2005年にウルリッヒ・コーレンバッハが始めた高階逆数学研究の最近の流れは、高階算術のサブシステムに焦点を当てています。^[4] 高階算術のより豊富な言語により、2階算術で一般的な表現（別名「コード」）の使用が大幅に削減されます。たとえば、カントール空間上の連続関数は、バイナリシーケンスをバイナリシーケンスにマッピングする関数であり、通常の連続性の「イプシロンデルタ」定義も満たします。

高階逆数学には、（2階）理解スキームの高階バージョンが含まれます。このような高階公理は、与えられた複雑さの式の真偽を決定する関数の存在を述べています。この文脈では、式の複雑さは算術階層と解析階層を使用して測定されます。2階算術の主要なサブシステムの高階対応物は、通常、元の2階システムと同じ2階文（または大きなサブセット）を証明します。^[5] たとえば、RCAと呼ばれる高階逆数学の基本理論は、^ω0
_​は、言語まで、 RCA ₀と同じ文を証明します。

前の段落で述べたように、2階の内包公理は高階の枠組みに簡単に一般化できます。しかし、基本空間のコンパクト性を表現する定理は、2階算術と高階算術ではまったく異なる動作をします。一方では、可算被覆/2階算術の言語に制限されている場合、単位区間のコンパクト性は次のセクションからWKL ₀で証明できます。一方、非可算被覆/高階算術の言語が与えられた場合、単位区間のコンパクト性は（完全な）2階算術からのみ証明できます。^{[6]他の被覆補題（たとえば、} Lindelöf、Vitali、Besicovitchなどによるもの）も同じ動作を示し、ゲージ積分の多くの基本的性質は、基礎となる空間のコンパクト性と同等です。

二階算術は、自然数と自然数の集合に関する形式的な理論です。可算 環、群、体、実効ポーランド空間内の点など、多くの数学的対象は自然数の集合として表現でき、この表現を法として二階算術で研究することができます。

逆数学は、2 階算術のいくつかのサブシステムを利用する。典型的な逆数学の定理は、特定の数学定理Tが、より弱いサブシステムB上の 2 階算術の特定のサブシステムSと同等であることを示す。この弱いシステムB は、結果の基本システムとして知られている。逆数学の結果が意味を持つためには、このシステム自体が数学定理Tを証明できない必要がある。^{[引用が必要]}

シンプソン（2009）は、逆算術で頻繁に出現する2階算術の5つの特定のサブシステム（ビッグファイブと呼ぶ）について述べている。これらのシステムは、強さが増す順に、RCA ₀、WKL ₀、ACA ₀、ATR ₀、Πという頭文字で名付けられている。¹
₁-CA ₀。

次の表は「ビッグファイブ」システム^[7]を要約し、高階算術における対応するシステムをリストしたものです。^[5] 後者は、通常、元の2階システムと同じ2階文（または大きなサブセット）を証明します。^[5]

これらの名前の添え字_{0 は}、帰納法のスキームが完全な 2 階帰納法のスキームから制限されていることを意味します。^[8]たとえば、ACA ₀には、帰納法公理(0 ∈ X ∀ n ( n ∈ X → n + 1 ∈ X )) → ∀ n n ∈ X${\displaystyle \wedge }$ が含まれます。これは、2 階算術の完全な内包公理と合わせて、任意の 2 階式 φ に対して、( φ (0) ∀ n ( φ ( n ) → φ ( n +1))) → ∀ n φ ( n )${\displaystyle \wedge }$ の普遍閉包によって与えられる完全な2 階帰納法のスキームを意味します。ただし、ACA ₀には完全な内包公理がなく、添え字₀は、完全な 2 階帰納法のスキームもないことを思い出させます。この制限は重要です。制限された帰納法を持つシステムは、完全な 2 次帰納法スキームを持つシステムよりも 証明理論的順序が大幅に低くなります。

RCA _0は、ロビンソン算術の公理、Σの帰納法を公理とする2階算術の一部である。⁰
₁式、およびΔの理解⁰
₁数式。

サブシステム RCA ₀は、逆数学の基本システムとして最も一般的に使用されているものです。頭文字「RCA」は「再帰的理解公理」の略で、「再帰的」は「計算可能」を意味し、再帰関数で使用されます。この名前が使用されるのは、RCA _{0 が非公式に「計算可能な数学」に対応するためです。特に、RCA 0}に存在することが証明できる自然数の集合は計算可能であり、したがって、計算不可能な集合が存在することを示唆する定理は RCA ₀では証明できません。この限りでは、RCA ₀は構成的システムですが、排中律を含む古典論理の理論であるため、構成主義のプログラムの要件を満たしていません。

_{RCA 0}は一見弱点があるように見えますが (計算不可能な集合が存在することを証明できない)、いくつかの古典的な定理を証明するには十分であり、そのため、論理的な強度は最小限で済みます。これらの定理は、ある意味では、基本システムですでに証明可能であるため、逆数学の取り組みの範囲外です。RCA ₀で証明可能な古典的な定理には次のものがあります。

• 自然数、整数、有理数の基本的な性質（たとえば、有理数は順序付き体を形成する）。
• 実数の基本的な性質（実数はアルキメデスの順序体である。長さがゼロに近づく閉区間の入れ子になった列はどれも交差点に1つの点を持つ。実数は可算ではない）。^{[1]セクション II.4}
• 完全な分離可能な距離空間に対するベールのカテゴリ定理（分離可能性条件は、定理を2階算術の言語で述べる場合にも必要である）。^{[1]定理 II.5.8}
• 連続実関数の中間値定理。^{[1]定理 II.6.6}
• 可分バナッハ空間上の連続線型作用素の列に対するバナッハ＝シュタインハウスの定理。[ 1 ^{]定理 II.10.8}
• ゲーデルの完全性定理の弱いバージョン(可算言語で、結果に関してすでに閉じている文の集合の場合)。
• 可算体の代数的閉包の存在（ただしその一意性は不明）。 ^{[1] II.9.4--II.9.8}
• 可算順序体の実閉包の存在と一意性。 ^{[1] II.9.5, II.9.7}

_{RCA 0}の1階部分（集合変数を含まないシステムの定理）は、Σに限定された帰納法による1階ペアノ算術の定理の集合である。⁰
_{1式。RCA 0}と同様に、完全な一階ペアノ算術では 一貫していることが証明されています。

サブシステム WKL ₀は、RCA _0とケーニッヒの補題の弱い形式、つまり完全な二分木（0 と 1 の有限シーケンスすべての木）のすべての無限部分木には無限パスがあるという命題から構成されます。この命題は弱いケーニッヒの補題として知られており、2 階算術の言語で簡単に述べることができます。WKL _{0 は}、Σ の原理として定義することもできます。⁰
₁分離（2つのΣが与えられた場合）⁰
₁排他的な自由変数nの式がある場合、一方を満たすすべてのn を含み、他方を満たすn を含まない集合が存在する)。この公理を RCA _{0に追加すると、結果として得られるサブシステムは WKL 0}と呼ばれます。特定の公理と、基本公理と帰納法を含むサブシステムとの間の同様の区別は、以下で説明するより強いサブシステムに対しても行われます。

ある意味では、弱いケーニッヒの補題は選択公理の一種である（ただし、前述のように、選択公理なしで古典的なツェルメロ-フランケル集合論で証明できる）。「構成的」という言葉のいくつかの意味では、構成的に有効ではない。

_{WKL 0が実際に RCA 0}よりも強い (RCA 0 では証明できない)ことを示すには、計算不可能な集合が存在することを意味する WKL ₀の定理を示すだけで十分です。これは難しくありません。WKL _{0 は}、実質的に分離不可能な再帰的に列挙可能な集合に対して分離集合が存在することを意味します。

_{RCA 0}と WKL ₀は同じ一階部分を持ち、同じ一階文を証明していることがわかります。ただし、WKL _{0 は、RCA 0}から導かれない古典的な数学的結果を多数証明できます。これらの結果は一階文として表現できませんが、二階文として表現できます。

以下の結果は弱ケーニッヒの補題と同等であり、したがってRCA _{0上のWKL 0}と同等である。

• 実数単位閉区間に対するハイン・ボレルの定理。意味は次の通り。開区間の列によるすべての被覆には有限の部分被覆がある。
• 完全な全有界可分距離空間に対するハイン・ボレルの定理（被覆は開球の列によって行われる）。
• 閉じた単位区間上（または上記のように任意のコンパクトで可分な距離空間上）の連続実関数は有界です（または、有界であり、その境界に達します）。
• 閉じた単位区間上の連続実関数は、多項式（有理係数）によって均一に近似できます。
• 閉じた単位区間上の連続実関数は一様連続です。
• 閉じた単位区間上の連続実関数はリーマン積分可能である。
• ブラウワー不動点定理（-単体上の連続関数に対して）。^{[1]定理IV.7.7}${\displaystyle n}$
• 可分ハーン・バナッハの定理は次の形式で表される: 可分バナッハ空間の部分空間上の有界線型形式は、空間全体の有界線型形式に拡張される。
• ジョルダン曲線定理
• ゲーデルの完全性定理（可算言語の場合）。
• 長さ ω の {0,1} 上の開ゲーム (または閉開ゲーム) の決定性。
• すべての可算可換環には素イデアルが存在します。
• すべての可算な形式実体は順序付け可能です。
• 代数的閉包の一意性（可算体の場合）。

ACA ₀は、RCA ₀に算術式の理解スキームを加えたものです (これは「算術理解公理」と呼ばれることもあります)。つまり、ACA ₀を使用すると、任意の算術式 (変数の束縛はないが、パラメータは含まれている可能性がある) を満たす自然数の集合を形成できます。^{[1] pp. 6--7実際には、完全な算術理解を得るには、RCA} ₀にΣ ₁式の理解スキーム(2 次自由変数も含む) を追加するだけで十分です。^{[1]補題 III.1.3}

_{ACA 0}の 1 階部分はまさに 1 階ペアノ算術です。ACA ₀は1 階ペアノ算術の保守的な拡張です。2 つのシステムは (弱いシステムでは) 証明可能で等価です。ACA _{0 は}述語的数学のフレームワークと考えることができますが、ACA ₀では証明できない述語的に証明可能な定理もあります。自然数に関する基本的な結果のほとんど、および他の多くの数学定理は、このシステムで証明できます。

_{ACA 0が WKL 0}より強いことを確認する 1 つの方法は、すべての算術セットを含まない WKL ₀モデルを示すことです。実際、低セットは低セットに比べて低いため、 低基底定理を使用して、完全に低セットで構成される WKL ₀モデルを構築できます。

次のアサーションは、ACA ₀ と RCA ₀の同等性を持ちます。

• 実数の連続完全性（実数の有界増加列はすべて極限を持つ）。^{[1]定理 III.2.2}
• ボルツァーノ・ワイエルシュトラスの定理。^{[1]定理III.2.2}
• アスコリの定理: 単位区間上の実関数のすべての有界等連続列には、一様収束する部分列が存在する。
• あらゆる可算体はその代数閉包に同型に埋め込まれる。^{[1]定理 III.3.2}
• あらゆる可算可換環には極大イデアルが存在する。^{[1]定理 III.5.5}
• 有理数体上の（または任意の可算体上の）すべての可算ベクトル空間には基底がある。^{[1]定理 III.4.3}
• 任意の可算体に対して、を超える超越基底が存在する。^{[1]定理 III.4.6}${\displaystyle K\subseteq L}$${\displaystyle L}$${\displaystyle K}$
• ケーニッヒの補題（任意の有限分岐木に対するもので、上で説明した弱いバージョンとは対照的である）。^{[1]定理 III.7.2}
• 任意の可算群と の任意の部分群に対して、 によって生成される部分群が存在する。^{[9] p.40}${\displaystyle G}$${\displaystyle H,I}$${\displaystyle G}$${\displaystyle H\cup I}$
• 任意の部分関数は全関数に拡張することができる。^[10]
• ラムゼーの定理の特定の形式など、組合せ論における様々な定理。^{[11] [1]定理III.7.2}

_{ATR 0}システムは、ACA ₀に、任意の算術関数（自由数変数nと自由集合変数Xを持つ任意の算術式を意味し、式を満たすnの集合にX を渡す演算子として見なされる）は、任意の集合から始まる任意の可算な整列順序に沿って超限反復できるという公理を追加します。ATR _{0は、ACA 0}上でΣ の原理と同等です。¹
₁分離。ATR _{0 は}非述語的であり、述語的システムの順序数の上限で ある証明理論的順序数を持ちます。 ${\displaystyle \Gamma _{0}}$

ATR _{0 はACA 0}の一貫性を証明しており、したがってゲーデルの定理によれば厳密にはより強力です。

次のアサーションは、ATR ₀対 RCA ₀と同等です。

• 任意の2つの可算な整列順序は比較可能である。つまり、それらは同型であるか、一方が他方の適切な初期セグメントに同型である。^{[1]定理 V.6.8}
• 可算な簡約アーベル群に対するウルムの定理。
• 完全集合定理は、完全な可分距離空間のすべての非可算閉部分集合には完全閉集合が含まれることを述べています。
• ルシンの分離定理（基本的にはΣ¹
  ₁分離）。^{[1]定理V.5.1}
• ベール空間における開集合の決定性。

Π¹
₁-CA _{0 は}算術超限再帰よりも強力で、完全に非述語的である。これは RCA ₀と Π の理解スキームから構成される。¹
₁数式。

ある意味では、Π¹
₁-CA _{0 の}理解は算術超限再帰（Σ¹
₁ACA ₀が弱いケーニッヒの補題 (Σ⁰
₁これは、記述的集合論のいくつかのステートメントと同等であり、その証明には強く非述語的な議論が利用されています。この同値性は、これらの非述語的な議論は削除できないことを示しています。

以下の定理はΠと同値である。¹
₁-CA ₀ から RCA ₀へ:

• カントール・ベンディクソンの定理（すべての実数閉集合は完全集合と可算集合の和集合である）。^{[1]演習VI.1.7}
• シルバーの二分法（すべての共解析的同値関係は、可算な数の同値類か、比較不可能な完全な集合のいずれかを持つ）^{[1]定理 VI.3.6}
• 全ての可算アーベル群は可分群と被約群の直和である。^{[1]定理VI.4.1}
• ゲームの決定性。^{[1]定理VI.5.4}${\displaystyle \Sigma _{1}^{0}\land \Pi _{1}^{0}}$

• 再帰的理解よりも弱いシステムを定義することができます。弱いシステムRCA^*
  ₀基本的な関数の算術EFA（基本公理とΔ⁰
  ₀指数関数的操作を伴う強化言語における帰納法）プラスΔ⁰
  ₁理解。RCA以上^*
  ₀、先に定義した再帰的内包（つまり、Σ⁰
  ₁帰納法は、多項式（可算体上）が有限個の根しか持たないという主張と、有限生成アーベル群の分類定理と同値である。RCA^*
  ₀はEFAと同じ証明論的順序数ω3^を持ち、Πに対してEFA上で保存的である。⁰
  ₂文章。
• 弱弱ケーニッヒの補題は、無限パスを持たない無限二分木のサブツリーには、長さnの葉の割合が漸近的にゼロになる（長さnの葉がいくつ存在するかについては一様な推定値がある）という主張である。同等の定式化は、正の測度を持つカントール空間の任意のサブセットが空でないということである（これは RCA ₀では証明できない）。WWKL _{0は、この公理を RCA 0}に付加することによって得られる。これは、単位実数区間が区間のシーケンスでカバーされる場合、それらの長さの合計が少なくとも 1 であるという主張と同等である。WWKL _{0のモデル理論は、}アルゴリズム的ランダムシーケンスの理論と密接に関連している。特に、RCA ₀の ω モデルが弱弱ケーニッヒの補題を満たすのは、すべての集合Xに対して、 Xに対して 1 ランダムな集合Yが存在する場合のみである。
• DNR (「対角非再帰」の略) は、すべての集合に対して対角非再帰関数が存在することを主張する公理をRCA _{0に追加します。つまり、DNR は、任意の集合}Aに対して、すべてのeに対して、オラクルAを持つe番目の部分再帰関数がfと等しくないような全関数f が存在することを述べています。DNR は、WWKL よりも厳密に弱いです (Lempp他、2004)。
• Δ¹
  ₁-内包は、ある意味では算術的超限再帰と類似しており、これは再帰的内包が弱いケーニッヒの補題に類似しているのと同様である。これは超算術的集合を最小のω-モデルとして持つ。算術的超限再帰はΔを証明する。¹
  ₁-理解はできますが、その逆はできません。
• Σ¹
  ₁-choiceは、 η ( n , X )がΣであるとき、¹
  ₁各nに対して η を満たすX が存在するような式であれば、各nに対してη ( n , X _n ) が成り立つような集合の列X _nが存在する。Σ¹
  ₁-選択は、超算術集合を最小ωモデルとして持つ。算術超限再帰はΣを証明する。¹
  ₁-選択はできますが、その逆はできません。
• HBU (「無数ハイネ・ボレル」の略) は、無数被覆を含む単位区間の(開被覆)コンパクト性を表現する。HBU の後者の側面により、HBU は3 階算術の言語でのみ表現可能となる。 カズンの定理(1895) は HBU を意味し、これらの定理はカズンとリンデレフによる同じ被覆の概念を使用する。HBU は証明が難しい。通常の内包公理の階層構造では、HBU の証明には完全な 2 階算術が必要である。^[6]
• 無限グラフに対するラムゼーの定理は5大サブシステムのいずれにも当てはまらず、証明の強さが異なる他の弱い変種も数多く存在する。^[11]

RCA ₀、Π以上¹
₁超限再帰、∆⁰
₂決定性、そして∆¹
₁ラムゼーの定理はすべて互いに同等です。

RCA _{0 を}超えると、Σ¹
₁単調帰納法、Σ⁰
₂決定性、およびΣ¹
₁ラムゼーの定理はすべて互いに同等です。

以下は同等である: ^{[12] [13]}

• （スキーマ）Π¹
  ₃Πの結果¹
  ₂-CA ₀
• RCA ₀ + (有限n上のスキーマ) Σの差分階層のn番目のレベルにおける決定性⁰
  ₂セット
• RCA ₀ + {τ: τは真のS2S文である}

Πの集合¹
₃2階算術Z _{2の結果は、} Σの差分階層のn番目のレベルにおけるRCA ₀ +（有限n上のスキーマ）決定性と同じ理論を持っています⁰
₃セット^[14]

半順序集合 に対して、 は、その開集合が何らかの に対して の形の集合であるようなフィルタからなる位相空間を表すものとする。次の命題は に対して と同等である。任意の可算半順序集合 に対して、位相空間 が完全に距離化可能であるのは、それが正則 である場合に限る。^[15]${\displaystyle P}$${\displaystyle {\textrm {MF}}(P)}$${\displaystyle P}$${\displaystyle \{F\in {\textrm {MF}}(P)\mid p\in F\}}$${\displaystyle p\in P}$${\displaystyle \Pi _{2}^{1}{\mathsf {-CA}}_{0}}$${\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}_{0}}$${\displaystyle P}$${\displaystyle {\textrm {MF}}(P)}$

ω-モデルの ω は、非負の整数（または有限順序数）の集合を表します。ω-モデルは、1 次部分がペアノ算術の標準モデルであるが^[1] 2 次部分が非標準である可能性がある 2 次算術の一部のモデルです。より正確には、ω-モデルはのサブセットの選択によって与えられます。1 次変数は通常どおり の要素として解釈され、は通常の意味を持ちますが、2 次変数は の要素として解釈されます。 が整数のすべてのサブセットで構成されると単純に考える標準的な ω-モデルがあります。ただし、他の ω-モデルもあります。たとえば、RCA ₀にはが の再帰サブセットで構成される最小の ω-モデルがあります。 ${\displaystyle S\subseteq {\mathcal {P}}(\omega )}$${\displaystyle \omega }$${\displaystyle \omega }$${\displaystyle +}$${\displaystyle \times }$${\displaystyle S}$${\displaystyle S}$${\displaystyle S}$${\displaystyle \omega }$

β モデルは、および文 (パラメータ付き)の真実性に関して標準 ω モデルと一致する ω モデルです。 ${\displaystyle \Pi _{1}^{1}}$${\displaystyle \Sigma _{1}^{1}}$

非ωモデルも、特に保存定理の証明に役立ちます。

• 閉形式表現 § 数値形式からの変換
• 帰納法、境界法、最小数原理
• 順序分析

• アンボス・スピース、Ｋ．ショース・ハンセン、B​​.レンプ、S. Slaman、TA (2004)、「Comparing DNR and WWKL」、Journal of Symbolic Logic、69 (4): 1089、arXiv : 1408.2281、doi :10.2178/jsl/1102022212、S2CID  17582399。
• フリードマン、ハーヴェイ (1975)、「2 次算術のいくつかのシステムとその使用法」、国際数学者会議の議事録 (バンクーバー、ブリティッシュ コロンビア州、1974 年)、第 1 巻、カナダ数学会議、モントリオール、ケベック州、pp. 235–242、MR  0429508
• フリードマン、ハーヴェイ (1976)、ボールドウィン、ジョン、マーティン、DA、ソアレ、RI、テイト、WW (編)、「制限付き帰納法による 2 次算術システム、I、II」、記号論理学会会議、記号論理ジャーナル、41 (2): 557–559、doi :10.2307/2272259、JSTOR  2272259
• ヒルシュフェルト、デニス・R.（2014）、真実を切り開く、シンガポール国立大学数学研究所講義ノートシリーズ、第28巻、World Scientific
• ハンター、ジェームズ (2008)、逆トポロジー(PDF) (博士論文)、ウィスコンシン大学マディソン校
• Kohlenbach, Ulrich (2005)、「高次逆数学」、Simpson, Stephen G (編)、高次逆数学、逆数学 2001 (PDF)、論理学講義ノート、ケンブリッジ大学出版局、pp. 281–295、CiteSeerX  10.1.1.643.551、doi :10.1017/9781316755846.018、ISBN 9781316755846
• ノーマン、ダグ、サンダース、サム（2018）「不可算数の数学的および基礎的意義について」、Journal of Mathematical Logic、19：1950001、arXiv：1711.08939、doi：10.1142/S0219061319500016、S2CID  119120366
• シンプソン、スティーブン G. (2009)、「第 2 階算術のサブシステム」、Perspectives in Logic (第 2 版)、ケンブリッジ大学出版局、doi :10.1017/CBO9780511581007、ISBN 978-0-521-88439-6、MR  2517689
• スティルウェル、ジョン（2018）、逆数学、内側からの証明、プリンストン大学出版、ISBN 978-0-691-17717-5

• ソロモン、リード (1999)、「順序群: 逆数学のケーススタディ」、The Bulletin of Symbolic Logic、5 (1): 45–58、CiteSeerX  10.1.1.364.9553、doi :10.2307/421140、ISSN  1079-8986、JSTOR  421140、MR  1681895、S2CID  508431

• スティーブン・G・シンプソンのホームページ
• 逆算数学動物園