Primitive recursive reverse mathematics

We use a second-order analogy PRA2 of PRA to investigate the proof-theoretic strength of theorems in countable algebra, analysis, and infinite combinatorics. We compare our results with similar results in the fast-developing field of primitive recursive ('punctual') algebra and analysis, and with results from 'online' combinatorics. We argue that PRA2 is sufficiently robust to serve as an alternative base system below RCA0 to study the proof-theoretic content of theorems in ordinary mathematics. (The most popular alternative is perhaps RCA*0.) We discover that many theorems that are known to be true in RCA0 either hold in PRA2 or are equivalent to RCA0 or its weaker (but natural) analogy 2N-RCA0 over PRA2. However, we also discover that some standard mathematical and combinatorial facts are incomparable with these natural subsystems.(c) 2023 Elsevier B.V. All rights reserved.