What is the exact consistency strength of this logic of succession and recursion?

19 Views Asked by At

The logic of Succession and Recursion is extending first order logic with equality by the following:

Add primitives of $N,0,S$ standing for "Natural, Zero, Successor". Also we add primitive function symbols $\mathcal R^{f,\alpha}$ for every function symbol $f$, and constant symbol $\alpha$.

Axiomatize:

Succession axioms: $N(0) \\ \forall x: N(x) \to N(S(x)) \\ \forall x: N(x) \to S(x) \neq 0 \\ \forall x \forall y : N(x) \land N(y) \land S(x)=S(y) \to x=y$

Recursion: if $f$ is a function symbol (primitive or parameter free definable), and $\phi$ a one place predicate symbol (primitive or definable), and $\alpha$ a constant symbol (primitive or definable), then:

$$\phi(\alpha) \land \\ \forall x: \phi(x) \to \exists y: f(x)=y \land \phi(y) \\ \implies \\ \mathcal R^{f,\alpha} (0) =\alpha \land \\ \forall n (N(n) \implies \mathcal R^{f,\alpha}(S(n)) = f(\mathcal R^{f,\alpha}(n)))$$

What's the exact consistency strength of this system?