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

The program was founded by Harvey Friedman and brought forward by Steve Simpson.

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 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 RCA<sub>0</sub>, 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.

Due to the richer language of higher-order arithmetic, the use of representations (also known as '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. For instance, the base theory of higher-order reverse mathematics, called RCA, proves the same sentences as RCA<sub>0</sub>, 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 WKL<sub>0</sub> 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. 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.

Steve Simpson 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 RCA<sub>0</sub>, WKL<sub>0</sub>, ACA<sub>0</sub>, ATR<sub>0</sub>, and Π-CA<sub>0</sub>.

The following table summarizes the "big five" systems and lists the counterpart systems in higher-order arithmetic.

The <math>\Sigma_1^0 </math>-induction axiom scheme states<math display="block">\quad \big[ \varphi(0) \land \forall x \big( \varphi(x) \to \varphi(x+1) \big) \big] \to \forall x\ \varphi (x)</math>for all <math>\Sigma_1^0</math>-formulas <math>\varphi</math> that do not quantify over set variables. More explicitly, these are formulas of the form <math display="block">\exists x_1\exists x_2\cdots \exists x_n \phi</math>where <math>\phi</math> is a <math>\Delta_0^0 </math>-formula that can include set variables. In words, <math>\varphi</math> is obtained by starting with a quantifier-free formula that can involve both first-order and second-order variables, then adding bounded quantifiers over the first-order variables, and finally adding existential quantifiers over the first-order variables.

The <math>\Delta_1^0 </math>-comprehension axiom scheme states that <math display="block">\forall n [\psi(n) \leftrightarrow\varphi(n) ]\to \exists X \forall n [n \in X \leftrightarrow \varphi(n)]</math>for all <math>\Pi_1^0</math>-formulas <math>\psi</math> and all <math>\Sigma_1^0</math>-formulas <math>\varphi</math>.

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

In first-order arithmetic, WKL<sub>0</sub> is more easily defined by adding the axiom scheme of &Sigma;-separation: given two &Sigma; 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. In symbols:<math display="block">\forall n \neg [\varphi(n) \and \psi(n)] \to \exists X \forall n[(\varphi(n) \to n \in X) \and (\psi(n) \to n \not\in X)] </math>for all <math>\Sigma_1^0</math>-formulas <math>\varphi, \psi</math>.

The terminology is somewhat confusing, as the weak Kőnig's lemma itself, as an axiom scheme, is also written as WKL, whereas WKL<sub>0</sub> stands for a system, not a variant of the WKL axiom scheme.

(The first-order part of RCA<sub>0</sub>) + (<math>\Delta_0^0</math>-comprehension) + (<math>\Sigma_1^0</math>-separation) together implies (<math>\Delta_1^0

</math>-comprehension).

To show that WKL<sub>0</sub> is actually stronger than (not provable in) RCA<sub>0</sub>, note that WKL<sub>0</sub> implies the existence of separating sets for computationally inseparable recursively enumerable sets. In particular, one can simply write down two <math>\Sigma_1^0</math>-formulas <math>\varphi, \psi</math> that define such two sets, then WKL<sub>0</sub> proves that there exists some <math>X </math> that separates them, whereas the standard model of RCA<sub>0</sub> contains only computable sets, and therefore there does not exist such a separating set.

It turns out that RCA<sub>0</sub> and WKL<sub>0</sub> have the same first-order part, meaning that they prove the same first-order sentences. WKL<sub>0</sub> can prove a good number of classical mathematical results that do not follow from RCA<sub>0</sub>, 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 WKL<sub>0</sub> over RCA<sub>0</sub>:

  • The Heine–Borel theorem for the closed unit real interval, in the following sense: every covering by a sequence of open intervals has a finite subcovering.
  • The Heine–Borel theorem for complete totally bounded separable metric spaces (where covering is by a sequence of open balls).
  • A continuous real function on the closed unit interval (or on any compact separable metric space, as above) is bounded (or: bounded and reaches its bounds).
  • A continuous real function on the closed unit interval can be uniformly approximated by polynomials (with rational coefficients).
  • A continuous real function on the closed unit interval is uniformly continuous.
  • A continuous real function on the closed unit interval is Riemann integrable.
  • The Brouwer fixed point theorem (for continuous functions on an n-simplex).

Arithmetical comprehension ACA<sub>0</sub>

The system ACA<sub>0</sub> adds to RCA<sub>0</sub> the comprehension scheme for arithmetical formulas, also called the arithmetical comprehension axiom (though it is an axiom scheme). That is, ACA<sub>0</sub> 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).<sup>p.40</sup>

  • Any partial function can be extended to a total function.<!-- This source says ACA, but it looks like the schema and not the version of ACA_0 with second-order induction -->
  • Higman's lemma.
  • (schema) Π consequences of Π-CA<sub>0</sub>
  • RCA<sub>0</sub> + (schema over finite n) determinacy in the nth level of the difference hierarchy of Σ sets
  • RCA<sub>0</sub> + {τ: τ is a true S2S sentence}

The set of Π consequences of second-order arithmetic Z<sub>2</sub> has the same theory as RCA<sub>0</sub> + (schema over finite n) determinacy in the nth level of the difference hierarchy of Σ sets.

For a poset P, let MF(P) denote the topological space consisting of the filters on P whose open sets are the sets of the form for some . The following statement is equivalent to <math>\Pi^1_2\mathsf{-CA}_0</math> over <math>\Pi^1_1\mathsf{-CA}_0</math>: for any countable poset P, the topological space MF(P) is completely metrizable iff it is regular.

&omega;-models and &beta;-models

The &omega; in &omega;-model stands for the set of non-negative integers (or finite ordinals). An &omega;-model is a model for a fragment of second-order arithmetic whose first-order part is the standard model of Peano arithmetic, It involves classifying theorems into 4 main systems: BISH (Bishop-style constructive mathematics), CLASS, INT, and RUSS.

See also

  • Induction, bounding and least number principles
  • Ordinal analysis

References

References/Further Reading

  • Stephen G. Simpson's home page
  • Reverse Mathematics Zoo