An introduction to reverse mathematics

March 2, 2012 | Benedict Eastaugh

In December 2011 I gave a presentation on reverse mathematics to the local logic seminar. Having neglected this site for so long, it seemed like a good idea to publish my handout from the presentation here. Here’s a teaser:

In ordinary mathematical practice, mathematicians prove theorems, reasoning from a fixed set of axioms to a logically derivable conclusion. The axioms in play are usually implicit: mathematicians are not generally in the habit of asserting at the beginning of their papers that they assume ZFC. Given a particular proof, we might reasonably ask which axioms were employed, making explicit the author’s assumptions.

Now that we have a set of axioms Γ which are sufficient to prove some theorem φ, we could further inquire whether or not they are necessary to prove the theorem, or whether a strictly weaker set of axioms would suffice. To a first approximation, reverse mathematics is the programme of discovering precisely which axioms are both necessary and sufficient to prove any given theorem of ordinary mathematics.

Expanding on this slightly, in reverse mathematics we calibrate the proof-theoretic strength of theorems of ordinary mathematics by proving equivalences between those theorems and systems of axioms in a hierarchy of known strength. This characterisation should provoke at least three immediate questions. Which hierarchy of systems? How do these equivalence proofs work? And just what is “ordinary mathematics”?

For the answers to these questions, and many more, you can read my introduction to reverse mathematics. If you notice any mistakes, please drop me a line via email or Twitter.

A note for the eagle-eyed: at one point I claim that an equivalence between ACA₀ and some statement φ would have to involve a theorem scheme, and thus cannot be formalised at the level of the object language. However, the latter does not strictly follow from the former, as ACA₀ is finitely axiomatisable. For more details on this, read Peter Smith’s handy little guide to finitely axiomatising ACA₀.