Editing Reverse mathematics (section)

== Additional systems ==

* Weaker systems than recursive comprehension can be defined.  The weak system RCA{{su|p=*|b=0}} consists of [[elementary function arithmetic]] EFA (the basic axioms plus Δ{{su|p=0|b=0}} induction in the enriched language with an exponential operation) plus Δ{{su|p=0|b=1}} comprehension. Over RCA{{su|p=*|b=0}},  recursive comprehension as defined earlier (that is, with Σ{{su|p=0|b=1}} 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{{su|p=*|b=0}} has the same [[Ordinal analysis|proof theoretic ordinal]] &omega;<sup>3</sup> as EFA and is conservative over EFA for &Pi;{{su|p=0|b=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<sub>0</sub>). WWKL<sub>0</sub> is obtained by adjoining this axiom to RCA<sub>0</sub>.  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<sub>0</sub> is closely connected to the theory of [[algorithmically random sequence]]s.  In particular, an ω-model of RCA<sub>0</sub> 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 RCA<sub>0</sub> an axiom asserting the existence of a [[Kleene's recursion theorem#Fixed-point-free functions|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 ''e''th partial recursive function with oracle ''A'' is not equal to ''f''. DNR is strictly weaker than WWKL (Lempp ''et al.'', 2004).
* Δ{{su|p=1|b=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 Δ{{su|p=1|b=1}}-comprehension but not the other way around.
* Σ{{su|p=1|b=1}}-choice is the statement that if ''η''(''n'',''X'') is a Σ{{su|p=1|b=1}} formula such that for each ''n'' there exists an ''X'' satisfying η then there is a sequence of sets ''X<sub>n</sub>'' such that ''η''(''n'',''X<sub>n</sub>'') holds for each ''n''.  Σ{{su|p=1|b=1}}-choice also has the hyperarithmetical sets as minimal ω-model.  Arithmetical transfinite recursion proves Σ{{su|p=1|b=1}}-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.{{sfnp|Normann|Sanders|2018}}
* [[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.{{sfnp|Hirschfeldt|2014}}

===Stronger systems===
Over RCA<sub>0</sub>, '''Π{{su|p=1|b=1}}''' transfinite recursion, '''∆{{su|p=0|b=2}}''' determinacy, and the '''∆{{su|p=1|b=1}}''' Ramsey theorem are all equivalent to each other.

Over RCA<sub>0</sub>, '''Σ{{su|p=1|b=1}}''' monotonic induction, '''Σ{{su|p=0|b=2}}''' determinacy, and the '''Σ{{su|p=1|b=1}}''' Ramsey theorem are all equivalent to each other.

The following are equivalent:<ref>{{cite conference |conference=LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science |date=2016  |title=How unprovable is Rabin's decidability theorem? |first1=Leszek |last1=Kołodziejczyk |first2=Henryk |last2=Michalewski |arxiv=1508.06780 }}</ref><ref>{{cite web |last=Kołodziejczyk |first=Leszek |url = https://cs.nyu.edu/pipermail/fom/2015-October/019257.html |title=Question on Decidability of S2S |publisher=FOM |date=October 19, 2015}}</ref>
* (schema) Π{{su|p=1|b=3}} consequences of Π{{su|p=1|b=2}}-CA<sub>0</sub>
* RCA<sub>0</sub> + (schema over finite ''n'')  determinacy in the ''n''th level of the difference hierarchy of '''Σ{{su|p=0|b=2}}''' sets
* RCA<sub>0</sub> + {τ: τ is a true [[S2S (mathematics)|S2S]] sentence}

The set of Π{{su|p=1|b=3}} consequences of second-order arithmetic Z<sub>2</sub> has the same theory as RCA<sub>0</sub> + (schema over finite ''n'')  determinacy in the ''n''th level of the difference hierarchy of '''Σ{{su|p=0|b=3}}''' sets.<ref>{{cite journal |first1=Antonio |last1=Montalban |first2=Richard |last2=Shore |title=The limits of determinacy in second order arithmetic: consistency and complexity strength | journal=[[Israel Journal of Mathematics]] |volume=204 |year=2014 | pages=477–508 |doi=10.1007/s11856-014-1117-9 | doi-access=|s2cid=287519 }}</ref>

For a [[poset]] <math>P</math>, let <math>\textrm{MF}(P)</math> denote the topological space consisting of the filters on <math>P</math> whose open sets are the sets of the form <math>\{F\in\textrm{MF}(P)\mid p\in F\}</math> for some <math>p\in P</math>. The following statement is equivalent to <math>\Pi^1_2\mathsf{-CA}_0</math> over <math>\Pi^1_1\mathsf{-CA}_0</math>: for any countable poset <math>P</math>, the topological space <math>\textrm{MF}(P)</math> is [[Completely metrizable space|completely metrizable]] iff it is [[Regular topological space|regular]].<ref>C. Mummert, S. G. Simpson. "Reverse mathematics and <math>\Pi^1_2</math> comprehension". In ''Bulletin of Symbolic Logic'' vol. 11 (2005), pp.526–533.</ref>