Countable strict reverse mathematics

TL;DR

This paper explores various subsystems of the elementary theory of functions in countable reverse mathematics, establishing equivalences among induction, recursion, permutation, and minimization axioms to provide multiple axiomatizations of ETF.

Contribution

It identifies and proves the equivalence of several axioms and subsystems within the elementary theory of functions, offering new foundational insights in countable reverse mathematics.

Findings

Inductions on unary, binary, and ternary functions are equivalent over COM_{fcn}.

Weak primitive recursion axiom WPRA is equivalent to PRA over COMI_{fcn}.

Permutation and minimization axioms are pairwise equivalent over PRA_{fcn}.

Abstract

We investigate subsystems $COM_{fcn}$, $COMI_{fcn}$ and $PRA_{fcn}$ of the elementary theory of functions $ETF$, the base theory for countable strict reverse mathematics. We show that inductions on any variable for unary, binary and ternary functions are pairwise equivalent over $COM_{fcn}$. We prove that weakened primitive recursion axiom $WPRA$ is equivalent to primitive recursion axiom $PRA$ over $COMI_{fcn}$. We show that permutation axiom and minimization axioms $MIN^1$, $MIN^2$, $MIN^3$ are pairwise equivalent over $PRA_{fcn}$. Thus, we present several equivalent axiomatizations of $ETF$.