Reverse mathematics is a strange subject (AMS Mathematics Subject Classification: 03B30, 03F35) that I didn't even know existed until I stumbled upon it by chance a few days ago. It was founded by Harvey Friedman and one of its leading experts is Stephen G. Simpson. Let me try to explain briefly what it is about.

Ordinary (“forward”?) mathematics, at least from the formalist's point of view, consists essentially of the following: start with a set of axioms, which is usually the Zermelo-Fraenkel set theory (although one of the things reverse mathematics teaches us is that in fact there is no need to make such incredibly strong assumptions), and try to derive theorems from them. Reverse mathematics goes the other way around, it tries to assess the “strength” of each theorem by seeing how much of the axioms has been captured in it and can be derived back from its content. Perhaps this is a big too vague to make much sense, so I'll try to be clearer.

No mathematical proof ever makes use of the full strength of the axioms[#]. Now what happens if we restrict the system—either by omitting some axioms or by weakening them in various ways? Some theorems will cease to be theorems, and if we continue that way we lose more and more theorems until the system becomes so weak that it is essentially useless and uninteresting and the irrelevant becomes a barrier (for example, irrelevant differences in the formulation of this or that axiom might cease to be irrelevant if the other axioms are weakened too much, because the equivalence between the formulations is no longer provable). Stop somewhere before you get to that point where the system is unmanageably weak, and call the resulting set of axioms the “core system”. So far this is not rigorous, we're just setting up the framework. Everything will then be done over that core system. Many results which “used to be” theorems (they are so in the full axiom system) are no longer so in the core system. A first step toward reverse mathematics would be to show that this or that theorem (of the full system) is indeed unprovable in the core system (the fact that the usual proof requires strong axioms doesn't mean that there doesn't exist a smarter proof which could do with weaker ones).

But reverse mathematics goes farther than this: one isn't content
with giving bounds on the “logical strength” of a theorem
over the core system (such as: the core system cannot prove
statement

— or even
`T`, but the full system canthis-or-that weakened system, intermediate between the core and
full systems, cannot prove statement

), one seeks to determine the
strength `T`, whereas
this-or-that weakened system can*exactly*. Indeed, it turns out, rather surprisingly,
that over reasonable core systems, many theorems (of stronger systems)
are in fact equivalent to one another, and equivalent to a certain
reasonably formulated logical statement (an axiom or axiom scheme
which is a weakening or a subset of some axioms of the full system
omitted in the core one). When one can show that statement
`T` not only follows from a certain natural set of axioms
intermediate between the core and full systems, but also, conversely,
implies (together with the core) the axioms in question, then one can
be satisfied that one has precisely assessed the logical strength of
`T`.

*A priori* I would have very much doubted this enterprise to
be feasible. It doesn't seem to make much sense to say that, for
example, the Cantor-Bendixson theorem (every closed subset of the
reals is the union of a perfect set and a countable one) and the
statement that every countable abelian group is direct sum of a
divisible group and a reduced group (one which doesn't have any
non-trivial divisible subgroup) are equivalent—or does
it?—let alone equivalent to some logical principle. True, when
one looks closely at their classical proof, they both make a similar
use of strong transfinite recursion (the Cantor-Bendixson theorem, in
fact, was what let Cantor to discover ordinal numbers, by
transfinitely iterating the operation of taking accumulation points).
Yet reverse mathematics teaches us that these theorems are, in fact,
equivalent in some sense (over a very reasonable core theory), being
both equivalent to the so-called “principle of
Π^{1}_{1}-comprehension”.

Another exciting feature of reverse mathematics is that it gives
rise to natural undecidability statements. We know from Gödel's
theorem that there will always be undecidables (even arithmetical
ones) in a useful mathematical theory, but the canonical examples are
very contrived: Gödel's sentence, written directly, is entirely
unnatural to the mathematician, examples within set theory appeal to
large cardinal hypotheses (this is no surprise: set theory was so
*designed* to be powerful enough—and indeed far more
powerful than necessary—to contain all of classical mathematics,
so undecidable statements in set theory must be non-classical in some
sense; nor is the continuum hypothesis a good example), and standard
examples for Peano arithmetic make use of other bizarre[#2] constructions. Now reverse
mathematics gives us undecidability results where the statements are
quite natural (they are classical mathematical theorems) and only the
axioms are weakened somewhat (and not in an unnatural way).

Another strange fact is that the logical systems which appear
naturally in reverse mathematics are very few in number (compared to
the body of theorems being studied) and, for the most part, totally
ordered in strength. To start with, we need to fix a theory and core
axiom system: unfortunately, it is not really feasible[#3] to use the usual language of set
theory and some weakened form of ZF, because
ZF, as I have noted several times, is far too strong a
system, and it cannot be conveniently weakened. Harvey Friedman has
suggested using second-order arithmetic as working language (this
means that some theorems might require a little effort to code, but it
is not wholly unnatural either), and a core system called
“recursive comprehension” (RCA in
short)—weaker even than Peano's axioms (basically, as far as
arithmetic goes, it is Peano's axioms restricted to
Σ_{1}-induction) but already sufficient for making a
whole lot of sense. The full system would be “classical
analysis”, or second-order arithmetic with unrestricted
comprehension, a system much weaker than ZF but far more
than sufficient to prove just about every standard theorem that can be
formulated in the language.

It turns out that, starting with a body of theorems of all sorts of
domains of classical mathematics, from both algebra and analysis,
reverse mathematicians have found nearly all of them to fit in a
sequence of five system: from weakest to strongest, “recursive
comprehension” (the core system, in other words, those theorems
that can be proved even from that weak system of axioms), “weak
König's lemma” (a weak form of the classical lemma by Dènes
König, namely: every infinite binary tree has an infinite path),
“arithmetical comprehension” (a system essentially of the
same strength as Peano's axioms—it has the same first-order
consequences; it is also equivalent, over the core system, to the full
König's lemma), “(autonomous) arithmetical transfinite
recursion” and
“Π^{1}_{1}-comprehension” (all five
systems are weaker than classical analysis). To my mind, this is the
sign that reverse mathematics is actually hitting on something very
profound: that a great variety of theorems from very different domains
of mathematics all reduce neatly to five systems in increasing order
of strength is a significant discovery.

For the sake of completeness, I should also say a word of what
happens in the other direction: if, instead of seeking to weaken the
axioms, we strengthen them. It turns out that there is essentially
one very natural way of doing so, starting from usual
(ZF) set theory, namely, adding large cardinal
hypotheses. I will not attempt to explain what these are, let's just
say that they are certain (very large, indeed quite monstrous) sets
whose existence cannot be proven using standard axioms and which must
be postulated. Now it so happens that they also form a quite orderly
hierarchy (that the cardinals themselves are well-ordered is a
triviality, but the logical principles behind their assumptions might
not be). Here, it must be understood that a hypothesis such as
there exists a Mahlo cardinal

is not so much interesting as the
arithmetical consequences that it implies: the important fact is that
it a Mahlo cardinal *can* exist, and the consistency of the
existence of a Mahlo cardinal is an arithmetical statement, one that
deals with the ordinary integers, even though the Mahlo cardinal is
some monstrous object living in the remote recesses of the platonic
heaven, but the arithmetical statement can somehow capture and conjure
the strength of the Mahlo cardinal itself—that is a strange
philosophical idea. Of course, these axioms of unreasonable strength,
there exists (can exist) a Mahlo cardinal

, there exists (can
exist) a measurable cardinal

, let alone there exists (can
exist) a supercompact cardinal

are of no use whatsoever in
ordinary mathematics (they are far to strong, we might say), so there
is no reverse mathematics to deal with them. But they somehow lie on
the same scale (I'm sure there should be a way to make precise the
statement that the consistency of Peano's axioms lies at the level of
ε_{0} and that of Zermelo-Fraenkel set theory at the
level of the first inaccessible cardinal).

To learn more about reverse mathematics, with prerequisites even lower than the little overview I have given, I recommend Simpson's Subsystems of Second Order Arithmetic, which is wonderfully written. Anyone with a basic (first-year graduate, perhaps) course in mathematical logic should be able to read the first chapter, which gives a beautiful account of what the game is all about. Sadly, as is too often the case with specialized mathematical textbooks, it is out of print.

[#] In the case of Zermelo-Fraenkel set theory, this is not just a vague idea: the axioms of (first order) ZF are infinite in number (because of the replacement scheme) and a proof, being finite in length, can only appeal to a finite number of them. And this fact is not anecdotal: a well-known result is that ZF is “reflexive” in the sense that the full system proves the consistency of any given finite subset of the axioms—whereas Gödel's incompleteness theorem implies that it cannot prove the consistency of all of them.

[#2] One of the
all-time favorite examples is the “Kirby-Paris Hydra
theorem”. It says the following. Start with a finite tree (the
“Hydra”). At each step of the game,
“Heracles” is allowed at each step to chop off one of the
Hydra's heads, i.e., a leaf (= terminal node) from the tree. But,
when he does so, the Hydra might grow some more heads. Specifically:
from the parent node on the tree to that (neck?) where Heracles has
chopped off a head (that is, the late head's grandparent, if I may
call it that way), every subbranch (including the one from which a
head was cut of) is multiplied a certain number of times, and from the
parent of *that* head, every subbranch (including that which
has already multiplied) is also multiplied a certain number of times,
and so on down to the root. The Hydra is allowed to reproduce itself
in that way an arbitrary number of times at each step (but
*only* starting from the parent node of that from which
Heracles has cut a head, and straight down to the root, not on any
other node—for example, if Heracles cuts off a head that is
directly attached to the root, the Hydra cannot grow any head back,
and if he chops off a head two steps from the root, the Hydra can only
grow subtrees on the root which are identical to the severed branch).
The statement is then that *no matter how* (that is, in which
order) Heracles chooses to chop heads off the Hydra and *no matter
how many* subtrees the Hydra grows back at every step (even if
that number increases dramatically), Heracles will chop every head off
in finite time. This statement is true, but is not provable from
(first order) Peano's axioms; as a matter of fact, it is equivalent,
over them, to the statement of transfinite recursion over
ε_{0}, which, as we know from Gentzen, is sufficient
to prove the consistency of Peano's axioms. Another classical example
is that of Goodstein sequences, which I will not describe here. From
the reverse mathematics point of view, both the Hydra theorem and that
on Goodstein sequences are equivalent to
ε_{0}-recursion.

[#3] For those that do not like second-order arithmetic, however, there are also some results of reverse mathematics in the language of set theory. They are quite parallel to the results in second-order arithmetic, only they don't have access to the very weakest systems, so they are considered less interesting.