逆数学
ATR 0 {\displaystyle {\mbox{ATR}}_{0}\,} は、 ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} に算術的超限再帰を追加した体系である。
ATR 0 {\displaystyle {\mbox{ATR}}_{0}\,} は ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} 上で、Σ1分離原理と同値である。
ATR 0 {\displaystyle {\mbox{ATR}}_{0}\,} は、 ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} の無矛盾性を証明可能なのでゲーデルの不完全性定理より、 ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} より強い。
RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} で次が ATR 0 {\displaystyle {\mbox{ATR}}_{0}\,} と同値。
任意の二つの可算整列順序は比較可能(一方が他方または他方の始片に同型)である。
可算被約アーベル群に対するウルムの定理。
完備可分距離空間の任意の非可算閉部分集合が完全閉集合を含むことを述べた完全集合定理。
ルージンの分離定理(essentially Σ 1 1 {\displaystyle \Sigma _{1}^{1}\,} 分離)。
ベール空間における開集合の決定性。
算術的集合を含まない WKL 0 {\displaystyle {\mbox{WKL}}_{0}\,} のモデルが存在するので、 ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} は WKL 0 {\displaystyle {\mbox{WKL}}_{0}\,} よりも強いことが示される。実際、低基底定理を使った低集合を含むような WKL 0 {\displaystyle {\mbox{WKL}}_{0}\,} のモデルは構成不可能。
RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} 上で次と ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} は同値。
実数全体の集合の点列コンパクト性(有界で単調増加な任意の実数列は極限を持つ)。
ボルツァーノ=ワイエルシュトラスの定理。
アスコリの定理: 単位閉区間上の任意の有界で同程度連続な実関数列は一様収束する部分列を持つ。
任意の可算可換環は極大イデアルを持つ。
有理数体(もしくは任意の可算体)上の任意の可算ベクトル空間は基底を持つ。
任意の可算体は超越基底を持つ。
(任意の有限分岐木に対する、弱でない)ケーニヒの補題。
ラムゼーの定理の一形態などを例とする組合せ論の諸定理。
逆数学は、フレームとなる言語と基本的な公理からはじめる。例えば、“すべての実数の有界な列は上限をもつ”という定理の研究には、実数と実数の列を定義する公理が必要となる。
基本体系において証明できない定理からはじめて、定理を証明するのに必要な(基本体系よりも強い)公理を決定することを目標とする。定理 T {\displaystyle T\,} とそれを証明可能な場合の体系 S {\displaystyle S\,} との関係を示す2つの証明がある。1つ目は、 S {\displaystyle S\,} から T {\displaystyle T\,} が証明可能であることの証明である。このとき普通の数学の定理は体系 S {\displaystyle S\,} で成り立つ。2つ目は*逆方向*、 すなわち T {\displaystyle T\,} が S {\displaystyle S\,} と同値であることであることの基本体系における証明である。 逆方向の証明ができれば、 S {\displaystyle S\,} より弱い体系 S ′ {\displaystyle S^{\prime }\,} であって T {\displaystyle T\,} を証明できるようなものは存在しないことが分かる。
Π 1 1 -CA 0 {\displaystyle \Pi _{1}^{1}{\text{-CA}}_{0}\,} は、 RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} に Π 1 1 {\displaystyle \Pi _{1}^{1}\,} 論理式に関する内包公理を追加した体系である。 Π 1 1 -CA 0 {\displaystyle \Pi _{1}^{1}{\text{-CA}}_{0}\,} は非可述的な体系である。
Π 1 1 -CA 0 {\displaystyle \Pi _{1}^{1}{\text{-CA}}_{0}\,} と ATR 0 {\displaystyle {\text{ATR}}_{0}\,} の関係は、 ACA 0 {\displaystyle {\text{ACA}}_{0}\,} と WKL 0 {\displaystyle {\text{WKL}}_{0}\,} の関係に似ている。
一方、集合変数は S {\displaystyle S\,} の元として解釈される。 S = P ( ω ) {\displaystyle S={\mathcal {P}}(\omega )\,} とする ω {\displaystyle \omega \,} -モデルを2階算術の標準モデルと呼ぶ。しかし、標準モデル以外にも ω {\displaystyle \omega \,} -モデルは存在する。たとえば、 RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} は S {\displaystyle S\,} として計算可能な ω {\displaystyle \omega \,} の部分集合全体をとった ω {\displaystyle \omega \,} -モデルをもつ。
ω {\displaystyle \omega \,} -モデルであって、 Σ 1 1 {\displaystyle \Sigma _{1}^{1}\,} 文について、標準モデルと真偽が一致するものを β {\displaystyle \beta \,} -モデルと呼ぶ。