Editing Reverse mathematics (section)

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