This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: "Reverse mathematics" – news · newspapers · books · scholar · JSTOR (October 2016) (Learn how and when to remove this message)

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 second-order arithmetic,[1] where many of its definitions and methods are inspired by previous work in constructive analysis and proof theory. The use of second-order arithmetic also allows many techniques from recursion theory to be employed; many results in reverse mathematics have corresponding results in computable analysis. In higher-order reverse mathematics, the focus is on subsystems of higher-order arithmetic, and the associated richer language.[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).

General principles

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.[1] The reversal establishes that no axiom system S′ that extends the base system can be weaker than S while still proving T.

Use of second-order arithmetic

Most reverse mathematics research focuses on subsystems of second-order arithmetic. The body of research in reverse mathematics has established that weak subsystems of second-order arithmetic suffice to formalize almost all undergraduate-level mathematics. In second-order 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 sequence 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 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.

Another effect of using second-order arithmetic is the need to restrict general mathematical theorems to forms that can be expressed within arithmetic. For example, second-order 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 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.

Use of higher-order arithmetic

A recent strand of higher-order reverse mathematics research, initiated by Ulrich Kohlenbach in 2005, focuses on subsystems of higher-order arithmetic.[3] Due to the richer language of higher-order arithmetic, the use of representations (aka 'codes') common in second-order 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 'epsilon-delta'-definition of continuity.

Higher-order reverse mathematics includes higher-order versions of (second-order) comprehension schemes. Such a higher-order 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 higher-order counterparts of the major subsystems of second-order arithmetic generally prove the same second-order sentences (or a large subset) as the original second-order systems.[4] For instance, the base theory of higher-order reverse mathematics, called RCAω
, 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. On the other hand, given uncountable covers/the language of higher-order arithmetic, the compactness of the unit interval is only provable from (full) second-order arithmetic.[5] 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.

The big five subsystems of second-order arithmetic

Second-order 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 second-order arithmetic.

Reverse mathematics makes use of several subsystems of second-order arithmetic. A typical reverse mathematics theorem shows that a particular mathematical theorem T is equivalent to a particular subsystem S of second-order 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 second-order 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 RCA0, WKL0, ACA0, ATR0, and Π1

The following table summarizes the "big five" systems[6] and lists the counterpart systems in higher-order arithmetic.[4] The latter generally prove the same second-order sentences (or a large subset) as the original second-order systems.[4]

Subsystem Stands for Ordinal Corresponds roughly to Comments Higher-order counterpart
RCA0 Recursive comprehension axiom ωω Constructive mathematics (Bishop) The base theory RCAω
; proves the same second-order sentences as RCA0
WKL0 Weak Kőnig's lemma ωω Finitistic reductionism (Hilbert) Conservative over PRA (resp. RCA0) for Π0
(resp. Π1
) sentences
Fan functional; computes modulus of uniform continuity on for continuous functions
ACA0 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
ATR0 Arithmetical transfinite recursion Γ0 Predicative reductionism (Friedman, Simpson) Conservative over Feferman's system IR for Π1
The 'transfinite recursion' functional outputs the set claimed to exist by ATR0.
comprehension axiom
Ψ0ω) Impredicativism The Suslin functional decides Π1
-formulas (restricted to second-order parameters).

The subscript 0 in these names means that the induction scheme has been restricted from the full second-order induction scheme.[7] For example, ACA0 includes the induction axiom (0 ∈ X ∧ ∀n(n ∈ X → n + 1 ∈ X)) → ∀n n ∈ X. This together with the full comprehension axiom of second-order arithmetic implies the full second-order induction scheme given by the universal closure of (φ(0) ∧ ∀n(φ(n) → φ(n+1))) → ∀n φ(n) for any second-order formula φ. However ACA0 does not have the full comprehension axiom, and the subscript 0 is a reminder that it does not have the full second-order induction scheme either. This restriction is important: systems with restricted induction have significantly lower proof-theoretical ordinals than systems with the full second-order induction scheme.

The base system RCA0

RCA0 is the fragment of second-order arithmetic whose axioms are the axioms of Robinson arithmetic, induction for Σ0
, and comprehension for Δ0

The subsystem RCA0 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 RCA0 corresponds informally to "computable mathematics". In particular, any set of natural numbers that can be proven to exist in RCA0 is computable, and thus any theorem that implies that noncomputable sets exist is not provable in RCA0. 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.

Despite its seeming weakness (of not proving any non-computable sets exist), RCA0 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 RCA0 include:

The first-order part of RCA0 (the theorems of the system that do not involve any set variables) is the set of theorems of first-order Peano arithmetic with induction limited to Σ0
formulas. It is provably consistent, as is RCA0, in full first-order Peano arithmetic.

Weak Kőnig's lemma WKL0

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. WKL0 can also be defined as the principle of Σ0
separation (given two Σ0
formulas of a free variable n that are exclusive, there is a set containing all n satisfying the one and no n satisfying the other). When this axiom is added to RCA0, the resulting subsystem is called WKL0. 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 WKL0 is actually stronger than (not provable in) RCA0, it is sufficient to exhibit a theorem of WKL0 that implies that noncomputable sets exist. This is not difficult; WKL0 implies the existence of separating sets for effectively inseparable recursively enumerable sets.

It turns out that RCA0 and WKL0 have the same first-order part, meaning that they prove the same first-order sentences. WKL0 can prove a good number of classical mathematical results that do not follow from RCA0, however. These results are not expressible as first-order statements but can be expressed as second-order statements.

The following results are equivalent to weak Kőnig's lemma and thus to WKL0 over RCA0:

Arithmetical comprehension ACA0

ACA0 is RCA0 plus the comprehension scheme for arithmetical formulas (which is sometimes called the "arithmetical comprehension axiom"). That is, ACA0 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 RCA0 the comprehension scheme for Σ1 formulas in order to obtain full arithmetical comprehension.

The first-order part of ACA0 is exactly first-order Peano arithmetic; ACA0 is a conservative extension of first-order Peano arithmetic. The two systems are provably (in a weak system) equiconsistent. ACA0 can be thought of as a framework of predicative mathematics, although there are predicatively provable theorems that are not provable in ACA0. 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 ACA0 is stronger than WKL0 is to exhibit a model of WKL0 that doesn't contain all arithmetical sets. In fact, it is possible to build a model of WKL0 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 ACA0 over RCA0:

Arithmetical transfinite recursion ATR0

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. ATR0 is equivalent over ACA0 to the principle of Σ1
separation. ATR0 is impredicative, and has the proof-theoretic ordinal , the supremum of that of predicative systems.

ATR0 proves the consistency of ACA0, and thus by Gödel's theorem it is strictly stronger.

The following assertions are equivalent to ATR0 over RCA0:

comprehension Π1

-CA0 is stronger than arithmetical transfinite recursion and is fully impredicative. It consists of RCA0 plus the comprehension scheme for Π1

In a sense, Π1
-CA0 comprehension is to arithmetical transfinite recursion (Σ1
separation) as ACA0 is to weak Kőnig's lemma (Σ0
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
-CA0 over RCA0:

Additional systems

Stronger Systems

Over RCA0, Π1
transfinite recursion, 0
determinacy, and the 1
Ramsey theorem are all equivalent to each other.

Over RCA0, Σ1
monotonic induction, Σ0
determinacy, and the Σ1
Ramsey theorem are all equivalent to each other.

The following are equivalent:[11][12]

The set of Π1
consequences of second-order arithmetic Z2 has the same theory as RCA0 + (schema over finite n) determinacy in the nth level of the difference hierarchy of Σ0

For a poset , let denote the topological space consisting of the filters on whose open sets are the sets of the form for some . The following statement is equivalent to over : for any countable poset , the topological space is completely metrizable iff it is regular.[14]

ω-models and β-models

Main article: Beta-model

The ω in ω-model stands for the set of non-negative integers (or finite ordinals). An ω-model is a model for a fragment of second-order arithmetic whose first-order part is the standard model of Peano arithmetic,[1] but whose second-order part may be non-standard. More precisely, an ω-model is given by a choice of subsets of . The first-order variables are interpreted in the usual way as elements of , and , have their usual meanings, while second-order variables are interpreted as elements of . There is a standard ω-model where one just takes to consist of all subsets of the integers. However, there are also other ω-models; for example, RCA0 has a minimal ω-model where consists of the recursive subsets of .

A β-model is an ω model that agrees with the standard ω-model on truth of and sentences (with parameters).

Non-ω models are also useful, especially in the proofs of conservation theorems.

See also


  1. ^ a b c d e f g h i j k l m n o p q r s t u v w Simpson, Stephen G. (2009), Subsystems of second-order arithmetic, Perspectives in Logic (2nd ed.), Cambridge University Press, doi:10.1017/CBO9780511581007, ISBN 978-0-521-88439-6, MR 2517689
  2. ^ H. Friedman, Some systems of second-order arithmetic and their use (1974), Proceedings of the International Congress of Mathematicians
  3. ^ Kohlenbach (2005).
  4. ^ a b c See Kohlenbach (2005) and Hunter (2008).
  5. ^ a b Normann & Sanders (2018).
  6. ^ Simpson (2009), p.42.
  7. ^ Simpson (2009), p. 6.
  8. ^ S. Takashi, "Reverse Mathematics and Countable Algebraic Systems". Ph.D. thesis, Tohoku University, 2016.
  9. ^ M. Fujiwara, T. Sato, "Note on total and partial functions in second-order arithmetic". In 1950 Proof Theory, Computation Theory and Related Topics, June 2015.
  10. ^ a b Hirschfeldt (2014).
  11. ^ Kołodziejczyk, Leszek; Michalewski, Henryk (2016). How unprovable is Rabin's decidability theorem?. LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science. arXiv:1508.06780.
  12. ^ Kołodziejczyk, Leszek (October 19, 2015). "Question on Decidability of S2S". FOM.
  13. ^ Montalban, Antonio; Shore, Richard (2014). "The limits of determinacy in second order arithmetic: consistency and complexity strength". Israel Journal of Mathematics. 204: 477–508. doi:10.1007/s11856-014-1117-9. S2CID 287519.
  14. ^ C. Mummert, S. G. Simpson. "Reverse mathematics and comprehension". In Bulletin of Symbolic Logic vol. 11 (2005), pp.526–533.