Countable strict reverse mathematics

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$.