[Math] Natural examples of Reverse Mathematics outside classical analysis

lo.logicprojective-geometry

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.

Best Answer

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.