The reverse mathematics program was foreshadowed by results in set theory such as the classical theorem that the axiom of choice and Zorn's lemma are equivalent over ZF set theory.
Reverse mathematics is usually carried out using subsystems of second-order arithmetic,[1] where many of its definitions and methods are inspired by previous work in constructive analysis and proof theory.
[clarification needed] The program was founded by Harvey Friedman (1975, 1976)[2] and brought forward by Steve Simpson.
A standard reference for the subject is Simpson (2009), while an introduction for non-specialists is Stillwell (2018).
An introduction to higher-order reverse mathematics, and also the founding paper, is Kohlenbach (2005).
A comprehensive introduction, covering major results and methods, is Dzhafarov & Mummert (2022)[3] In reverse mathematics, one starts with a framework language and a base theory—a core axiom system—that is too weak to prove most of the theorems one might be interested in, but still powerful enough to develop the definitions necessary to state these theorems.
[1] The reversal establishes that no axiom system S′ that extends the base system can be weaker than S while still proving T. Most reverse mathematics research focuses on subsystems of second-order arithmetic.
Such a scheme states that any set of natural numbers definable by a formula of a given complexity exists.
In the context of second-order arithmetic, results such as Post's theorem establish a close link between the complexity of a formula and the (non)computability of the set it defines.
Many principles that imply the axiom of choice in their general form (such as "Every vector space has a basis") become provable in weak subsystems of second-order arithmetic when they are restricted.
For example, "every field has an algebraic closure" is not provable in ZF set theory, but the restricted form "every countable field has an algebraic closure" is provable in RCA0, the weakest system typically employed in reverse mathematics.
Such a higher-order axiom states the existence of a functional that decides the truth or falsity of formulas of a given complexity.
[5] For instance, the base theory of higher-order reverse mathematics, called RCAω0, proves the same sentences as RCA0, up to language.
As noted in the previous paragraph, second-order comprehension axioms easily generalize to the higher-order framework.
However, theorems expressing the compactness of basic spaces behave quite differently in second- and higher-order arithmetic: on one hand, when restricted to countable covers/the language of second-order arithmetic, the compactness of the unit interval is provable in WKL0 from the next section.
exhibit the same behavior, and many basic properties of the gauge integral are equivalent to the compactness of the underlying space.
Many mathematical objects, such as countable rings, groups, and fields, as well as points in effective Polish spaces, can be represented as sets of natural numbers, and modulo this representation can be studied in second-order arithmetic.
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] Steve Simpson describes five particular subsystems of second-order arithmetic, which he calls the Big Five, that occur frequently in reverse mathematics.
To this extent, RCA0 is a constructive system, although it does not meet the requirements of the program of constructivism because it is a theory in classical logic including the law of excluded middle.
These theorems are, in a sense, below the reach of the reverse mathematics enterprise because they are already provable in the base system.
The subsystem WKL0 consists of RCA0 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.
To show that WKL0 is actually stronger than (not provable in) RCA0, it is sufficient to exhibit a theorem of WKL0 that implies that noncomputable sets exist.
WKL0 can prove a good number of classical mathematical results that do not follow from RCA0, however.
Most of the fundamental results about the natural numbers, and many other mathematical theorems, can be proven in this system.
The following assertions are equivalent to ACA0 over RCA0: The system ATR0 adds to ACA0 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.
The following assertions are equivalent to ATR0 over RCA0: Π11-CA0 is stronger than arithmetical transfinite recursion and is fully impredicative.
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.
[17] The ω in ω-model stands for the set of non-negative integers (or finite ordinals).
A β-model is an ω model that agrees with the standard ω-model on truth of