逆算

逆算術研究のほとんどは、2階算術のサブシステムに焦点を当てています。逆算術の研究により、2階算術の弱いサブシステムで、学部レベルの数学のほぼすべてを形式化できることが確立されています。2階算術では、すべてのオブジェクトは自然数または自然数の集合として表現できます。たとえば、実数に関する定理を証明するために、実数は有理数のコーシー列として表現でき、その各列は自然数の集合として表現できます。^{[ 7 ]}

逆算において最もよく考慮される公理系は、内包スキームと呼ばれる公理スキームを用いて定義される。このようなスキームは、与えられた複雑さの式で定義可能な自然数の任意の集合が存在することを述べる。この文脈では、式の複雑さは算術階層と解析階層を用いて測定される。^{[ 8 ]}

逆算が集合論を基本システムとして使用しない理由は、集合論の言語が表現力に富みすぎるためである。^{[ 9 ]} 極めて複雑な自然数の集合は、集合論の言語（任意の集合を量化できる）の単純な式で定義できる。2階算術の文脈では、ポストの定理などの結果により、式の複雑さと、それが定義する集合の（非）計算可能性との間に密接な関係が確立される。

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

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

高階逆算術には、（2階）内包表記スキームの高階バージョンが含まれます。このような高階公理は、与えられた複雑さの式の真偽を決定する関数の存在を述べています。この文脈では、式の複雑さは算術階層と解析階層を使用して測定されます。2階算術の主要なサブシステムの高階対応物は、一般的に元の2階システムと同じ2階文（または大きな部分集合）を証明します。^{[ 13 ]例えば、RCA ω} ₀ と呼ばれる高階逆算術の基本理論は、言語を除いてRCA ₀と同じ文を証明します。

前の段落で述べたように、2 階の内包公理は高階の枠組みに容易に一般化できます。しかし、基本空間のコンパクト性を表す定理は、2 階と高階の算術でかなり異なる振る舞いをします。一方では、可算カバー/2 階算術の言語に限定すると、単位区間のコンパクト性は次のセクションから WKL ₀で証明できます。他方では、非可算カバー/高階算術の言語が与えられると、単位区間のコンパクト性は (完全な) 2 階算術からのみ証明できます。^{[ 14 ]}他の被覆補題 (例えば、 Lindelöf、Vitali、Besicovitchなどによるもの) も同様の振る舞いを示し、ゲージ積分の多くの基本特性は、基礎となる空間のコンパクト性と同等です。

RCA _0は、ロビンソン算術の公理、Σ ⁰ ₁式の帰納的公理体系、およびΔ ⁰ ₁式の内包表記（再帰的内包表記とも呼ばれる）の公理を持つ、2 階算術の断片である。^{[ 19 ]}

の${\displaystyle \Sigma _{1}^{0}}$-帰納法の公理スキームの状態$${\displaystyle \quad {\big [}\varphi (0)\land \forall x{\big (}\varphi (x)\to \varphi (x+1){\big )}{\big ]}\to \forall x\ \varphi (x)}$$すべての人々のために${\displaystyle \Sigma _{1}^{0}}$-数式${\displaystyle \varphi }$集合変数に対して量化を行わない式。より具体的には、これらは次の形式の式である。$${\displaystyle \exists x_{1}\exists x_{2}\cdots \exists x_{n}\phi }$$どこ${\displaystyle \phi }$は${\displaystyle \Delta _{0}^{0}}$-セット変数を含めることができる式。言い換えると、${\displaystyle \varphi }$これは、一階変数と二階変数の両方を含むことができる量化子なしの式から始めて、一階変数に有界量化子を追加し、最後に一階変数に存在量化子を追加することによって得られます。^{[ 20 ]}

の${\displaystyle \Delta _{1}^{0}}$-理解公理体系は次のように述べている。$${\displaystyle \forall n[\psi (n)\leftrightarrow \varphi (n)]\to \exists X\forall n[n\in X\leftrightarrow \varphi (n)]}$$すべての人々のために$\displaystyle \Pi _{1}^{0}}$-数式${\displaystyle \psi }$そしてすべて${\displaystyle \Sigma _{1}^{0}}$-数式${\displaystyle \varphi }$[ ^{19 ]​}

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

一見すると弱点（計算不可能な集合の存在を証明できないこと）があるにもかかわらず、RCA _0は多くの古典的な定理を証明するのに十分であり、したがって、最小限の論理的強度しか必要としない。これらの定理は、ある意味で、逆算的な数学的試みの範疇を下回るものであり、基本システムにおいて既に証明可能である。RCA ₀で証明可能な古典的な定理には、以下のものがある。

• 自然数、整数、有理数の基本的な性質（例えば、有理数は順序体を形成すること）。
• 実数の基本的な性質（実数はアルキメデス的順序体である。長さがゼロに近づく閉区間の入れ子列は、その交点に一点を持つ。実数は可算ではない）。^{[ 21 ]}
• 完全可分距離空間に対するベールのカテゴリー定理（可分性条件は、定理を2階算術の言葉で述べるためにも必要である）。^{[ 22 ]}
• 連続実関数の中間値の定理。^{[ 23 ]}
• 可分バナッハ空間上の連続線形作用素列に対するバナッハ・シュタインハウスの定理。 ^{[ 24 ]}
• ゲーデルの完全性定理の弱いバージョン（可算言語における、帰結に関して既に閉じている文の集合に関する定理）。
• 可算体に対する代数閉包の存在（ただし一意性ではない）。 ^{[ 25 ]}
• 可算順序体の実閉包の存在と一意性。 ^{[ 26 ]}

_{RCA 0}の一次部分(集合変数を含まないシステムの定理) は、Σ ⁰ ₁式に限定された帰納法による一次ペアノ算術の定理の集合です。 ^{[ 27 ]}完全な一次ペアノ算術では、 RCA ₀と同様に、証明可能な一貫性があります。

サブシステム WKL ₀は、RCA _0とケーニッヒの補題の弱形式、すなわち完全二分木 (0 と 1 のすべての有限シーケンスの木) のすべての無限部分木には無限パスがあるという命題から構成されます。この命題は弱ケーニッヒの補題として知られており、2 階算術の言葉で簡単に述べることができます。^{[ 28 ]}

1階算術では、WKL _{0 は}Σ ⁰ ₁分離の公理スキームを追加することでより簡単に定義できます。つまり、自由変数nの 2 つのΣ ⁰ ₁式が互いに排他的である場合、一方の式を満たすすべてのnを含み、他方の式を満たさないnを含まない集合が存在します。記号で表すと次のようになります。$${\displaystyle \forall n\neg [\varphi (n)\land \psi (n)]\to \exists X\forall n[(\varphi (n)\to n\in X)\land (\psi (n)\to n\not \in X)]}$$すべての人々のために${\displaystyle \Sigma _{1}^{0}}$-数式${\displaystyle \varphi ,\psi }$[ ^{28 ]​}

用語はやや紛らわしい。弱いケーニッヒの補題自体も公理系としてWKLと表記されるが、WKL _0はWKL公理系の変種ではなく、システムを表す。^{[ 28 ]}

_{(RCA 0}の一次部分) + (${\displaystyle \Delta _{0}^{0}}$-理解）+（${\displaystyle \Sigma _{1}^{0}}$-分離) 一緒には (${\displaystyle \Delta _{1}^{0}}$-内包表記)。^{[ 1 ]：補題IV.4.4}

ある意味では、弱いケーニッヒの補題は選択公理の一形態である（ただし、前述のように、選択公理を用いなくても古典的なツェルメロ・フレンケル集合論で証明できる）。「構成的」という言葉の意味によっては、構成的に妥当ではない。^{[ 29 ]}

_{WKL 0が実際には RCA 0}よりも強力である（証明不可能）ことを示すには、WKL ₀が計算上分離不可能な再帰的列挙可能集合の分離集合の存在を意味することに注目してください。特に、2 つのことを簡単に書き下すことができます。${\displaystyle \Sigma _{1}^{0}}$-数式${\displaystyle \varphi ,\psi }$このような2つの集合を定義するならば、WKL ₀は、ある集合が存在することを証明する。${\displaystyle X}$_{それらを分離する集合が存在するのに対し、RCA 0}の標準モデルには計算可能な集合しか含まれていないため、そのような分離集合は存在しない。^{[ 30 ]}

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

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

• 閉単位実数区間に関するハイネ・ボレル定理は、次の意味で成り立つ。開区間の列による任意の被覆は、有限部分被覆を持つ。
• 完全かつ完全に有界な分離可能距離空間（被覆が開球の列によって行われる場合）に対するハイネ・ボレル定理。
• 閉単位区間（または上記のように任意のコンパクト可分距離空間）上の連続実関数は有界である（または：有界であり、その境界に達する）。
• 閉区間上の連続な実関数は、（有理係数を持つ）多項式によって一様に近似することができる。
• 閉区間上の連続な実関数は一様連続である。
• 閉単位区間上の連続な実関数はリーマン積分可能である。
• ブロワーの不動点定理（ n単体上の連続関数について）。^{[ 31 ]}
• 可分バナッハ空間の部分空間上の有界線形形式という形式の可分ハーン・バナッハ定理は、空間全体上の有界線形形式に拡張される。
• ジョルダン曲線定理。
• ゲーデルの完全性定理（可算言語の場合）。
• 長さωの{0, 1}上のオープンゲーム（またはクローオープンゲーム）の決定性。
• すべての可算可換環は素イデアルを持つ。
• 可算な形式的実体はすべて順序付け可能である。
• 代数閉包の一意性（可算体の場合）。
• 可算グラフに関するデ・ブルイン・エルデシュの定理：有限部分グラフがk彩色可能な可算グラフはすべてk彩色可能である。^{[ 32 ]}

システムACA _0は、 RCA ₀に算術式の内包表記スキーム（算術内包公理とも呼ばれるが、これは公理スキームである）を追加する。つまり、ACA ₀では、任意の算術式（束縛集合変数を持たないが、集合パラメータを含む可能性のあるもの）を満たす自然数の集合を構成できる。^{[ 33 ]}算術式とは、集合変数がパラメータとして現れる可能性があるが、量化されていない式のことである。言い換えれば、それは和集合である。$\displaystyle \cup _{n=0}^{\infty }\Sigma _{n}^{0}}$。

記号で表すと：$${\displaystyle \exists X\forall n[n\in X\leftrightarrow \varphi (n)]}$$すべての算術式について${\displaystyle \varphi }$また、制限付き帰納法公理（公理体系ではない）も備えている。$${\displaystyle 0\in X\to \forall n[n\in X\to n+1\in X]\to \forall n(n\in X)}$$これは、${\displaystyle \Sigma _{1}^{0}}$_{-WKL 0}およびRCA ₀で使用される帰納法公理スキームだが、完全な帰納法公理スキームと比較すると依然として制限がある。$${\displaystyle \varphi (0)\to \forall n[\varphi (n)\to \varphi (n+1)]\to \forall n[\varphi (n)]}$$すべての数式について${\displaystyle \varphi }$2階算術において。具体的には、完全な帰納法の公理体系は必ずしも導出可能ではない。なぜなら、ACA ₀は、次のことを証明できない可能性があるからである。${\displaystyle \varphi }$理解できる。つまり、いくつかの公式がある。${\displaystyle \varphi }$、したがって${\displaystyle \exists X\forall n[n\in X\leftrightarrow \varphi (n)]}$ACA ₀では証明できません。

実際、RCA ₀に理解スキームを追加するだけで十分です。${\displaystyle \Sigma _{1}^{0}}$-式、なぜなら論理否定を取って理解を得ることができるから$\displaystyle \Pi _{1}^{0}}$-数式、そしてこれを繰り返して算術階層のすべてのレベルの理解を得る。^{[ 34 ]}

_{ACA 0}の一次部分は、まさに一次ペアノ算術です。言い換えれば、ACA ₀は一次ペアノ算術の保守的な拡張です。 ^{[ 35 ]} 2 つのシステムは、（弱いシステムでは）等無矛盾であることが証明できます。ACA _{0 は}述語的数学の枠組みと考えることができますが、ACA ₀では証明できない述語的に証明可能な定理も存在します。自然数に関する基本的な結果のほとんど、および他の多くの数学的定理は、このシステムで証明できます。

_{ACA 0 がWKL 0}よりも強いことを示す一つの方法は、すべての算術集合を含まないWKL ₀のモデルを示すことです。実際、低基底定理を用いると、低集合同士の相対的な関係が低くなるため、低集合のみで構成されるWKL _{0のモデルを構築することが可能になります。}

以下の主張は、ACA ₀が RCA ₀を上回ることと同等です。

• 実数の列的完全性（有界な増加実数列には必ず極限が存在する）。^{[ 36 ]}
• ボルツァーノ・ワイエルシュトラスの定理。^{[ 36 ]}
• アスコリの定理：単位区間上の有界な等連続な実関数列はすべて、一様収束する部分列を持つ。
• すべての可算体は、その代数的閉包に同型的に埋め込まれる。^{[ 37 ]}
• すべての可算可換環には極大イデアルが存在する。^{[ 38 ]}
• 有理数体（または任意の可算体）上の可算ベクトル空間はすべて基底を持つ。^{[ 39 ]}
• 任意の可算体K ⊆ Lに対して、 K上のLの超越基底が存在する。^{[ 40 ]}
• ケーニッヒの補題（上記で説明した弱いバージョンとは異なり、任意の有限分岐木の場合）。^{[ 41 ]}
• ^任意の可算群Gと、 Gの任意の部分群H、Iに対して、 H ∪ Iによって生成される部分群が存在する。^{[ 42 ] p.40} 
• 任意の部分関数は全体関数に拡張できる。^{[ 43 ]}
• ヒグマンの補題。^{[ 44 ]}
• 組み合わせ論における様々な定理、例えばラムゼーの定理の特定の形式など。^{[ 45 ] [ 41 ]}

システムATR ₀は、 ACA _{0に算術的超限再帰と呼ばれる公理体系を追加する。非公式には、任意の算術関数は、任意の集合から始まる任意の}可算整列に沿って超限的に反復できると述べている。

算術的超限再帰の公理体系は、算術式ごとに1つの公理を持つ。${\displaystyle \theta (n,Z,{\vec {x}},{\vec {X}})}$公理は次のように述べている。${\displaystyle (A,<_{A})}$が整列集合であるならば、${\displaystyle Y}$これは、によってインデックス付けされたセットです。${\displaystyle A}$整列帰納法によって得られた${\displaystyle A}$:

• セット全体は${\displaystyle Y=\{(n,a):a\in A,n\in Y_{a}\}}$各索引項目は次の形式です。${\displaystyle Y_{a}=\{n\in \mathbb {N}$ :(n,a)\in Y\}} 。各初期セグメントは次の形式です。${\displaystyle Y^{a}=\{(n,b):b\in A,b<_{A}a,n\in Y_{b}\}}$。
  • 特に、一番下の先頭部分は空です。${\displaystyle Y^{\min A}=\emptyset }$。
• 整然とした導入は${\displaystyle Y^{\min A}=\emptyset }$そして、帰納法によって進行する。$${\displaystyle Y_{a}=\{n\in \mathbb {N}$$ :\theta (n,Y^{a},{\vec {x}},{\vec {X}})\}}

ATR _{0 は}、ACA _0上でΣ ¹ ₁分離の原理と同等である。ATR ₀は非述語的であり、証明論的順序数Γ ₀を持ち、これは述語的システムの順序数の上限である。

ATR _{0は ACA 0}の無矛盾性を証明しており、したがってゲーデルの定理により厳密に強い。

以下の主張は、RCA _{0上での ATR 0}と同等です。

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

Π ¹ ₁ -CA ₀は算術的超限再帰よりも強力であり、完全に非述語的である。それは RCA ₀と帰納法の公理から構成される。$${\displaystyle 0\in X\to \forall n[n\in X\to n+1\in X]\to \forall n(n\in X)}$$^{さらに、Π 1} ₁式の内包表記スキーム。

A$\displaystyle \Pi _{1}^{1}}$-式は次の形式です${\displaystyle \forall X\theta }$、 どこ${\displaystyle \theta }$これは算術式です。$\displaystyle \Pi _{1}^{1}}$-理解とは、次のように述べる公理体系である。$${\displaystyle \exists X\forall n[n\in X\leftrightarrow \varphi (n)]}$$すべての人々のために$\displaystyle \Pi _{1}^{1}}$-数式${\displaystyle \varphi }$。

ある意味では、Π ¹ ₁ -CA ₀内包表記は、算術的超限再帰 ( Σ ¹ ₁分離) と、ACA ₀が弱いケーニッヒの補題 ( Σ ⁰ ₁分離) と等価である。これは、証明に強い非述語的議論を用いる記述集合論のいくつかの命題と等価であり、この等価性は、これらの非述語的議論を取り除くことができないことを示している。

以下の定理は、 RCA _{0上の Π} ¹ ₁ -CA ₀と同等である。

• カントール・ベンディクソン定理（実数の閉集合はすべて完全集合と可算集合の和集合である）。^{[ 48 ]}
• シルバーの二分法（すべての共解析的同値関係は、可算個の同値類を持つか、比較不可能なものの完全な集合を持つかのいずれかである）^{[ 49 ]}
• すべての可算アーベル群は、可除群と既約群の直和である。^{[ 50 ]}
• Σ ⁰ ₁の決定性${\displaystyle \wedge }$Π ⁰ ₁ゲーム。 ^{[ 51 ]}

_{RCA 0}に完全な 2 階帰納法公理体系を追加すると、無制限帰納法による再帰的内包算体系である RCA が得られます。同様に、WKL ₀に完全な 2 階帰納法公理体系を追加すると、WKL が得られます。

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

RCA ₀上では、Σ ¹ ₁単調誘導、Σ ⁰ ₂決定性、およびΣ ¹ ₁ラムゼーの定理はすべて互いに同等です。

以下は同等です: ^{[ 52 ] [ 53 ]}

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

2 階算術 Z _{2の Π} ¹ ₃の結果の集合は、Σ ⁰ ₃集合の差分階層のn番目のレベルにおける RCA ₀ + (有限n上のスキーマ) 決定性と同じ理論を持つ。 ^{[ 54 ]}

半順序集合Pに対して、MF( P )を、開集合が{ F ∈ MF( P ) | p ∈ F }の形の集合であるP上のフィルタからなる位相空間とする。次の記述は、${\displaystyle \Pi _{2}^{1}{\mathsf {-CA}}_{0}}$以上${\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}_{0}}$: 任意の可算半順序集合Pに対して、位相空間 MF( P ) は、それが正則である場合に限り、完全に距離化可能である。^{[ 55 ]}