Editing Reverse mathematics (section)

=== 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>