论文标题
原始递归反向数学
Primitive recursive reverse mathematics
论文作者
论文摘要
我们使用二阶类比$ \ mathsf {pra}^2 $ of $ \ mathsf {pra} $来研究定理在可数代数，分析和无限组合方中的证明理论强度。我们将结果与原始递归（\ lq Punctual \ rq）代数的快速开发领域和分析进行了比较，以及\ lq Online \ rq \ combinatorics的结果。我们认为，$ \ mathsf {pra}^2 $足够坚固，可以作为$ \ mathsf {rca} _0 $的替代基本系统，以研究普通数学中定理的证明理论内容。 （最受欢迎的替代方法可能是$ \ Mathsf {rca} _0^*$。）我们发现，许多在$ \ Mathsf {rca} _0 $中以$ \ Mathsf {pra}^2 $中的定理属于$ \ Mathsf {rca} _0 $，或者等于$ \ \ nathsf {rca} _0 $或fiff teff。 $ 2^n- \ Mathsf {rca} _0 $ of $ \ mathsf {pra}^2 $。但是，我们还发现，某些标准的数学和组合事实与这些自然子系统无与伦比。
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.
