Primitive recursive reverse mathematics

TL;DR

This paper explores the proof-theoretic strength of theorems in countable algebra, analysis, and combinatorics using a second-order system $ extsf{PRA}^2$, revealing its robustness and limitations compared to classical systems.

Contribution

It introduces and analyzes $ extsf{PRA}^2$ as an alternative base system below $ extsf{RCA}_0$ for studying proof-theoretic content of mathematical theorems.

Findings

Many theorems in $ extsf{RCA}_0$ hold or are equivalent to weaker systems over $ extsf{PRA}^2$.

Some mathematical and combinatorial facts are incomparable with these subsystems.

$ extsf{PRA}^2$ is shown to be a robust yet nuanced base system for reverse mathematics.

Abstract

We use a second-order analogy $\mathsf{PRA}^2$ of $\mathsf{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 (\lq punctual\rq) algebra and analysis, and with results from \lq online\rq\ combinatorics. We argue that $\mathsf{PRA}^2$ is sufficiently robust to serve as an alternative base system below $\mathsf{RCA}_0$ to study the proof-theoretic content of theorems in ordinary mathematics. (The most popular alternative is perhaps $\mathsf{RCA}_0^*$.) We discover that many theorems that are known to be true in $\mathsf{RCA}_0$ either hold in $\mathsf{PRA}^2$ or are equivalent to $\mathsf{RCA}_0$ or its weaker (but natural) analogy $2^N-\mathsf{RCA}_0$ over $\mathsf{PRA}^2$. However, we also discover that some standard mathematical and combinatorial facts are incomparable with these natural subsystems.