I want to play with a fragment of constructive primitive recursive arithmetic lacking induction kind of like Robinson arithmetic. Basically the intent is to axiomize a sort of "weak natural numbers object" and to better understand what weak limits "mean."
So anyhow as terms I think you want
$$ e \mathrel{::=} x \mid \mathop{\text{S}} e \mid \text{O} \mid \mu(x. e_0, e_1, e_2) $$
And you axiomize recursion as something like
$$ \begin{align} \mu(x. e_0, e_1, \text{O}) & = e_1 \\ \mu(x. e_0, e_1, \mathop{ \text{S}} e_2) & = [x := \mu(x. e_0, e_1, e_2)]e_0 \end{align}$$
But you don't assume induction, disjoint terms or eta laws.
I think maybe you can then define an equivalence in terms of the absolute value of the difference between two numbers.
$$ m \cong n = \lvert n - m \rvert = 0 $$
And you ought to have some sort of "pseudo induction" with respect to this equivalence.
There's also a minor technical problem that first order logic lacks variable binders. So you can't really treat $\mu$ as a term without messing around a bunch. Defining $\mu$ while avoiding introducing a form of induction or a principle of unique choice would be annoying.
It's strange because I know how to build something like what I want in a prover like Coq but I don't know how to axiomize things abstractly.
Set Primitive Projections.
Inductive nat := roll {
unroll: option nat ;
}.
Eta laws cause non-termination issues here so dependent elimination is banned with inductive primitive projections in Coq. So you obtain a type of natural numbers without induction which is very weird.
Anyhow I kind of have an idea of what the category theory ought to be but I'm still very confused about how you might translate this precisely to a logical theory. Is there a pre-existing study of constructive primitive recursive arithmetic without induction sort of like Robinson arithmetic? I come from a computer science background so I'm familiar with the basics of Peano arithmetic and such but I've never really delved deeply into weaker foundations of arithmetic.