Replacing $\mathsf{RCA}_0$ by a Weaker Base Theory

In all but section X.4 of my book [32], $\mathsf{RCA}_0$ is taken as the base theory for reverse mathematics. That is to say, reversals are stated as theorems of $\mathsf{RCA}_0$. An important research direction for the future is to replace $\mathsf{RCA}_0$ 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 $\mathsf{RCA}_0$.

A start on this has already been made. In Simpson/Smith [33] we defined $\mathsf{RCA}_0^{\textstyle{*}}$ to be the same as $\mathsf{RCA}_0$except that $\Sigma^0_1$ induction is weakened to $\Sigma^0_0$induction, and exponentiation of natural numbers is assumed. Thus $\mathsf{RCA}_0$ is equivalent to $\mathsf{RCA}_0^{\textstyle{*}}$ plus $\Sigma^0_1$ induction. It turns out that $\mathsf{RCA}_0^{\textstyle{*}}$ is conservative over $\mathsf{EFA}$ (elementary function arithmetic) for $\Pi^0_2$ sentences, just as $\mathsf{RCA}_0$ is conservative over $\mathsf{PRA}$ (primitive recursive arithmetic) for $\Pi^0_2$ sentences.

One project for the future is to redo all of the known results in reverse mathematics using $\mathsf{RCA}_0^{\textstyle{*}}$ 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 $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$, but it unclear whether $\mathsf{RCA}_0$ can be replaced by $\mathsf{RCA}_0^{\textstyle{*}}$. 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 $\Sigma^0_1$ induction over $\mathsf{RCA}_0^{\textstyle{*}}$. 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 $\Sigma^0_1$ induction over $\mathsf{RCA}_0^{\textstyle{*}}$.

A more visionary project would be to replace $\mathsf{RCA}_0^{\textstyle{*}}$ by even weaker base theories, dropping exponentiation and $\Delta^0_1$ 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.