Reverse mathematics is the branch of mathematics concerned with what are the minimal axioms needed to prove the particular theorem. It turns out that over a weak base theory, many mathematical statements are equivalent to the particular additional axiom needed to prove them.

Most of mathematics can be formalized in second order arithmetic, and the famous theorems proved in ACA₀, which is conservative over Peano arithmetic.

Most relevant sets of real numbers, including all Borel sets, can be coded by real numbers with the membership relation expressible in second order arithmetic . The primary difference between doing classical mathematics in set theory (ZFC) and doing it in second order arithmetic is that in second order arithmetic one deals with codes for sets rather than sets themselves (except sets of integers).

Under the correct formalizations, most of the general theorems are actually equivalent to the minimal canonical axiom required for their proof. Most of the basic results in analysis and algebra are provable WKL₀, which has the same consistency strength as primitive recursive arithmetic and whose repertoire provably recursive functions consists of the primitive recursive functions.

Basic arithmetical theorems can be proved in exponential function arithmetic, EFA, which besides the basic axioms for addition, multiplication, and exponentiation, includes the axiom of induction for bounded quantifier formulas. EFA suffices, among other things, to prove that the theory of real closed fields, and hence of classical geometry, is complete.

External link

• Detailed introduction to reverse mathematics