Replacing by a Weaker Base Theory

In all but section X.4 of my book [32], is taken as the base theory for reverse mathematics. That is to say, reversals are stated as theorems of . An important research direction for the future is to replace by weaker base theories. In this way we can hope to substantially broaden the scope of reverse mathematics, by obtaining reversals for many ordinary mathematical theorems which are provable in .

A start on this has already been made. In Simpson/Smith [33] we defined to be the same as except that induction is weakened to induction, and exponentiation of natural numbers is assumed. Thus is equivalent to plus induction. It turns out that is conservative over (elementary function arithmetic) for sentences, just as is conservative over (primitive recursive arithmetic) for sentences.

One project for the future is to redo all of the known results in reverse mathematics using as the base theory. The groundwork for this has already been laid, but there are some difficulties. For example, we know that Ramsey's theorem for exponent 3 is equivalent to over , but it unclear whether can be replaced by . Other problems of this nature are listed in my book [32, remark X.4.3].

Another project is to find ordinary mathematical theorems that are equivalent to induction over . Several results of this kind are already known and are mentioned in my book [32, § X.4]. For example, Hatzikiriakou [14] has shown that the well known structure theorem for finitely generated Abelian groups is equivalent to induction over .

A more visionary project would be to replace by even weaker base theories, dropping exponentiation and comprehension. One could even consider base theories that are conservative over the theory of discrete ordered rings. At the present time, almost nothing is known about this.