逆数学
ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} において全ての β {\displaystyle \beta \,} -モデルが ATR 0 {\displaystyle {\mbox{ATR}}_{0}\,} のモデルであることが示せる。また、 ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} において、「任意の集合 X {\displaystyle X\,} について X {\displaystyle X\,} を含む β {\displaystyle \beta \,} モデルが存在する」は Π 1 1 -CA 0 {\displaystyle \Pi _{1}^{1}{\mbox{-CA}}_{0}\,} と同値である。
一般に、 ω {\displaystyle \omega \,} -モデルであって、 Σ n 1 {\displaystyle \Sigma _{n}^{1}\,} 文について、標準モデルと真偽が一致するものは β n {\displaystyle \beta _{n}\,} -モデルと呼ばれる。
また、Non- ω {\displaystyle \omega \,} -モデル(1階部分が標準ではないモデル)も、ある公理系が保存的拡大であることの証明にしばしば登場する。
2階算術の部分体系 RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} 、 WKL 0 {\displaystyle {\mbox{WKL}}_{0}\,} 、 ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} 、 ATR 0 {\displaystyle {\mbox{ATR}}_{0}\,} 、 Π 1 1 -CA 0 {\displaystyle \Pi _{1}^{1}{\mbox{-CA}}_{0}\,} は, Big Fiveと呼ばれ、 逆数学において頻繁に扱われるものである。
次は"big five"の特徴である。Simpson (2009, p.42)参照。
なお, Big Fiveの名前についている 0 {\displaystyle {}_{0}\,} は帰納法の図式が制限されていることを意味する。例えば、 ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} は算術的論理式についての帰納法しか持たない。帰納法を制限した体系は、一般の2階算術の論理式についての帰納法をもつ体系に比べ、大幅に小さい証明論的順序数を持つ。
しかし、 WKL 0 {\displaystyle {\mbox{WKL}}_{0}\,} で証明可能で、 RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} では証明不可能な古典的数学の定理もある。これらの結果は2階部分の証明能力の違いを示している。
RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} 上で、 WKL 0 {\displaystyle {\mbox{WKL}}_{0}\,} と以下の定理が同値であることが示せる。
実数からなる単位閉区間に対する(開区間による任意の被覆が有限部分被覆を持つという意味での)ハイネ=ボレルの定理。
完備全有界可分距離空間に対する(開球体列による被覆についての)ハイネ=ボレルの定理。
単位閉区間(もしくは任意のコンパクト可分距離空間)上の連続実函数が有界であること(もしくは有界かつその境界値を実現する点が存在すること)。
単位閉区間上の連続実函数が有理係数多項式で一様に近似できること。
単位閉区間上の連続実函数が一様連続であること。
単位閉区間上の連続実函数がリーマン積分可能であること。
単位閉区間の有限個のコピーの直積上の連続函数に対するブラウワーの不動点定理。
可分バナッハ空間の部分空間上の有界線型形式が全体空間上の有界線型形式に拡張できるという形での可分ハーン=バナッハの定理。
ジョルダンの閉曲線定理
可算言語に対するゲーデルの完全性定理。
任意の可算可換環が素イデアルを持つこと。
任意の可算形式的実体を順序体にできること。
可算体に対する代数閉包の一意性。