逆数学
実際、 RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} の ω {\displaystyle \omega \,} -モデル M {\displaystyle M\,} に対し, M {\displaystyle M\,} が WWKL 0 {\displaystyle {\mbox{WWKL}}_{0}\,} のモデルであることと, M {\displaystyle M\,} に含まれる任意の集合 X {\displaystyle X\,} について、 X {\displaystyle X\,} に対し相対的に1-randomなある Y {\displaystyle Y\,} が存在して Y {\displaystyle Y\,} が M {\displaystyle M\,} に含まれることは同値である。
DNR("diagonally non-recursive"の略)は、 RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} に「任意の集合に対し対角的非再帰な関数が存在する」を追加した公理系である。 DNR {\displaystyle {\mbox{DNR}}\,} とはつまり「任意の集合 A {\displaystyle A\,} に対して、ある全域的関数 f {\displaystyle f\,} が存在して、fは A {\displaystyle A\,} から計算可能などんな部分関数とも等しくない」が成り立つということである。 DNR {\displaystyle {\mbox{DNR}}\,} は、 WWKL 0 {\displaystyle {\mbox{WWKL}}_{0}\,} よりも真に弱い。(Lempp et al., 2004).
「超算術的な集合全体からなる構造の上で成り立つ」「極小 ω {\displaystyle \omega \,} モデルは超算術的な集合全体である」という性質を満たす公理系はTheory of hyperarithmetic analysisと呼ばれる。
WKL 0 {\displaystyle {\mbox{WKL}}_{0}\,} は、 RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} に弱ケーニッヒの補題(すべての無限二分木は無限路をもつ)を付け加えた体系である。
弱ケーニッヒの補題は選択公理に近く、実際 RCA 0 {\displaystyle {\text{RCA}}_{0}\,} において、 Π 1 1 {\displaystyle \Pi _{1}^{1}\,} 選択公理と WKL 0 {\displaystyle {\text{WKL}}_{0}\,} が同値であることを示せる。また、 Σ 1 0 {\displaystyle \Sigma _{1}^{0}\,} 分離原理とも同値になる。
WKL 0 {\displaystyle {\mbox{WKL}}_{0}\,} は、 RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} よりも証明能力が高く、 WKL 0 {\displaystyle {\mbox{WKL}}_{0}\,} では非計算可能集合の存在を示せる。
RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} と WKL 0 {\displaystyle {\mbox{WKL}}_{0}\,} の1階部分は同じ、つまり算術的な定理については証明能力は同じである。
「 ω {\displaystyle \omega \,} -モデル」の ω {\displaystyle \omega \,} は非負整数全体の集合を意味する。
その1階部分が1階ペアノ算術の標準モデルになっているような、2階算術の部分体系のモデルを ω {\displaystyle \omega \,} -モデルと呼ぶ。ただし、2階部分は非標準であっても良い。すなわち、 ω {\displaystyle \omega \,} -モデルは S ⊆ P ( ω ) {\displaystyle S\subseteq {\mathcal {P}}(\omega )\,} ( P ( ω ) {\displaystyle {\mathcal {P}}(\omega )\,} は ω {\displaystyle \omega \,} の部分集合全体のクラス)によって与えられる。数変数は ω {\displaystyle \omega \,} の元として解釈され、定数記号 0 , 1 {\displaystyle 0,1\,} や関数記号 + , × {\displaystyle +,\times \,} は標準的に解釈される。