Reverse mathematics

Reverse mathematics is a branch of mathematics which could briefly be described as “going back from the theorems to the axioms” rather than the usual way (from the axioms to the theorems). A little more precisely, it tries to assess the logical strength of a whole body of usual mathematical results by determining exactly which axioms are necessary and sufficient to prove them.

The domain was founded by Harvey Friedman in his article “Some systems of second order arithmetic and their use” (Proceedings of the International Congress of Mathematicians (Vancouver, B.C., 1974), Vol. 1, pp. 235–242. Canad. Math. Congress, Montreal, Que., 1975). It was pursued, among other people, by Stephen G. Simpson and his students. Simpson wrote the reference textbook on the subject, Subsystems of Second Order Arithmetic (Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1999, ISBN 3-540-64882-8); most, if not all, of this article is taken from the introductory first chapter of Simpson's book.

Principles

Generalities

The principle of reverse mathematics is the following: one starts with a framework language and a base theory—a core (axiom) system—, which is too weak to prove most of the theorems one might be interested in, but still powerful enough to prove the equivalence of certain statements whose difference is deemed irrelevant or establish certain facts which are considered obvious enough (such as the fact that addition is commutative). Above that weak base theory there is a full theory (set of axioms) which is strong enough to prove the theorems one is interested in, and in which normal mathematical intuition is unimpaired.

Between the base and full systems the reverse mathematician seeks to mark a certain number of axiom sets of intermediate strength, which are pairwise probably non-equivalent (over the base system): each system should not only prove this or that classical theorem but should also be equivalent to it over the core system. This ensures that the logical strength of the theorem has been precisely assessed (at least for the chosen framework language and core system): weaker axioms will not suffice to prove the theorem and stronger ones will not be implied by it.

Choice of the language and base system

If the base system is chosen too strong (as an extreme case, take it to be full Zermelo-Fraenkel set theory), then reverse mathematics is uniformative: many theorems (of the full system, that is, usual mathematical theorems) will actually be theorems of this core system, so they are all equivalent and we learn nothing about their strength. If the base system is chosen too weak (as an extreme case, take it to be mere predicate calculus), then the equivalence relation between theorems is overfussy: nothing is ever equivalent to anything except when it is trivially so, and we also learn nothing. There is also the question of how to choose the framework language: it should be sufficient to express usual mathematical ideas without too much translation, yet it should not presuppose strong axioms otherwise we again run into the trouble of the core system being too strong.

For example, while usual (forward) mathematics is done in the language of set theory and in the system of Zermelo-Fraenkel set theory (which, unless the contrary is explicitly stated, is assumed to be the foundation system taken for granted by working mathematicians), this system is really much stronger than is necessary—this is one of the lessons of reverse mathematics. Although certain results of reverse mathematics can be stated in the framework of set theory, it is usually not well suited, because it presupposes too strong assumptions (such as the existence of sets of arbitrary rank and the uniformity of construction across them).

In the current embodiment of reverse mathematics, following Friedman, Simpson and others, the framework language is (usually) taken to be second order arithmetic and the core theory, recursive comprehension, whereas the full theory would be classical analysis. We must now say a word about these.

Second order arithmetic

This section is somewhat technical and tries to describe precisely the usual framework for reverse mathematics (namely, subsystems of second order arithmetic).

The Language

The language of second order arithmetic is a two-kinded language (of (first order) predicate calculus): certain terms and variables (usually written in lower case) refer to individuals/numbers (thought of to be natural numbers) and certain variables (usually written in upper case) refer to classes/predicates/properties (thought of to be sets of natural numbers) of individuals. Both individuals and predicates can be quantified (universally or existentially), but a formula which has no bound class variables (though it may have free class variables and bound individual variables) is known as arithmetical.

Individual terms can be formed by the constant 0, the unary function S (successor function) and the binary operations + and · (addition and multiplication). The relations = (equality) and < (comparison of natural numbers) relate two individuals, whereas the relation ∈ (membership) relates an individual and a class.

For example $\forall n(n\in X\rightarrow Sn\in X)$ is a well-formed formula of second-order arithmetic which is arithmetical, which has one free class variable X and one bound individual variable n (but no bound class variables, as is required of an arithmetical formula), whereas $\exists X\forall n(n\in X\leftrightarrow n<SSSSSS0\cdot SSSSSSS0)$ is a well-formed formula which is not arithmetical with one bound class variable X and one bound individual variable n.

Coding mathematics in second order arithmetic

Second order arithmetic allows us to speak directly (without coding) of natural numbers and sets of natural numbers. Pairs of natural numbers can be coded in the usual way as natural numbers, so arbitrary integers or rational numbers are first-class citizens in the same manner as natural numbers. Functions between these sets can be encoded as sets of pairs, so as subsets of the natural numbers, without difficulty. Real numbers can be defined as Cauchy sequences of rational numbers, but for technical reasons which we will not go into (in the weak axiom systems) it is preferable to put an actual constraint on the convergence rate (say, asking that the distance between the n-th and (n+1)-th term is less than 2⁻ⁿ). Real functions, or subsets of the reals, cannot be spoken of directly in the system, but continuous real functions are legitimate objects of study since they are defined by their values on the rationals, and by a similar trick it is possible to speak, for example, of open subsets of the reals. Even Borel sets of reals can be coded in the language of second order arithmetic (though it is a bit tricky).

Basic axioms

The following axioms are known as the basic axioms, or sometimes the Robinson axioms because they essentially define Robinson arithmetic, and they will always be assumed:

• $\forall m(Sm=0\rightarrow \bot )$ (“the successor of a natural number is never zero”)
• $\forall m\forall n(Sm=Sn\rightarrow m=n)$ (“the successor function is injective”)
• $\forall n(0=n\lor \exists m(Sm=n))$ (“every natural number is zero or a successor”)
• $\forall m(m+0=m)$
• $\forall m\forall n(m+Sn=S(m+n))$
• $\forall m(m\cdot 0=0)$
• $\forall m\forall n(m\cdot Sn=(m\cdot n)+m)$
• $\forall m(m<0\rightarrow \bot )$
• $\forall m(m<Sn\leftrightarrow (m<n\lor m=n))$
• $\forall n(0=n\lor 0<n)$
• $\forall m\forall n((Sm<n\lor Sm=n)\leftrightarrow m=n)$

Note that all these axioms are first order (that is involve no class variables at all, something even stronger than being arithmetical). The first three, together with mathematical induction, form the usual Peano axioms (the third, actuall, is a consequence of even the weakest induction schemes), whereas the subsequent axioms are a definition of addition, multiplication and order on the natural numbers (again, the last two are redudant as soon as any kind of induction axiom is added).

Induction and comprehension axioms

All the systems considered will include the basic axioms defined above.

If φ(n) is a formula of second order arithmetic with a free individual variable n and possible other free individual or class variables (written m_• and X_•), the induction axiom for φ is the axiom:

$\forall m_{\bullet }\forall X_{\bullet }(\varphi (0)\rightarrow \forall n(\varphi (n)\rightarrow \varphi (Sn))\rightarrow \forall n(\varphi (n)))$

One particularly important instance of this axiom is when φ is the formula “n∈X” expressing the fact that n is a member of X (X being a free class variable): in this case, the induction axiom for φ becomes

$\forall X(0\in X\rightarrow \forall n(n\in X\rightarrow Sn\in X)\rightarrow \forall n(n\in X))$

We shall call the latter the “ordinary second-order induction axiom”.

Returning to the case where φ(n) is a formula with a free variable n and possibly other free variables, we define the comprehension axiom for φ to be:

$\forall m_{\bullet }\forall X_{\bullet }\exists Z\forall n(n\in Z\leftrightarrow \varphi (n))$

Essentially, this allows us to form the set $Z=\{n|\varphi (n)\}$ of natural numbers satisfying φ(n).

The full system

The full second order arithmetic, also known as classical analysis is the axiom system (for the language of second order arithmetic) consisting of the basic axioms, plus the unrestricted comprehension axiom scheme, in other words the comprehension axiom for every formula φ, arithmetic or otherwise, and the ordinary second-order induction axiom (in the presence of the unrestricted comprehension axiom scheme, it is easy to see that it makes no difference whether to include the unrestricted induction axiom scheme, in other words the induction axiom for every formula φ, or merely the ordinary second-order induction axiom as defined above).

Although it is much weaker than Zermelo-Fraenkel set theory, classical analysis is already a very strong axiom system, much more than is needed to do essentially all of classical mathematics that can be encoded in the framework language of second-order arithmetic.

Arithmetical comprehension

Arithmetical comprehension is more restricted than full second-order arithmetic. It is defined as the axiom system consisting of the basic axioms, plus the arithmetical comprehension axiom scheme, in other words the comprehension axiom for every arithmetical formula φ, and the ordinary second-order induction axiom; again, we could also choose to include the arithmetical induction axiom scheme, in other words the induction axiom for every arithmetical formula φ, without making a difference.

This system is closely related to first-order arithmetic (or first-order Peano axioms), defined as the basic axioms, plus the first order induction axiom scheme (for all formulas φ involving no class variables at all, bound or otherwise), in the language of first order arithmetic (which does not permit class variables at all).

The arithmetical hierarchy for formulas

To define the following system, we will need a bit more terminology.

A formula is called bounded arithmetical, or Δ₀, when all its quantifiers are of the form ∀n<t or ∃n<t (where n is the individual variable being quantified and t is an individual term), where $\forall n<t(\cdots )$ stands for $\forall n(n<t\rightarrow \cdots )$ and $\exists n<t(\cdots )$ stands for $\exists n(n<t\land \cdots )$.

A formula is called Σ₁ (or, more accurately, Σ⁰₁), respectively Π₁ (or, more accurately, Π⁰₁) when it of the form ∃m_•(φ), respectively ∀m_•(φ) where φ is a bounded arithmetical formula and m is an individual variable (that is free in φ). More generally, a formula is called Σ_n, respectively Π_n when it is obtained by adding existential, respectively universal, individual quantifiers to a Π_n−1, respectively Σ_n−1 formula (and Σ₀ and Π₀ are all equivalent to Δ₀). Note that by construction all these formulas are arithmetical (no class variables are ever bound) and, in fact, by putting the formula in Skolem prenex form one can see that every arithmetical formula is equivalent to a Σ_n or Π_n formula for all large enough n.

The base system

Recursive comprehension is an even more restricted system than arithmetical comprehension. It consists of: the basic axioms, plus the Σ₁ induction scheme and Δ₁ comprehension. The former term is clear: the Σ₁ induction scheme is the induction axiom for every Σ₁ formula φ. The term “Δ₁ comprehension” requires a little more explaining, however: there is no such thing as a Δ₁ formula (the intended meaning is a formula which is both Σ₁ and Π₁), but we are instead postulating the comprehension axiom for every Σ₁ formula subject to the condition that it is equivalent to a Π₁ formula, in other words, for every Σ₁ formula φ and every Π₁ formula ψ we postulate

$\forall m_{\bullet }\forall X_{\bullet }((\forall n(\varphi (n)\leftrightarrow \psi (n)))\rightarrow \exists Z\forall n(n\in Z\leftrightarrow \varphi (n)))$

Recursive comprehension is usually taken as the base system when doing reverse mathematics. Sometimes, however, an even weaker system is desired. One possible candidate is defined as follows: one must first augment the language of arithmetic with an exponential function (in stronger systems the exponential can be defined in terms of addition and multiplication by the usual trick, but when the system becomes too weak this is no longer possible) and the basic axioms by the obvious axioms defining exponentiation inductively from multiplication; then the system consists of the (enriched) basic axioms, plus Δ₁ comprehension plus Δ₀ induction.

Stronger systems

Much as we have defined Σ_n and Π_n (or, more accurately, Σ⁰_n and Π⁰_n) formulae, we can define Σ¹_n and Π¹_n formulae in the following way: a Δ¹₀ (or Σ¹₀ or Π¹₀) formula is just an arithmetical formula, and a Σ¹_n, respectively Π¹_n, formula is obtained by adding existential, respectively universal, class quantifiers in front of a Π¹_n−1, respectively Σ¹_n−1.

It is not too hard to see that over a not too weak system, any formula of second order arithmetic is equivalent to a Σ¹_n or Π¹_n formula for all large enough n. The system Π¹₁-comprehension is the system consisting of the basic axioms, plus the ordinary second-order induction axiom and the comprehension axiom for every Π¹₁ formula φ. It is an easy exercise to show that this is actually equivalent to Σ¹₁-comprehension (on the other hand, Δ¹₁-comprehension, defined by the same trick as introduced earlier for Δ⁰₁ comprehension, is actually weaker).

Models of second order arithmetic

A model of the language of second order arithmetic is a set M (which forms the range of individual variables) together with a constant 0 (an element of M), a function S from M to M, two binary operations + and · on M, a binary relation < on M, and a set of subsets of M which form the range of class variables. By omitting the latter we obtain a model of the language of first order arithmetic. When the set of subsets of M is the full powerset of M, we speak if a full model. When M is the usual set of natural numbers with its usual operations, we say that M is an ω-model (in which case we can choose to call “the model” the set of sets of natural which is the only interesting part of the structure).

The only full ω-model, in other words the usual set of natural numbers with its usual structure and all its subsets, is called the intended model of second-order arithmetic. Evidently it satisfies the full axiom system (classical analysis).

It is not too hard to concoct some other models of weaker systems. For example, the ω-model consisting of (the usual natural numbers together with) the set of recursive sets of natural numbers is an ω-model of recursive comprehension (in fact, the smallest one) which is not a model of arithmetical comprehension. The ω-model consisting of the set of arithmetical sets of natural numbers (i.e., those definable in first order arithmetic, or, equivalently, which can be obtained by a finite number of iterations of the Turing jump) is a model of arithmetical comprehension.

The main systems

We now attempt to describe, with less technicalities (and perhaps slightly more handwaving), what the main formal systems of reverse mathematics are. It turns out that, in the framework language of second order arithmetic, and over the core system of recursive comprehension (as defined in the previous section), a considerable variety of classical mathematical theorems are equivalent to one of the following five main subsystems of second-order arithmetic: in order of increasing strength: recursive comprehension (the base system), weak König's lemma, arithmetical comprehension, (autonomous) arithmetical transfinite recursion, and Π¹₁-comprehension.

Recursive comprehension

Recursive comprehension serves as our core system, so to state that a theorem is “equivalent” to recursive comprehension merely means that it is provable even in that weak system.

Intuitively, recursive comprehension is a constructivist system. One must imagine that it proves theorems which remain valid in the context of recursive functions and subsets of the integers (as was pointed out earlier, the recursive subsets of the natural numbers form an ω-model of recursive comprehension). This is a very strong limitation the allowed proof means (for example, recursive comprehension is not sufficient to prove König's lemma as described in the next subsection).

Despite its weakness, recursive comprehension is still sufficient to prove a number of classical results which are, therefore, “core mathematical statements” requiring only minimal logical strength (and, in a sense, below the reach of the reverse mathematics enterprise). Let us state:

• Basic properties of the natural numbers, integers, and rational numbers (for example, 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 have an intersection point, and consequently the real numbers are uncountable).
• The Baire category theorem in a complete separable metric space (the separability condition is necessary to even code the theorem in the language of second order arithmetic).
• The intermediate value theorem on continuous real functions.
• The Banach-Steinhaus theorem for a sequence of continuous linear operators on separable Banach spaces.
• A weak version of Gödel's completeness theorem (for a set of sentences, in a countable language, that is already closed under consequence).
• The existence of an algebraic closure for a countable field (but not its uniqueness!).
• The existence and uniqueness of the real closure of a countable ordered field.

The first order part of recursive comprehension (in other words, theorems of the system which do not involve any class variables) is the set of theorems of first order Peano arithmetic with induction limited to Σ₁ formulae. It is provably consistent, and so is recursive comprehension, in the full first-order Peano arithmetic.

Weak König's lemma

We add to recursive comprehension 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. It is easy to encode this statement in the language of second order arithmetic. We call the resulting system weak König's lemma. It can also be defined as the principle of Σ⁰₁ separation (given two Σ⁰₁ formulae of a free variable n which are exclusive, there is a class containing all n satisfying the one but none of the other).

In a sense, weak König's lemma is already 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). At any rate, it is no longer a constructivist system.

To see that weak König's lemma is actually stronger than (not provable in) recursive comprehension, it is sufficient to exhibit a recursive counterexample, which is not difficult (take a set of recursively inseparable recursively enumerable sets of natural numbers). It turns out, however, that recursive comprehension and weak König's lemma have the same first order part. But weak König's lemma is useful for proving a good number of classical mathematical results which do not follow for recursive comprehension alone.

The following results are equivalent, over recursive comprehension, to weak König's lemma:

• 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 a finite product of copies of the closed unit interval).
• The separable Hahn-Banach theorem in the form: a bounded linear form on a subspace of a separable Banach space extends to a bounded linear form on the whole space.
• Gödel's completeness theorem (for a countable language).
• Every countable commutative ring has a prime ideal.
• Every countable formally real field is orderable.
• Uniqueness of algebraic closure (for a countable field).

Arithmetical comprehension

Arithmetical comprehension is the comprehension axiom scheme for arithmetical formulae: that is, it allows us to form the set of natural numbers satisfying an arbitrary arithmetical formula (one with no bound class variables). Actually, over recursive comprehension, it suffices to postulate comprehension for Σ₁ formulae to obtain full arithmetical comprehension.

The first order part of arithmetical comprehension turns out to be exactly first order Peano arithmetic: one says that arithmetical comprehension is a conservative extension of first order Peano arithmetic. It is provably (in a weak system) equiconsistent with it. Arithmetical comprehension can be thought of as the framework of predicative mathematics. Seemingly every natural arithmetical result, and many other mathematical theorems, can be proven in this system.

As for reverse mathematics, the following assertions are equivalent, over recursive comprehension, to arithmetical comprehension:

• The sequential completeness of the real numbers (every bounded increasing sequence of real numbers has a limit).
• The Bolzano-Weierstraß theorem.
• Ascoli's theorem: every bounded equicontinuous sequence of real functions on the unit interval has a uniformly convergent subsequence.
• Every countable commutative ring has a maximal ideal.
• Every countable vector space over the rationals (or over any countable field) has a basis.
• Every countable field has a transcendence basis.
• The full König's lemma (as opposed to the weak version described above).
• Various theorems in combinatorics, such as certain forms of Ramsey's theorem.

Arithmetical transfinite recursion

Arithmetical transfinite recursion is, loosely speaking, the statement that an arithmetical operator (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 applied transfinitely along any countable well ordering (a total countable order with no decreasing sequence). It can also be defined as the principle of Σ¹₁ separation.

Arithmetical transfinite recursion proves the consistency of arithmetical comprehension, so by Gödel's theorem it is strictly stronger.

The following assertions are equivalent, over recursive comprehension, to arithmetical transfinite recursion:

• Any two countable well orderings are comparable.
• Ulm's theorem for countable reduced Abelian groups.
• The perfect set theorem.
• Lusin's separation theorem (essentially Σ¹₁ separation).
• Open determinacy in the Baire space.

Π¹₁-comprehension

The principle of Π¹₁ comprehension is stronger than arithmetical transfinite recursion, and it is fully imprecative. In a sense, Π¹₁-comprehension is to arithmetical transfinite recursion (Σ¹₁ separation) as arithmetical comprehension is to weak König's lemma (Σ⁰₁ separation). It is essentially equivalent to statements of descriptive set theory that make use of strongly imprecative arguments.

Among the theorems of classical analysis equivalent, over recursive comprehension, to Π¹₁-comprehension, let us mention:

• The Cantor-Bendixson theorem (every closed set of reals is the union of a perfect set and a countable set).
• Every Abelian group is the direct sum of a divisible group and a reduced group.

Some further systems

Weaker systems than recursive comprehension can be defined. Over such a weak system as elementary function arithmetic (the basic axioms plus Δ₀ induction in the enriched language with an exponential operation) plus Δ₁ comprehension, recursive comprehension as defined earlier (that is, with Σ₁ induction) can be shown to be equivalent to the statement that a polynomial (over a countable field) has only finitely many roots, or to the classification theorem for finitely generated Abelian groups.

Weak weak König's lemma is the statement that a subtree of the infinite binary tee having no infinite paths has an asymptotically vanishing proportion of the leaves at length n. It is equivalent, for example, to the statement that if the unit real interval is covered by a sequence of intervals then the sum of their lengths is at least one.

Δ¹₁-comprehension is in certain ways to arithmetical transfinite recursion as recursive comprehension is to weak König's lemma. It has the hyperarithmetical sets as minimal ω-model. Arithmetical transfinite recursion proves Δ¹₁-comprehension but not the other way around.

Σ¹₁-choice is (over arithmetical comprehension) the statement that if η is a Σ¹₁ property of a natural number n and a class X (or real number, perhaps) such that for each n there exists X satisfying η then there is a sequence (of classes, or real numbers) satisfying the property. Σ¹₁-choice also has the hyperarithmetical sets as minimal ω-model. Arithmetical transfinite recursion proves Σ¹₁-choice but not the other way around.

An example of a reverse mathematical proof

As an example of the theory, let us sketch the proof of the fact that the Bolzano-Weierstraß theorem (in the form: every bounded sequence of real numbers has a convergent subsequence) is equivalent over recursive comprehension to arithmetical comprehension. We define a “real number” to be a sequence of rationals such that the difference between the n-th and (n+1)-th terms is less than 2⁻ⁿ.

For the forward direction (proving Bolzano-Weierstraß from arithmetical comprehension), we proceed by dichotomy as usual. For definiteness, assume the sequence is bounded between 0 and 1. For each n, divide the interval in 2⁻ⁿ subintervals of equal lengths, and consider the first of these for which infinitely many terms of the sequence lie in the subinterval: defining this requires arithmetical comprehension (because of the “for infinitely many terms”). Then take the subsequence formed by the first element from each the selected nested subintervals.

(Note: it may appear at first sight that weak König's lemma should suffice, because the nested intervals form a binary tree like in the hypothesis of weak König's lemma and we are taking an finite branch. But the tree consisting of those binary intervals containing an element of the sequence requires arithmetical comprehension to define.)

For the reverse, the idea is as follows: to prove arithmetical comprehension it is actually sufficient to prove Σ₁ comprehension (because that allows us to remove a quantifier, and we then use induction on the number of quantifiers since we can certainly pass to the complement). Now this means essentially that given a Δ₀ predicate θ(m,n) we need to prove comprehension for the predicate ∃m(θ(m,n)). But we can at least form the predicate ∃m<k(θ(m,n)) for all k. Considering this as the binary (or perhaps ternary, to avoid problems with non-uniqueness of binary expansions) expansion (letting n vary) for a real number x_k between 0 and 1 (our definition of real numbers is essentially by binary expansion), we get a nondecreasing bounded sequence which, by Bolzano-Weierstraß, converges to some real number x_∞ whose binary expansion is exactly the desired predicate ∃m(θ(m,n)). This suffices for what we want.