David Madore's WebLog: Reverse Mathematics

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]

↓Entry #0882 [older| permalink|newer] / ↓Entrée #0882 [précédente| permalien|suivante] ↓


Reverse Mathematics

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 T, but the full system can— or even this-or-that weakened system, intermediate between the core and full systems, cannot prove statement T, whereas this-or-that weakened system can), one seeks to determine the strength 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 Π11-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 “Π11-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.

Addendum (): Oh! I think I may have, through this blog entry, coined the French term mathématiques à rebours (as the translation of the entry's title). What happened is that (around ) I rewrote the English edition Wikipedia article on the subject; then I was asked in the comments to this entry whether I might also write a French version or at least suggest a title, I said I did not have the time and did not think a standard translation existed but I suggested mathématiques à rebours (comment dated ) as a possible French name (compte à rebours means countdown, and ingénierie à rebours is a more-or-less standard translation of reverse engineering); one of my blog readers at the time (Jko) started a short French version on , and the name may have become standard in this way. I offered mathématiques à rebours as a possible translation of the subject's name in my review for the Gazette des Mathématiciens (the SMF's bulletin) in 2010(?) of the second edition of Simpson's book. Since then, at least one PhD thesis with a French title and summary has used the term mathématiques à rebours for reverse mathematics.

↑Entry #0882 [older| permalink|newer] / ↑Entrée #0882 [précédente| permalien|suivante] ↑

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]