# Reverse mathematics below RCA

I'm sure this is a fairly basic question, but I can't seem to find a solid answer:

My primary question is: Is there a reasonably nice subsystem of second-order arithmetic corresponding essentially to "primitive recursive comprehension?" I'm interested only in $\omega$-models - that is, I don't care about how much induction the system allows. In fact, I'd prefer it to have full induction, so that I know the weakness of the system lies squarely in its comprehension axioms. I do mean "comprehension" here: I'd like this system to be a two-sorted system, like $RCA$ itself, so e.g. $PRA$ is not what I'm looking for - although maybe it can be tweaked into a satisfactory system in an easy way?

My secondary question is: assuming a positive answer to the first question, what are some natural statements which are equivalent (over this base system) to $RCA$ (or $RCA_0$)?

(I'm almost certain this is written up nicely somewhere easily accessible, and my google-fu is simply failing me; if this is the case, and this question is therefore inappropriate for mathoverflow, please feel free to close it.)

-
I looked for something like that a while ago and didn't find much. There is such a thing in my paper arxiv.org/pdf/1110.6559v2.pdf on page 2 (with no explicit name). Note that $RCA_0$ is equivalent to what I call the Uniformization Axiom over the nameless base system there. This axiom is also known as $QF$-$AC^{00}$, quantifier-free axiom of choice. Such systems occur naturally in proof theory but $QF$-$AC^{00}$ is a standard assumption there too. – François G. Dorais Mar 29 '13 at 12:23
Interesting aside... The system often known as $RCA^*_0$ is exactly the opposite: the only thing missing to get $RCA_0$ is primitive recursion. – François G. Dorais Mar 29 '13 at 17:07
@Francois, your nameless system looks like exactly what I want. But is there any reason we need to refer to $n$-ary functions instead of using just unary functions or sets, given that there are primitive recursive pairing operators? – Noah Schweber Mar 29 '13 at 17:17
@Noah, have you seen the very last section of Simpson's book on Subsystems of Second Order Arithmetic? It might be of interest. – Ali Enayat Mar 29 '13 at 23:17
@Francois, Carl: Thanks for the answers! I wish I could accept them both. – Noah Schweber Mar 30 '13 at 20:39

Surprisingly, this kind of base system hasn't gotten much attention in the reverse mathematics literature. Note that the system $\mathsf{RCA}_0^*$ proposed by Simpson in §X.4 of Subsystems of Second Order Arithmetic is a weakening of $\mathsf{RCA}_0$ in precisely the opposite direction: namely $\mathsf{RCA}_0^*$ plus primitive recursion is equivalent to $\mathsf{RCA}_0$ [D. R. Hirschfeldt, R. A. Shore, Combinatorial principles weaker than Ramsey's theorem for pairs, JSL 72 (2007), 171–206; PDF].

I implicitly used a system like you want in A variant of Mathias forcing that preserves ACA0 [AML 51 (2012), 751–780; arXiv:1110.6559]. This is a function-based system of the form $\mathfrak{N} = (\mathbb{N},\mathcal{N}_1,\mathcal{N}_2,\ldots)$ where $\mathbb{N}$ is the underlying set and each $\mathcal{N}_k$ is a set of functions $\mathbb{N}^k\to\mathbb{N}$ which together form an algebraic clone: each $\mathcal{N}_k$ contains all the constant functions, the projections $\pi_i(x_1,\dots,x_k) = x_i,$ and if $f \in \mathcal{N}_\ell$ and $g_1,\dots,g_\ell \in \mathcal{N}_k$ then the superposition $f(g_1(x_1,\dots,x_k),\dots,g_\ell(x_1,\dots,x_k))$ belongs to $\mathcal{N}_{k}$. And this algebraic clone is closed under primitive recursion: there are distinguished $0 \in \mathbb{N}$ (zero) and $\sigma \in \mathcal{N}_{1}$ (successor) such that for any $f \in \mathcal{N}_{k-1}$ and $g \in \mathcal{N}_{k+1}$ there is a unique $h \in \mathcal{N}_k$ such that $$h(0,\bar{w}) = f(\bar{w}) \quad\text{and}\quad h(\sigma(x),\bar{w}) = g(h(x,\bar{w}),x,\bar{w})$$ for all $x, \bar{w} \in \mathbb{N}.$ Note that the uniqueness requirement on $h$ is crucial since this is the only form of induction in this system. Strangely, one needs to assume dichotomy $x \dot- y = 0 \lor y \dot- x = 0$ to avoid a few bizarre models. Over this base system, $\Delta^0_1$-comprehension boils down to what I called uniformization:

• If $f \in \mathcal{N}_{k+1}$ is such that $\forall \bar{w}\,\exists x\,{f(x,\bar{w}) = 0},$ there is a $g \in \mathcal{N}_k$ such that $\forall\bar{w}\,{f(g(\bar{w}),\bar{w}) = 0}.$

And arithmetic comprehension boils down to what I called minimization:

• For every $f \in \mathcal{N}_{k+1}$ there is a $g \in \mathcal{N}_k$ such that $\forall x,\bar{w}\,{f(x,\bar{w}) \geq f(g(\bar{w}),\bar{w})}.$

(The above description is semantic but it is straightforward to formalize the above as a multi-sorted system.)

Similar systems do appear in proof theory (as described in Carl's answer) but only a few are restricted to second-order types. Kohlenbach proposed similar systems in various places. The closest I've seen is what he called $\mathsf{PRA}^2$ in Things that can and things that cannot be done in PRA [APAL 102 (2000), 223–245; PDF]. He doesn't actually give a fully detailed description in that paper, but if you chase references you see that it is exactly as the system I described above except that closure under superposition and primitive recursion are ensured by type-2 functionals $\mathbf{S}^k_\ell:\mathcal{N}_k\times\mathcal{N}_\ell^k\to\mathcal{N}_\ell$ and $\mathbf{R}_k:\mathcal{N}_{k-1}\times\mathcal{N}_{k+1}\to\mathcal{N}_{k}$. Uniformization is equivalent to the AC0,0-qf scheme in Kohlenbach's paper. The system assumes quantifier-free induction, which is probably not stronger than the formally weaker form of induction in the system I described above.

-

There is a large family of systems that go by names such as $\text{E-}\widehat{\text{PRA}}^\omega$. These are all somewhat related to the "System T" introduced by Gödel as part of this Dialectica interpretation. These systems are function-based, rather than set-based, and they are typically axiomatized in all finite types, although it would be easy enough to limit the collection of types. But they have a "feel" very much like PRA, in that the rules for creating functions of higher types by recursion are generalizations of the primitive recursion scheme in PRA. Comprehension is usually replaced, in these function-based settings, by fragments of the axiom of choice.

One aspect of this area is that, unlike reverse mathematics where there are five big systems that are each robust against minor changes, in the context of proof theory there are many different systems (e.g. $\text{PA}^\omega$, $\text{E-PA}^{\omega}$, $\text{E-}\widehat{\text{PA}}^{\omega}$, $\text{E-}\widehat{\text{PA}}^{\omega} \mathord{\upharpoonright}$ are different systems) and the fine details make a difference in the strengths. Moreover, different authors may use different notation for the same system.

The best references I know of for these systems are the books Applied Proof Theory by Kohlenbach and Metamathematical Investigation by Troelstra. Kohlenbach's book, in particular, has one of the most clear developments I have seen. There are a few papers online that have some information, such as

-
I wish there was a map of these systems since there are so many fine details. – François G. Dorais Mar 30 '13 at 13:46