Reverse mathematics below RCA

Question

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.)

Answer 1

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 ACA₀ [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 AC^0,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.

Answer 2

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

• "Foundational and Mathematical Uses of Higher Types", Kohlenbach, http://brics.dk/RS/99/31/BRICS-RS-99-31.ps.gz

• "Gödel's functional Interpretation", Avigad and Feferman, http://www.andrew.cmu.edu/~avigad/Papers/dialect.pdf

Answer 3

It looks like there is now a paper explicitly treating such a system! Bazhenov/Fiori-Carones/Liu/Melnikov, Primitive Recursive Reverse Mathematics just appeared on the arxiv. Here are a couple key points:

• Models of their base theory, $\mathsf{PRA}^2$, are precisely pairs $(M,X)$ where $M\models\mathsf{PRA}$ and $X$ is a family of functions on $M$ closed under composition and primitive recursion and containing the constants.

• Over $\mathsf{PRA^2}$, there are two natural versions of recursive comprehension: $\mathsf{RCA_0}$ itself and the somewhat-weaker $2^\mathbb{N}$-$\mathsf{RCA_0}$. The difference is whether the objects considered belong to Baire or Cantor space.