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.

Automated summary

This study investigates the proof-theoretic strength of theorems in countable algebra, analysis, and infinite combinatorics using the second-order analogy PRA2 of PRA, and compares the results with similar studies in primitive recursive algebra and analysis, as well as combinatorics. The researchers argue that PRA2 is robust enough to be an alternative base system for studying the proof-theoretic content of theorems in ordinary mathematics. The study discovers that many theorems known to be true in RCA0 also hold in PRA2 or are equivalent to RCA0 or its weaker analogy 2N-RCA0 over PRA2, but some standard mathematical and combinatorial facts are incomparable with these natural subsystems.