 |
| Reverse Mathemathics |
Reverse mathematics has its origins in Harvey Friedman's 1974 address to the International Congress of Mathematicians. In it Friedman asked two fundamental questions: "What are the proper axioms to use in carrying out proofs of particular theorems, or bodies of theorems, in mathematics?" and "What are those formal systems which isolate the essential properties needed to prove them?"
Reverse mathematics was developed as an attempt to answer these questions, and since 1974 many logicians (especially Friedman and Stephen Simpson) have contributed to this project.
The goal in reverse mathematics is to find the minimal collection S of set theoretic axioms which suffices to prove a given theorem T. Because Zermelo-Frankel set theory is too powerful to provide this type of delicate analysis, second order arithmetic is used as the axiomatization of set theory.
 |
| theoretic axioms |
The formal language of second order arithmetic contains the symbols +, ·, <, 0, 1, and =, as well as two types of variables: number variables (denoted by lower case letters and intended to range over natural numbers) and set variables (denoted by upper case letters and intended to range over sets of natural numbers).
In this formalization, sets of numbers are referred to using the set variables, but there are no variables that range over sets of sets of numbers. Thus, unlike Zermelo-Frankel set theory, second order arithmetic has to treat collections of sets as formal classes. One potential point of confusion concerning second order arithmetic is that despite its name, it is not a form of full second order logic.
Second order arithmetic uses first order predicate logic, but allows two distinguished kinds of variables to separate its notation for numbers from its notation for sets. Therefore, the usual tools of first order logic such as compactness and the Lowenheim-Skolem theorems apply to second order arithmetic and its subsystems. In particular, there are countable models of second order arithmetic.
 |
| Zermelo-Frankel |
The axioms for second order arithmetic fall into three categories. First, there is a finite number of axioms stating the basic relationships between +, ·, <, 0, and 1 in the natural numbers. Two examples of these axioms are that for all m, m + 0 = m and that for all m and n, m ·(n + 1) =(m ·n) + m.
Technically these axioms are exactly the noninduction axioms from Peano arithmetic. Second, there is an induction axiom for sets which says that from the assumptions that 0 is an element of X and that for all n, if n is an element of X, then n + 1 is an element of X, we can conclude that every n is an element of X. This axiom captures the fundamental inductive nature of the natural numbers.
Third, there is an infinite collection of axioms called the comprehension scheme. For each formula j(x) in the language of second order arithmetic (allowing additional free variables as parameters), there is an axiom stating that there exists a set whose members are exactly the numbers n for which j(n) holds.
 |
| comprehension scheme |
Because second order arithmetic does not allow the formation of sets of sets, these axioms do not give rise to a version of Russell's Paradox concerning the set of all sets which are not members of themselves.
The first step in analyzing a theorem T in reverse mathematics is to formalize the statement of T in second order arithmetic. This formalization can be done for most theorems in areas of mathematics that can be captured in some countable manner, such as classical geometry, number theory, real and complex analysis, countable algebra, and countable combinatorics.
However, one of the limitations of using second order arithmetic as the underlying form of set theory is that it is not well suited to formalizing theorems from subjects such as general topology that depend heavily on the twentieth-century development of abstract set theory.
 |
| countable algebra |
The second step is to find a subsystem S of second order arithmetic that is strong enough to prove T. This step often involves translating a classical proof of T into the formal system of second order arithmetic and letting S be the collection of axioms needed in the proof.
The third step is to show that T can prove each of the axioms in S over a suitably weak base theory (described below). This process of proving the axioms from the theorem is called a reversal, and it gives rise to the name reverse mathematics.
If the system S contains axioms which are too powerful then the third step may be not possible. For example, a classical proof may use more axioms than are necessary. Therefore it is not uncommon to return to the second step and to try to find a different proof of T which uses weaker axioms.
 |
| minimum collection |
The third step is then repeated to see if these weaker axioms are provable from T. Once the third step is realized, the equivalence of the theorem T with the axioms S shows that S is a minimum collection of axioms which suffices to prove T.
Because the comprehension axioms (which state that for any formula j(x), there is a set whose elements are exactly the numbers n for which j(n) holds) are the only ones which explicitly state the existence of sets, the subsystem S is often formed by restricting the types of formulas allowed in this scheme. For example, the base theory over which one typically proves the reversals is denoted RCA and is called Recursive Comprehension Axiom.
Roughly, RCA restricts the comprehension scheme to those formulas which define sets whose membership can be calculated by a finite algorithmic procedure.
 |
| algorithmic procedure |
Many of the theorems analyzed in reverse mathematics as of this writing fall into one of five categories. They are either provable in RCA or equivalent to one of four standard subsystems: WKL (which is RCA plus an axiom stating that every infinite binary branching tree has an infinite path); ACA (which allows sets to be defined by formulas that do not contain quantifiers ranging over sets, but may contain quantifiers ranging over numbers); ATR (which allows sets to be defined by transfinite recursion); and P1-CAo. (which allows sets to be defined by formulas containing arbitrarily many quantifiers ranging over numbers and at most one quantifier ranging over sets). A small number of examples do not fit neatly into these systems, but there is little evidence that this number will not grow as more theorems are analyzed.
One of the philosophical applications of reverse mathematics is that it provides a general framework for showing the necessity of impredicative methods in particular areas of mathematics. (Roughly, a set A is predicative if it can be defined as the set of all numbers satisfying a predicate for which the truth value does not depend on the existence of A.)
On the one hand, if a theorem T is equivalent to a set of axioms that contains impredicative axioms (such as P1-CAo.) then T cannot be established without the use of impredicative methods. On the other hand, if T can be proved inside a system which contains only predicative axioms (such as ACA), then this proof shows that T constitutes a piece of predicative mathematics.
 |
| predicative mathematics |
Some of the other subsystems have similar foundational connections. For example, because RCA restricts comprehension to formulas defining sets whose membership can be decided by a finite algorithmic procedure, proofs in RCA have a number of similarities to constructive proofs. However, this analogy is not perfect because most varieties of constructivism differ sharply with RCA over the treatment of induction and over the law of excluded middle.
A second philosophical application of reverse mathematics is to give a partial realization of Hilbert's program. In order to eliminate concerns over set theoretic paradoxes and to establish the consistency of infinitary methods in mathematics, Hilbert tried to find two formal systems to capture mathematical reasoning.
The first system would be foundationally secure but would only capture finitary reasoning. The second system would be large enough to encompass all of mathematics including the general methods of infinitary reasoning. His goal was to use the first system to show the consistency of the second system, thus justifying the use of infinitary methods once and for all.
 |
| formal systems |
Gödel's Second Incompleteness Theorem is widely viewed as showing that Hilbert's program cannot succeed as it was originally conceived. However, it is still possible that a reasonable fragment of mathematics could be developed within a formal system that could be shown to be relatively consistent in a finitistic formal system.
Hilbert did not provide a strict definition for his notion of finitary, but it has been argued that the system of primitive recursive arithmetic satisfies his intuitive concept. Furthermore, since primitive recursive arithmetic can prove the relative consistency of WKL, the (substantial amount of) mathematics that can be developed in WKL is finitely reducible in Hilbert's sense and provides a partial realization of Hilbert's program.
 |
| recursive arithmetic |
