• Weaker systems than recursive comprehension can be defined. The weak system RCA consists of
elementary function arithmetic EFA (the basic axioms plus Δ induction in the enriched language, with an exponential operation) plus Δ comprehension. Over RCA, recursive comprehension as defined earlier (that is, with Σ 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 has the same
proof theoretic ordinal ω3 as EFA and is conservative over EFA for Π 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 RCA0). WWKL0 is obtained by adjoining this axiom to RCA0. 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 WWKL0 is closely connected to the theory of
algorithmically random sequences. In particular, an ω-model of RCA0 satisfies weak weak Kőnig's lemma if and only if for every set
X there is a set
Y that is 1-random relative to
X. • DNR (short for "diagonally non-recursive") adds to RCA0 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). • Δ-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 Δ-comprehension but not the other way around. • Σ-choice is the statement that if
η(
n,
X) is a Σ formula such that for each
n there exists an
X satisfying
η then there is a sequence of sets
Xn such that
η(
n,
Xn) holds for each
n. Σ-choice also has the hyperarithmetical sets as minimal ω-model. Arithmetical transfinite recursion proves Σ-choice but not the other way around. • HBU (short for "uncountable Heine-Borel") expresses the (open-cover)
compactness of the unit interval, involving
uncountable covers. The latter aspect of HBU makes it only expressible in the language of
third-order arithmetic.
Cousin's theorem (1895) implies HBU, and these theorems use the same notion of cover due to
Cousin and
Lindelöf. HBU is
hard to prove: in terms of the usual hierarchy of comprehension axioms, a proof of HBU requires full second-order arithmetic. •
Ramsey's theorem for infinite graphs does not fall into one of the big five subsystems, and there are many other weaker variants with varying proof strengths.
Stronger systems Adding the full second-order induction axiom scheme to RCA0 results in RCA, the system of recursive comprehension arithmetic with unrestricted induction. Similarly, adding the full second-order induction axiom scheme to WKL0 results in WKL, etc. Over RCA0,
Π transfinite recursion,
∆ determinacy, and the
∆ Ramsey theorem are all equivalent to each other. Over RCA0,
Σ monotonic induction,
Σ determinacy, and the
Σ Ramsey theorem are all equivalent to each other. The following are equivalent: • (schema) Π consequences of Π-CA0 • RCA0 + (schema over finite
n) determinacy in the
nth level of the difference hierarchy of
Σ sets • RCA0 + {
τ:
τ is a true
S2S sentence} The set of Π consequences of second-order arithmetic Z2 has the same theory as RCA0 + (schema over finite
n) determinacy in the
nth level of the difference hierarchy of
Σ sets. For a
poset P, let MF(
P) denote the topological space consisting of the filters on
P whose open sets are the sets of the form for some . The following statement is equivalent to \Pi^1_2\mathsf{-CA}_0 over \Pi^1_1\mathsf{-CA}_0: for any countable poset
P, the topological space MF(
P) is
completely metrizable iff it is
regular. == ω-models and β-models ==