Editing Reverse mathematics (section)

== The big five subsystems of second-order arithmetic ==

[[Second-order arithmetic]] is a formal theory of the natural numbers and sets of natural numbers.  Many mathematical objects, such as [[countable set|countable]] [[ring (mathematics)|rings]], [[group (mathematics)|groups]], and [[field (mathematics)|fields]], as well as points in [[effective Polish space]]s, can be represented as sets of natural numbers, and modulo this representation can be studied in second-order arithmetic.

Reverse mathematics makes use of several subsystems of second-order arithmetic. A typical reverse mathematics theorem shows that a particular mathematical theorem ''T'' is equivalent to a particular subsystem ''S'' of second-order arithmetic over a weaker subsystem ''B''. This weaker system ''B'' is known as the '''base system''' for the result; in order for the reverse mathematics result to have
meaning, this system must not itself be able to prove the mathematical theorem ''T''.{{citation needed|date=July 2017}}

Steve Simpson describes five particular subsystems of second-order arithmetic, which he calls the '''Big Five''', that occur frequently in reverse mathematics.{{sfnp|Simpson|2009}}<ref>Simpson claims to have ''not'' invented the term. [{{cite web|url=https://www.youtube.com/watch?v=asPCn9-qcfg&t=540s |title=Panel Discussion |last1=Simpson |first1=S. |last2=Eastaugh |first2=B. |last3=Dean |first3=W. |location=Paris, France |date=June 17, 2022 |website=YouTube |publisher=University of Chicago, Reverse Mathematics and its Philosophy}}]</ref> In order of increasing strength, these systems are named by the initialisms RCA<sub>0</sub>, WKL<sub>0</sub>, ACA<sub>0</sub>, ATR<sub>0</sub>, and Π{{su|p=1|b=1}}-CA<sub>0</sub>.

The following table summarizes the "big five" systems{{sfnp|Simpson|2009|loc=p.42}} and lists the counterpart systems in higher-order arithmetic.<ref name=k05h08/>  
The latter generally prove the same second-order sentences (or a large subset) as the original second-order systems.<ref name=k05h08/>
{| class="wikitable"
!Subsystem
!Stands for
![[Ordinal analysis|Ordinal]]
!Corresponds roughly to
!Comments
!Higher-order counterpart
|-
|RCA<sub>0</sub>
|Recursive comprehension axiom
|&omega;<sup>&omega;</sup>
|Constructive mathematics ([[Errett Bishop|Bishop]])
|The base theory 
|RCA{{math|{{su|p=&omega;|b=0}}}}; proves the same second-order sentences as RCA<sub>0</sub>
|-
|WKL<sub>0</sub>
|Weak Kőnig's lemma
|&omega;<sup>&omega;</sup>
|Finitistic reductionism ([[David Hilbert|Hilbert]])
| Conservative over [[Primitive recursive arithmetic|PRA]] (resp. RCA<sub>0</sub>) for {{math|Π{{su|p=0|b=2}}}} (resp. {{math|Π{{su|p=1|b=1}}}}) sentences
|Fan functional; computes modulus of uniform continuity on <math>2^{\mathbb{N}}</math> for continuous functions
|-
|ACA<sub>0</sub>
|Arithmetical comprehension axiom
|[[epsilon numbers (mathematics)|&epsilon;<sub>0</sub>]]
|Predicativism ([[Hermann Weyl|Weyl]], [[Solomon Feferman|Feferman]])
|Conservative over Peano arithmetic for arithmetical sentences
|The 'Turing jump' functional <math>\exists^2</math> expresses the existence of a discontinuous function on {{mathbb|R}}
|-
|ATR<sub>0</sub>
|Arithmetical transfinite recursion
|[[Feferman–Schütte ordinal|&Gamma;<sub>0</sub>]]
|Predicative reductionism (Friedman, Simpson)
|Conservative over Feferman's system IR for {{math|Π{{su|p=1|b=1}}}} sentences
| The 'transfinite recursion' functional outputs the set claimed to exist by ATR<sub>0</sub>.      
|-
|Π{{su|p=1|b=1}}-CA<sub>0</sub>
|Π{{su|p=1|b=1}} comprehension axiom
|[[Buchholz's ordinal|&Psi;<sub>0</sub>(&Omega;<sub>&omega;</sub>)]]
|Impredicativism
|
| The Suslin functional <math>S^2</math> decides {{math|Π{{su|p=1|b=1}}}}-formulas (restricted to second-order parameters).  
|}

The subscript <sub>0</sub> in these names means that the induction scheme has been restricted from the full second-order induction scheme.{{sfnp|Simpson|2009|p=6}} For example, ACA<sub>0</sub> includes the induction axiom {{math|(0 ∈ ''X'' {{and}} ∀''n''(''n'' ∈ ''X'' → ''n'' + 1 ∈ ''X'')) → ∀''n'' ''n'' ∈ X}}. This together with the full comprehension axiom of second-order arithmetic  implies the full second-order induction scheme given by the universal closure of {{math|(''φ''(0) {{and}} ∀''n''(''φ''(''n'') → ''φ''(''n''+1))) → ∀''n'' ''φ''(''n'')}} for any second-order formula ''φ''. However ACA<sub>0</sub> does not have the full comprehension axiom, and the subscript <sub>0</sub> is a reminder that it does not have the full second-order induction scheme either.  This restriction is important: systems with restricted induction have significantly lower [[Ordinal analysis|proof-theoretical ordinals]] than systems with the full second-order induction scheme.

=== The base system RCA<sub>0</sub>===
RCA<sub>0</sub> is the fragment of second-order arithmetic whose axioms are the axioms of [[Robinson arithmetic]], [[Induction, bounding and least number principles|induction for &Sigma;{{su|p=0|b=1}} formulas]], and comprehension for {{DELTA}}{{su|p=0|b=1}} formulas.

The subsystem RCA<sub>0</sub> is the one most commonly used as a base system for reverse mathematics. The initials "RCA" stand for "recursive comprehension axiom", where "recursive" means "computable", as in [[computable function|recursive function]].  This name is used because RCA<sub>0</sub> corresponds informally to "computable mathematics". In particular, any set of natural numbers that can be proven to exist in RCA<sub>0</sub> is computable, and thus any theorem that implies that noncomputable sets exist is not provable in RCA<sub>0</sub>. To this extent, RCA<sub>0</sub> is a constructive system, although it does not meet the requirements of the program of [[constructivism (mathematics)|constructivism]] because it is a theory in classical logic including the [[law of excluded middle]].

Despite its seeming weakness (of not proving any non-computable sets exist), RCA<sub>0</sub> is sufficient to prove a number of classical theorems which, therefore, require only minimal logical strength. These theorems are, in a sense, below the reach of the reverse mathematics enterprise because they are already provable in the base system. The classical theorems provable in RCA<sub>0</sub> include:
* Basic properties of the natural numbers, integers, and rational numbers (for example, that the latter form an [[ordered field]]).
* Basic properties of the real numbers (the real numbers are an [[Archimedean property|Archimedean]] ordered field; any [[nested sequence of closed intervals]] whose lengths tend to zero has a single point in its intersection; the real numbers are not countable).<ref name="Simpson2009" /><sup>Section II.4</sup>
* The [[Baire category theorem]] for a [[complete metric space|complete]] [[separable space|separable]] [[metric space]] (the separability condition is necessary to even state the theorem in the language of second-order arithmetic).<ref name="Simpson2009" /><sup>theorem II.5.8</sup>
* The [[intermediate value theorem]] on continuous real functions.<ref name="Simpson2009" /><sup>theorem II.6.6</sup>
* The [[Banach–Steinhaus theorem]] for a sequence of continuous linear operators on separable Banach spaces.<ref name="Simpson2009" /><sup>theorem II.10.8</sup>
* A weak version of [[Gödel's completeness theorem]] (for a set of sentences, in a countable language, that is already closed under consequence).
* The existence of an [[algebraic closure]] for a countable field (but not its uniqueness).<ref name="Simpson2009" /><sup>II.9.4--II.9.8</sup>
* The existence and uniqueness of the [[Real closed field|real closure]] of a countable ordered field.<ref name="Simpson2009" /><sup>II.9.5, II.9.7</sup>

The first-order part of RCA<sub>0</sub> (the theorems of the system that do not involve any set variables) is the set of theorems of first-order Peano arithmetic with [[Induction, bounding and least number principles|induction]] limited to &Sigma;{{su|p=0|b=1}} formulas.  It is provably consistent, as is RCA<sub>0</sub>, in full first-order Peano arithmetic.

=== Weak Kőnig's lemma WKL<sub>0</sub>===

The subsystem WKL<sub>0</sub> consists of RCA<sub>0</sub> plus a weak form of [[Kőnig's lemma]], namely the statement that every infinite subtree of the full binary tree (the tree of all finite sequences of 0's and 1's) has an infinite path. This proposition, which is known as ''weak Kőnig's lemma'', is easy to state in the language of second-order arithmetic. WKL<sub>0</sub> can also be defined as the principle of &Sigma;{{su|p=0|b=1}} separation (given two &Sigma;{{su|p=0|b=1}} formulas of a free variable ''n'' that are exclusive, there is a set containing all ''n'' satisfying the one and no ''n'' satisfying the other). When this axiom is added to RCA<sub>0</sub>, the resulting subsystem is called WKL<sub>0</sub>. A similar distinction between particular axioms on the one hand, and subsystems including the basic axioms and induction on the other hand, is made for the stronger subsystems described below.

In a sense, weak Kőnig's lemma is a form of the [[axiom of choice]] (although, as stated, it can be proven in classical Zermelo–Fraenkel set theory without the axiom of choice).  It is not constructively valid in some senses of the word "constructive".

To show that WKL<sub>0</sub> is actually stronger than (not provable in) RCA<sub>0</sub>, it is sufficient to exhibit a theorem of WKL<sub>0</sub> that implies that noncomputable sets exist. This is not difficult; WKL<sub>0</sub> implies the existence of separating sets for effectively inseparable recursively enumerable sets.

It turns out that RCA<sub>0</sub> and WKL<sub>0</sub> have the same first-order part, meaning that they prove the same first-order sentences.  WKL<sub>0</sub> can prove a good number of classical mathematical results that do not follow from RCA<sub>0</sub>, however.  These results are not expressible as first-order statements but can be expressed as second-order statements.

The following results are equivalent to weak Kőnig's lemma and thus to WKL<sub>0</sub> over RCA<sub>0</sub>:

* The [[Heine–Borel theorem]] for the closed unit real interval, in the following sense: every covering by a sequence of open intervals has a finite subcovering.
* The Heine–Borel theorem for complete totally bounded separable metric spaces (where covering is by a sequence of open balls).
* A continuous real function on the closed unit interval (or on any compact separable metric space, as above) is bounded (or: bounded and reaches its bounds).
* A continuous real function on the closed unit interval can be uniformly approximated by polynomials (with rational coefficients).
* A continuous real function on the closed unit interval is uniformly continuous.
* A continuous real function on the closed unit interval is [[Riemann integral|Riemann]] integrable.
* The [[Brouwer fixed point theorem]] (for continuous functions on an <math>n</math>-simplex).<ref name="Simpson2009" /><sup>Theorem IV.7.7</sup>
* The separable [[Hahn–Banach theorem]] in the form: a bounded linear form on a subspace of a separable Banach space extends to a bounded linear form on the whole space.
* The [[Jordan curve theorem]].
* Gödel's completeness theorem (for a countable language).
* Determinacy for open (or even clopen) games on {0,1} of length ω.
* Every countable [[commutative ring]] has a [[prime ideal]].
* Every countable formally real field is orderable.
* Uniqueness of algebraic closure (for a countable field).
* The [[De Bruijn–Erdős theorem (graph theory)|De Bruijn–Erdős theorem]] for countable graphs: every countable graph whose finite subgraphs are <math>k</math>-colorable is <math>k</math>-colorable.<ref>{{cite journal
 | last = Schmerl | first = James H.
 | doi = 10.1002/1521-3870(200010)46:4<543::AID-MALQ543>3.0.CO;2-E
 | issue = 4
 | journal = Mathematical Logic Quarterly
 | mr = 1791549
 | pages = 543–548
 | title = Graph coloring and reverse mathematics
 | volume = 46
 | year = 2000}}</ref>

=== Arithmetical comprehension ACA<sub>0</sub>===

ACA<sub>0</sub> is RCA<sub>0</sub> plus the comprehension scheme for arithmetical formulas (which is sometimes called the "arithmetical comprehension axiom"). That is, ACA<sub>0</sub> allows us to form the set of natural numbers satisfying an arbitrary arithmetical formula (one with no bound set variables, although possibly containing set parameters).<ref name="Simpson2009" /><sup>pp. 6--7</sup> Actually, it suffices to add to RCA<sub>0</sub> the comprehension scheme for &Sigma;<sub>1</sub> formulas (also including second-order free variables) in order to obtain full arithmetical comprehension.<ref name="Simpson2009"/><sup>Lemma III.1.3</sup>

The first-order part of ACA<sub>0</sub> is exactly first-order Peano arithmetic; ACA<sub>0</sub> is a ''conservative'' extension of first-order Peano arithmetic.<ref name="Simpson2009" /><sup>Corollary IX.1.6</sup>  The two systems are provably (in a weak system) equiconsistent.  ACA<sub>0</sub> can be thought of as a framework of [[Impredicativity|predicative]] mathematics, although there are predicatively provable theorems that are not provable in ACA<sub>0</sub>. Most of the fundamental results about the natural numbers, and many other mathematical theorems, can be proven in this system.

One way of seeing that ACA<sub>0</sub> is stronger than WKL<sub>0</sub> is to exhibit a model of WKL<sub>0</sub> that does not contain all arithmetical sets. In fact, it is possible to build a model of WKL<sub>0</sub> consisting entirely of [[Low (computability)|low sets]] using the [[low basis theorem]], since low sets relative to low sets are low.

The following assertions are equivalent to ACA<sub>0</sub>
over RCA<sub>0</sub>:
* The sequential completeness of the real numbers (every bounded increasing sequence of real numbers has a limit).<ref name="Simpson2009" /><sup>theorem III.2.2</sup>
* The [[Bolzano–Weierstrass theorem]].<ref name="Simpson2009" /><sup>theorem III.2.2</sup>
* [[Ascoli's theorem]]: every bounded equicontinuous sequence of real functions on the unit interval has a uniformly convergent subsequence.
* Every countable field embeds isomorphically into its algebraic closure.<ref name="Simpson2009" /><sup>theorem III.3.2</sup>
* Every countable commutative ring has a [[maximal ideal]].<ref name="Simpson2009" /><sup>theorem III.5.5</sup>
* Every countable vector space over the rationals (or over any countable field) has a basis.<ref name="Simpson2009" /><sup>theorem III.4.3</sup>
* For any countable fields <math>K\subseteq L</math>, there is a [[transcendence basis]] for <math>L</math> over <math>K</math>.<ref name="Simpson2009" /><sup>theorem III.4.6</sup>
* Kőnig's lemma (for arbitrary finitely branching trees, as opposed to the weak version described above).<ref name="Simpson2009" /><sup>theorem III.7.2</sup>
* For any countable group <math>G</math> and any subgroups <math>H,I</math> of <math>G</math>, the subgroup generated by <math>H\cup I</math> exists.<ref>S. Takashi, "[https://core.ac.uk/download/pdf/236077134.pdf Reverse Mathematics and Countable Algebraic Systems]". Ph.D. thesis, Tohoku University, 2016.</ref><sup>p.40</sup>
* Any partial function can be extended to a total function.<ref>M. Fujiwara, T. Sato, "[https://repository.kulib.kyoto-u.ac.jp/dspace/handle/2433/223934 Note on total and partial functions in second-order arithmetic]". In ''1950 Proof Theory, Computation Theory and Related Topics'', June 2015.</ref><!--This source says ACA, but it looks like the schema and not the version of ACA_0 with second-order induction-->
* Various theorems in combinatorics, such as certain forms of [[Ramsey's theorem]].{{sfnp|Hirschfeldt|2014}}<ref name="Simpson2009" /><sup>Theorem III.7.2</sup>

=== Arithmetical transfinite recursion ATR<sub>0</sub>===

The system ATR<sub>0</sub> adds to ACA<sub>0</sub> an axiom that states, informally, that any arithmetical functional (meaning any arithmetical formula with a free number variable ''n'' and a free set variable ''X'', seen as the operator taking ''X'' to the set of ''n'' satisfying the formula) can be iterated transfinitely along any countable [[well ordering]] starting with any set.  ATR<sub>0</sub> is equivalent over ACA<sub>0</sub> to the principle of &Sigma;{{su|p=1|b=1}} separation. ATR<sub>0</sub> is impredicative, and has the [[Ordinal analysis|proof-theoretic ordinal]] <math>\Gamma_0</math>, the supremum of that of predicative systems.

ATR<sub>0</sub> proves the consistency of ACA<sub>0</sub>, and thus by [[Gödel's incompleteness theorems|Gödel's theorem]] it is strictly stronger.

The following assertions are equivalent to
ATR<sub>0</sub> over RCA<sub>0</sub>:
* Any two countable well orderings are comparable. That is, they are isomorphic or one is isomorphic to a proper initial segment of the other.<ref name="Simpson2009" /><sup>theorem V.6.8</sup>
* [[Ulm's theorem]] for countable reduced Abelian groups.
* The [[perfect set property|perfect set theorem]], which states that every uncountable closed subset of a complete separable metric space contains a perfect closed set.
* [[Lusin's separation theorem]] (essentially &Sigma;{{su|p=1|b=1}} separation).<ref name="Simpson2009" /><sup>Theorem V.5.1</sup>
* [[Determinacy]] for [[open set]]s in the [[Baire space]].

=== Π{{su|p=1|b=1}} comprehension Π{{su|p=1|b=1}}-CA<sub>0</sub>===

Π{{su|p=1|b=1}}-CA<sub>0</sub> is stronger than arithmetical transfinite recursion and is fully impredicative. It consists of RCA<sub>0</sub> plus the comprehension scheme for Π{{su|p=1|b=1}} formulas.

In a sense, Π{{su|p=1|b=1}}-CA<sub>0</sub> comprehension is to arithmetical transfinite recursion (&Sigma;{{su|p=1|b=1}} separation) as ACA<sub>0</sub> is to weak Kőnig's lemma (&Sigma;{{su|p=0|b=1}} separation).   It is equivalent to several statements of descriptive set theory whose proofs make use of strongly impredicative arguments; this equivalence shows that these impredicative arguments cannot be removed.

The following theorems are equivalent to Π{{su|p=1|b=1}}-CA<sub>0</sub>  over RCA<sub>0</sub>:
* The [[Cantor–Bendixson theorem]] (every closed set of reals is the union of a perfect set and a countable set).<ref name="Simpson2009" /><sup>Exercise VI.1.7</sup>
* [[Silver's dichotomy]] (every coanalytic equivalence relation has either countably many equivalence classes or a perfect set of incomparables)<ref name="Simpson2009" /><sup>Theorem VI.3.6</sup>
* Every countable abelian group is the direct sum of a divisible group and a reduced group.<ref name="Simpson2009" /><sup>Theorem VI.4.1</sup>
* Determinacy for <math>\Sigma^0_1\land\Pi^0_1</math> games.<ref name="Simpson2009" /><sup>Theorem VI.5.4</sup>