Reverse Mathematics - Additional Systems

Additional Systems

• Weaker systems than recursive comprehension can be defined. The weak system RCA*
  0 consists of elementary function arithmetic EFA (the basic axioms plus Δ0₀ induction in the enriched language with an exponential operation) plus Δ0₁ comprehension. Over RCA*
  0, recursive comprehension as defined earlier (that is, with Σ0₁ induction) is equivalent to the statement that a polynomial (over a countable field) has only finitely many roots and to the classification theorem for finitely generated Abelian groups. The system RCA*
  0 has the same proof theoretic ordinal ω3 as EFA and is conservative over EFA for Π0
  2 sentences.

• Weak Weak König's Lemma is the statement that a subtree of the infinite binary tree having no infinite paths has an asymptotically vanishing proportion of the leaves at length n (with a uniform estimate as to how many leaves of length n exist). An equivalent formulation is that any subset of Cantor space that has positive measure is nonempty (this is not provable in RCA₀). WWKL₀ is obtained by adjoining this axiom to RCA₀. It is equivalent to the statement that if the unit real interval is covered by a sequence of intervals then the sum of their lengths is at least one. The model theory of WWKL₀ is closely connected to the theory of algorithmically random sequences. In particular, an ω-model of RCA₀ satisfies weak weak König's lemma if and only if for every set X there is a set Y which is 1-random relative to X.

• DNR (short for "diagonally non-recursive") adds to RCA₀ an axiom asserting the existence of a diagonally non-recursive function relative to every set. That is, DNR states that, for any set A, there exists a total function f such that for all e the eth partial recursive function with oracle A is not equal to f. DNR is strictly weaker than WWKL (Lempp et al., 2004).

• Δ1₁-comprehension is in certain ways analogous to arithmetical transfinite recursion as recursive comprehension is to weak König's lemma. It has the hyperarithmetical sets as minimal ω-model. Arithmetical transfinite recursion proves Δ1₁-comprehension but not the other way around.

• Σ1₁-choice is the statement that if η(n,X) is a Σ1₁ formula such that for each n there exists an X satisfying η then there is a sequence of sets X_n such that η(n,X_n) holds for each n. Σ1₁-choice also has the hyperarithmetical sets as minimal ω-model. Arithmetical transfinite recursion proves Σ1₁-choice but not the other way around.