This article has multiple issues. Please help improve it or discuss these issues on the talk page . (Learn how and when to remove these template messages)

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of deriving theorems from axioms. It can be conceptualized as sculpting out necessary conditions from sufficient ones.
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. The goal of reverse mathematics, however, is to study possible axioms of ordinary theorems of mathematics rather than possible axioms for set theory.
Reverse mathematics is usually carried out using subsystems of secondorder arithmetic, where many of its definitions and methods are inspired by previous work in constructive analysis and proof theory. The use of secondorder arithmetic also allows many techniques from recursion theory to be employed; many results in reverse mathematics have corresponding results in computable analysis. Recently,^{[ when? ]}higherorder reverse mathematics has been introduced, in which the focus is on subsystems of higherorder arithmetic, and the associated richer language.^{[ clarification needed ]}
The program was founded by HarveyFriedman ( 1975 , 1976 ) and brought forward by Steve Simpson. A standard reference for the subject is Simpson (2009), while an introduction for nonspecialists is Stillwell (2018). An introduction to higherorder reverse mathematics, and also the founding paper, is Kohlenbach (2005).
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. For example, to study the theorem “Every bounded sequence of real numbers has a supremum” it is necessary to use a base system that can speak of real numbers and sequences of real numbers.
For each theorem that can be stated in the base system but is not provable in the base system, the goal is to determine the particular axiom system (stronger than the base system) that is necessary to prove that theorem. To show that a system S is required to prove a theorem T, two proofs are required. The first proof shows T is provable from S; this is an ordinary mathematical proof along with a justification that it can be carried out in the system S. The second proof, known as a reversal, shows that T itself implies S; this proof is carried out in the base system. 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 secondorder arithmetic. The body of research in reverse mathematics has established that weak subsystems of secondorder arithmetic suffice to formalize almost all undergraduatelevel mathematics. In secondorder arithmetic, all objects can be represented as either natural numbers or sets of natural numbers. For example, in order to prove theorems about real numbers, the real numbers can be represented as Cauchy sequences of rational numbers, each of which can be represented as a set of natural numbers.
The axiom systems most often considered in reverse mathematics are defined using axiom schemes called comprehension schemes. Such a scheme states that any set of natural numbers definable by a formula of a given complexity exists. In this context, the complexity of formulas is measured using the arithmetical hierarchy and analytical hierarchy.
The reason that reverse mathematics is not carried out using set theory as a base system is that the language of set theory is too expressive. Extremely complex sets of natural numbers can be defined by simple formulas in the language of set theory (which can quantify over arbitrary sets). In the context of secondorder 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.
Another effect of using secondorder arithmetic is the need to restrict general mathematical theorems to forms that can be expressed within arithmetic. For example, secondorder arithmetic can express the principle "Every countable vector space has a basis" but it cannot express the principle "Every vector space has a basis". In practical terms, this means that theorems of algebra and combinatorics are restricted to countable structures, while theorems of analysis and topology are restricted to separable spaces. 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 secondorder 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 RCA_{0}, the weakest system typically employed in reverse mathematics.
A recent strand of higherorder reverse mathematics research, initiated by Ulrich Kohlenbach, focuses on subsystems of higherorder arithmetic (Kohlenbach (2005)). Due to the richer language of higherorder arithmetic, the use of representations (aka 'codes') common in secondorder arithmetic, is greatly reduced. For example, a continuous function on the Cantor space is just a function that maps binary sequences to binary sequences, and that also satisfies the usual 'epsilondelta'definition of continuity.
Higherorder reverse mathematics includes higherorder versions of (secondorder) comprehension schemes. Such a higherorder axiom states the existence of a functional that decides the truth or falsity of formulas of a given complexity. In this context, the complexity of formulas is also measured using the arithmetical hierarchy and analytical hierarchy. The higherorder counterparts of the major subsystems of secondorder arithmetic generally prove the same secondorder sentences (or a large subset) as the original secondorder systems (see Kohlenbach (2005) and Hunter (2008)). For instance, the base theory of higherorder reverse mathematics, called RCA^{ω}
_{0}, proves the same sentences as RCA_{0}, up to language.
As noted in the previous paragraph, secondorder comprehension axioms easily generalize to the higherorder framework. However, theorems expressing the compactness of basic spaces behave quite differently in second and higherorder arithmetic: on one hand, when restricted to countable covers/the language of secondorder arithmetic, the compactness of the unit interval is provable in WKL_{0} from the next section. On the other hand, given uncountable covers/the language of higherorder arithmetic, the compactness of the unit interval is only provable from (full) secondorder arithmetic (Normann and Sanders (2018) ). Other covering lemmas (e.g. due to Lindelöf, Vitali, Besicovitch, etc.) exhibit the same behavior, and many basic properties of the gauge integral are equivalent to the compactness of the underlying space.
Secondorder arithmetic is a formal theory of the natural numbers and sets of natural numbers. 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 secondorder arithmetic.
Reverse mathematics makes use of several subsystems of secondorder arithmetic. A typical reverse mathematics theorem shows that a particular mathematical theorem T is equivalent to a particular subsystem S of secondorder 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 ]}
Simpson (2009) describes five particular subsystems of secondorder arithmetic, which he calls the Big Five, that occur frequently in reverse mathematics. In order of increasing strength, these systems are named by the initialisms RCA_{0}, WKL_{0}, ACA_{0}, ATR_{0}, and Π^{1}
_{1}CA_{0}.
The following table summarizes the "big five" systems (Simpson (2009 , p.42)) and lists the counterpart systems in higherorder arithmetic (Kohlenbach (2008) ). The latter generally prove the same secondorder sentences (or a large subset) as the original secondorder systems (see Kohlenbach (2005) and Hunter (2008)).
Subsystem  Stands for  Ordinal  Corresponds roughly to  Comments  Higherorder counterpart 

RCA_{0}  Recursive comprehension axiom  ω^{ω}  Constructive mathematics (Bishop)  The base theory  RCA^{ω} _{0}; proves the same secondorder sentences as RCA_{0} 
WKL_{0}  Weak Kőnig's lemma  ω^{ω}  Finitistic reductionism (Hilbert)  Conservative over PRA (resp. RCA_{0}) for Π^{0} _{2} (resp. Π^{1} _{1}) sentences  Fan functional; computes modulus of uniform continuity on for continuous functions 
ACA_{0}  Arithmetical comprehension axiom  ε_{0}  Predicativism (Weyl, Feferman)  Conservative over Peano arithmetic for arithmetical sentences  The 'Turing jump' functional expresses the existence of a discontinuous function on 
ATR_{0}  Arithmetical transfinite recursion  Γ_{0}  Predicative reductionism (Friedman, Simpson)  Conservative over Feferman's system IR for Π^{1} _{1} sentences  The 'transfinite recursion' functional outputs the set claimed to exist by ATR_{0}. 
Π^{1} _{1}CA_{0}  Π^{1} _{1} comprehension axiom  Ψ_{0}(Ω_{ω})  Impredicativism  The Suslin functional decides Π^{1} _{1}formulas (restricted to secondorder parameters). 
The subscript _{0} in these names means that the induction scheme has been restricted from the full secondorder induction scheme ( Simpson 2009 , p. 6). For example, ACA_{0} includes the induction axiom (0 ∈ X ∧ ∀n(n ∈ X → n + 1 ∈ X)) → ∀n n ∈ X. This together with the full comprehension axiom of secondorder arithmetic implies the full secondorder induction scheme given by the universal closure of (φ(0) ∧ ∀n(φ(n) → φ(n+1))) → ∀nφ(n) for any secondorder formula φ. However ACA_{0} does not have the full comprehension axiom, and the subscript _{0} is a reminder that it does not have the full secondorder induction scheme either. This restriction is important: systems with restricted induction have significantly lower prooftheoretical ordinals than systems with the full secondorder induction scheme.
RCA_{0} is the fragment of secondorder arithmetic whose axioms are the axioms of Robinson arithmetic, induction for Σ^{0}
_{1} formulas, and comprehension for Δ^{0}
_{1} formulas.
The subsystem RCA_{0} 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 recursive function. This name is used because RCA_{0} corresponds informally to "computable mathematics". In particular, any set of natural numbers that can be proven to exist in RCA_{0} is computable, and thus any theorem that implies that noncomputable sets exist is not provable in RCA_{0}. To this extent, RCA_{0} 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.
Despite its seeming weakness (of not proving any noncomputable sets exist), RCA_{0} 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_{0} include:
The firstorder part of RCA_{0} (the theorems of the system that do not involve any set variables) is the set of theorems of firstorder Peano arithmetic with induction limited to Σ^{0}
_{1} formulas. It is provably consistent, as is RCA_{0}, in full firstorder Peano arithmetic.
The subsystem WKL_{0} consists of RCA_{0} 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 secondorder arithmetic. WKL_{0} can also be defined as the principle of Σ^{0}
_{1} separation (given two Σ^{0}
_{1} formulas of a free variable n that are exclusive, there is a class containing all n satisfying the one and no n satisfying the other).
The following remark on terminology is in order. The term “weak Kőnig's lemma” refers to the sentence that says that any infinite subtree of the binary tree has an infinite path. When this axiom is added to RCA_{0}, the resulting subsystem is called WKL_{0}. 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_{0} is actually stronger than (not provable in) RCA_{0}, it is sufficient to exhibit a theorem of WKL_{0} that implies that noncomputable sets exist. This is not difficult; WKL_{0} implies the existence of separating sets for effectively inseparable recursively enumerable sets.
It turns out that RCA_{0} and WKL_{0} have the same firstorder part, meaning that they prove the same firstorder sentences. WKL_{0} can prove a good number of classical mathematical results that do not follow from RCA_{0}, however. These results are not expressible as firstorder statements but can be expressed as secondorder statements.
The following results are equivalent to weak Kőnig's lemma and thus to WKL_{0} over RCA_{0}:
ACA_{0} is RCA_{0} plus the comprehension scheme for arithmetical formulas (which is sometimes called the "arithmetical comprehension axiom"). That is, ACA_{0} 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). Actually, it suffices to add to RCA_{0} the comprehension scheme for Σ_{1} formulas in order to obtain full arithmetical comprehension.
The firstorder part of ACA_{0} is exactly firstorder Peano arithmetic; ACA_{0} is a conservative extension of firstorder Peano arithmetic. The two systems are provably (in a weak system) equiconsistent. ACA_{0} can be thought of as a framework of predicative mathematics, although there are predicatively provable theorems that are not provable in ACA_{0}. 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_{0} is stronger than WKL_{0} is to exhibit a model of WKL_{0} that doesn't contain all arithmetical sets. In fact, it is possible to build a model of WKL_{0} consisting entirely of low sets using the low basis theorem, since low sets relative to low sets are low.
The following assertions are equivalent to ACA_{0} over RCA_{0}:
The system ATR_{0} adds to ACA_{0} an axiom that states, informally, that any arithmetical functional (meaning any arithmetical formula with a free number variable n and a free class 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_{0} is equivalent over ACA_{0} to the principle of Σ^{1}
_{1} separation. ATR_{0} is impredicative, and has the prooftheoretic ordinal , the supremum of that of predicative systems.
ATR_{0} proves the consistency of ACA_{0}, and thus by Gödel's theorem it is strictly stronger.
The following assertions are equivalent to ATR_{0} over RCA_{0}:
Π^{1}
_{1}CA_{0} is stronger than arithmetical transfinite recursion and is fully impredicative. It consists of RCA_{0} plus the comprehension scheme for Π^{1}
_{1} formulas.
In a sense, Π^{1}
_{1}CA_{0} comprehension is to arithmetical transfinite recursion (Σ^{1}
_{1} separation) as ACA_{0} is to weak Kőnig's lemma (Σ^{0}
_{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 Π^{1}
_{1}CA_{0} over RCA_{0}:
The ω in ωmodel stands for the set of nonnegative integers (or finite ordinals). An ωmodel is a model for a fragment of secondorder arithmetic whose firstorder part is the standard model of Peano arithmetic, but whose secondorder part may be nonstandard. More precisely, an ωmodel is given by a choice S⊆2^{ω} of subsets of ω. The firstorder variables are interpreted in the usual way as elements of ω, and +, × have their usual meanings, while secondorder variables are interpreted as elements of S. There is a standard ω model where one just takes S to consist of all subsets of the integers. However, there are also other ωmodels; for example, RCA_{0} has a minimal ωmodel where S consists of the recursive subsets of ω.
A β model is an ω model that is equivalent to the standard ωmodel for Π^{1}
_{1} and Σ^{1}
_{1} sentences (with parameters).
Nonω models are also useful, especially in the proofs of conservation theorems.
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that a Cartesian product of a collection of nonempty sets is nonempty. Informally put, the axiom of choice says that given any collection of bins, each containing at least one object, it is possible to make a selection of exactly one object from each bin, even if the collection is infinite. Formally, it states that for every indexed family of nonempty sets there exists an indexed family of elements such that for every . The axiom of choice was formulated in 1904 by Ernst Zermelo in order to formalize his proof of the wellordering theorem.
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in firstorder logic.
Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of provability in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.
In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if it has a model, i.e., there exists an interpretation under which all formulas in the theory are true. This is the sense used in traditional Aristotelian logic, although in contemporary mathematical logic the term satisfiable is used instead. The syntactic definition states a theory is consistent if there is no formula such that both and its negation are elements of the set of consequences of . Let be a set of closed sentences and the set of closed sentences provable from under some formal deductive system. The set of axioms is consistent when for no formula .
Kőnig's lemma or Kőnig's infinity lemma is a theorem in graph theory due to the Hungarian mathematician Dénes Kőnig who published it in 1927. It gives a sufficient condition for an infinite graph to have an infinitely long path. The computability aspects of this theorem have been thoroughly investigated by researchers in mathematical logic, especially in computability theory. This theorem also has important roles in constructive mathematics and proof theory.
Proof theory is a major branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductivelydefined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.
In mathematical logic, a conservative extension is a supertheory of a theory which is often convenient for proving theorems, but proves no new theorems about the language of the original theory. Similarly, a nonconservative extension is a supertheory which is not conservative, and can prove more theorems than the original.
In mathematics, Robinson arithmetic is a finitely axiomatized fragment of firstorder Peano arithmetic (PA), first set out by R. M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q is weaker than PA but it has the same language, and both theories are incomplete. Q is important and interesting because it is a finitely axiomatized fragment of PA that is recursively incompletable and essentially undecidable.
In mathematical logic, a theory is a set of sentences in a formal language. In most scenarios, a deductive system is first understood from context, after which an element of a theory is then called a theorem of the theory. In many deductive systems there is usually a subset that is called "the set of axioms" of the theory , in which case the deductive system is also called an "axiomatic system". By definition, every axiom is automatically a theorem. A firstorder theory is a set of firstorder sentences (theorems) recursively obtained by the inference rules of the system applied to the set of axioms.
In mathematical logic, secondorder arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
In mathematical logic, an ωconsistenttheory is a theory that is not only (syntactically) consistent, but also avoids proving certain infinite combinations of sentences that are intuitively contradictory. The name is due to Kurt Gödel, who introduced the concept in the course of proving the incompleteness theorem.
Gentzen's consistency proof is a result of proof theory in mathematical logic, published by Gerhard Gentzen in 1936. It shows that the Peano axioms of firstorder arithmetic do not contain a contradiction, as long as a certain other system used in the proof does not contain any contradictions either. This other system, today called "primitive recursive arithmetic with the additional principle of quantifierfree transfinite induction up to the ordinal ε_{0}", is neither weaker nor stronger than the system of Peano axioms. Gentzen argued that it avoids the questionable modes of inference contained in Peano arithmetic and that its consistency is therefore less controversial.
In the mathematical discipline of set theory, there are many ways of describing specific countable ordinals. The smallest ones can be usefully and noncircularly expressed in terms of their Cantor normal forms. Beyond that, many ordinals of relevance to proof theory still have computable ordinal notations. However, it is not possible to decide effectively whether a given putative ordinal notation is a notation or not ; various moreconcrete ways of defining ordinals that definitely have notations are available.
Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same firstorder language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.
In mathematical logic, a formula is said to be absolute if it has the same truth value in each of some class of structures. Theorems about absoluteness typically establish relationships between the absoluteness of formulas and their syntactic form.
In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength. If theories have the same prooftheoretic ordinal they are often equiconsistent, and if one theory has a larger prooftheoretic ordinal than another it can often prove the consistency of the second theory.
In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic, is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, x^{y}, together with induction for formulas with bounded quantifiers.
Slicing the Truth: On the Computability Theoretic and Reverse Mathematical Analysis of Combinatorial Principles is a book on reverse mathematics in combinatorics, the study of the axioms needed to prove combinatorial theorems. It was written by Denis R. Hirschfeldt, based on a course given by Hirschfeldt at the National University of Singapore in 2010, and published in 2014 by World Scientific, as volume 28 of the Lecture Notes Series of the Institute for Mathematical Sciences, National University of Singapore.