Natural examples of Reverse Mathematics outside classical analysis?

Question

Harvey Friedman at the 1974 ICM motivated Reverse Mathematics by the following statement:

When the theorem is proved from the right axioms, the axioms can be proved from the theorem.

Reverse Mathematics has had many successes in finding the "right axioms," but to date mainly for theorems of classical analysis, where real numbers (or equivalent infinite objects, such as sets of natural numbers) are involved. This may be partly for historical reasons, since the subject grew from the study of subsystems of second order number theory.

It seems to me that there are classical theorems in other fields that also fit the Reverse Mathematics paradigm: add a strong axiom $A$ to a weak theory $W$ and prove $A$ equivalent, over $W$, to a strong theorem $T$ of $W+A$. The example I have in mind is where $W$ is the theory of a projective plane $P$, which has three simple axioms about objects called "points" and "lines":

1. Any two points belong to a unique line.

2. Any two lines have a unique common point.

3. There exist at least four distinct points.

This $W$ is a weak theory with very few interesting theorems. But if we add to $W$ the theorem of Pappus as an axiom $A$, then results of von Staudt, Hilbert, and Hessenberg enable us to prove the theorem

$T$: The plane $P$ can be coordinatized by a field.

Conversely, if $T$ holds then we can prove $A$. This is because the Pappus axiom $A$ states that certain points lie on a line, and $A$ can be proved once we have coordinates in a field -- by computing the coordinates of the points in question and showing that they satisfy a linear equation.

There are a few variations of this result. For example, if axiom $A$ is replaced by the theorem of Desargues then the equivalent theorem $T$ of $W+A$ is that $P$ can be coordinatized by a skew field.

This leads me to the following questions. Are these results reasonable examples of Reverse Mathematics? Are there other natural examples outside analysis?

Edit (Nov 15, 2014). Many thanks to the logicians who have answered this question. It appears to me now that the term "reverse mathematics" is too narrow for what I had in mind, but I am still interested in examples of "finding the right axioms." An even more elementary example than the Pappus axiom/theorem is the Euclid's parallel axiom. It is needed to prove many theorems, e.g. Pythagorean theorem, angle sum of a triangle equals $\pi$, ... and these theorems also prove the axiom.

Answer 1

Reverse math usually means work in subsystems of arithmetic. That goes a bit beyond analysis---Simpson's book has plenty of classic results from the theory of countable groups, rings, and fields, and much of the more recent focus in the area has been countable combinatorics. But all of these are basically about sets of natural numbers and things those can code.

As a sociological matter, addressing the same question with deeply different base theories usually isn't called reverse math. For instance, one could argue that Shelah's proof of the independence of the Whitehead problem is in some sense a result in reverse math (or at least, that a stronger result showing the equivalence of the Whitehead problem with ZFC plus some additional axiom would be), but that's not how people usually use the term: determining what can be proven in extensions of ZFC is a branch of set theory, not reverse math. Similarly, there's work on what can be proven in very weak theories of arithmetic (like arithmetic with only bounded quantifiers), but that usually doesn't get called reverse math either.

So I think most people would think that those geometric aren't quite in the field called "reverse mathematics", as it's currently understood, but are closely related results which belong to the broader philosophical umbrella which spawned reverse math.

Answer 2

I agree with Henry Towsner that the terminology "reverse mathematics" is generally used only for things in or near second-order arithmetic. If, however, you're interested in situations where one tries to prove a theorem from some axioms and then show that the axiom actually follows from the theorem, regardless of whether these situations are called "reverse mathematics", then I'd point to the study of weak forms of the axiom of choice. Here the base theory is ZF (or perhaps a variant ZFA that allows atoms), the additional axioms that one considers are the axiom of choice and weakenings of it, and one tries to show that various results of ordinary (not set-theoretic) mathematics are equivalent (over ZF) to one or another of these axioms. The book "Consequences of the Axiom of Choice" by Paul Howard and Jean Rubin gives lots of examples.

Answer 3

This is mostly a comment on the proposed example of Pappian planes.

One of the aspects of the Reverse Mathematics methodology is to analyze results in their natural setting, which is then distilled to its essential parts in the hope of extracting the minimal axiomatic setting to prove the given results. So, what is the natural setting for the Pappian plane result? In other words, what is the natural background theory to state this result? It's not the theory of projective planes since "field" makes no sense there; it's also not the algebraic theory of fields since "projective plane" makes no sense there. This is a result in elementary model theory. More specifically, it is a strong mutual interpretability result:

• Every field can interpret a Pappian projective plane using coordinates. More precisely, in the language of fields, one can interpret points and lines using tuples of numbers, interpret the incidence and equality relations, and this interpretation always results in a Pappian projective plane.

• Every Pappian projective plane can interpret a field. More precisely, using three (or four?) points in a certain position, one can interpret $0$, $1$, geometric relations that define addition and multiplication of points on the line joining $0$ and $1$, and the result satisfies the field axioms.

• These two interpretations are inverses of each other in the sense that if one composes them, the outcome is an isomorphic copy of the original object.

Mutual interpretations of this kind have an important role to play in Reverse Mathematics but mostly for background theories. For example, these are used for transferring results back and forth between subsystems of second-order arithmetic, subsystems of set theory as well as other systems with different languages.

In the context of model theory, the mutual interpretation between fields and Pappian planes has little Reverse Mathematics content since the back and forth translations are purely syntactic and easily computable. (Perhaps there might be some interest in Bounded Reverse Mathematics if the translations have some non-trivial computational content.)

There are result of this type which would be more in the flavor of Reverse Mathematics. The mutual interpretation extends to Desargesian planes and division rings. Given that, Pappus's Theorem on the geometric side is equivalent to the commutativity axiom on the algebraic side. Similarly, the existence of a Fano configuration is equivalent to 1+1=0. These equivalences can be construed as "reversals" in the theory of division rings or in the theory of projective planes.