Peano structure ordering and the recursion theorem circular definitions

Question

Suppose $(P, 0, S)$ is a Peano structure. I am trying to prove the Recursion theorem* and I'm mixed up as to if the recursion theorem needs to be proven first or the order $<$ needs to be defined first. What I'm seeing is that many proofs of the Recursion theorem rely on approximations to the function $F$ called out in the theorem which have conditions that are something like "for all $m < n$ the approximation is defined by...". Such conditions then rely on $<$ already being defined.

But, for the definition of $<$ I see something like $m < n$ if there exists a $p\not = 0$ and $m+p = n$. But, as far as I know, the binary operation $+$ is defined using the recursion theorem.

So I'm curious for ways out of this circular logic.

• One way I could see is to define the $F:P\to X$ in the recursion theorem without using approximations, but as the intersection of subsets of $P\times X$ (i.e. relations) which satisfy the desired condition for the recursion theorem and whose intersection results in a genuine function. Though I haven't found a complete proof along these lines. This would be my preferred approach so if someone could point me to a reference that takes this approach it would be very appreciated
• Maybe the "approximation" approach to the Recursion theorem can be done without relying on $<$ having been defined.
• Maybe $<$ can be defined without recursively defining $+$.

Finally, if it matters, I'm working with first order logic and ZF set theory for the background language/axioms etc.

• For my case, in which I'm defining $P=\mathbb{N}$ as the minimal inductive set and the successor operation $S(n) = n \cup \{n\}$ I can define $<$ by $m < n$ if $m \in n$ or, alternatively, $m\subset n$ and this would get me out of circularity. However, such a definition is "outside the scope" of the Peano axioms. I would be surprised if there isn't a way to both prove the recursion theorem and define $<$ all within the scope of the Peano axioms.

*which states that if $X$, $f:X \to X$ and $x\in X$ that we can find an $F:P \to X$ with $f(0) = x$ and for $p\in P$ that $F(S(p)) = f(F(p))$

---

edit: I've answered this question myself below after finding another reference. However, I'm still curious if other approaches are possible, or, for example, if we should consider proofs of the recursion theorem that rely on $+$ or $<$ to in fact be incorrect proofs due to circularity.

Answer 1

In ZF set theory, the specific structure of $\mathbb{N}$ allows us to define $<$ as $\in$ (assuming we use the usual von Neumann ordinals where $0 = \emptyset$ and $s(x) = x \cup \{x\}$). So there is no circularity in using $<$.

Furthermore, we can also define transitive closures of relations without reference to natural numbers and define $<$ as the transitive closure of the relation $R = \{(x, s(x)) \mid x \in \mathbb{N}\}$. This approach requires an impredicative proof of the existence of transitive closures, so it is not my first choice. But it is also an option.

Finally, there is also the well-known “top-down” approach to proving the recursion theorem. This approach also requires some impredicativity, but it is a perfectly valid tactic in ZF.

Answer 2

Indeed, further research reveals the first bullet point is a correct approach. That is, it is possible to prove the recursion theorem in a "top down" approach by defining the intersection over a set of relations which satisfy the desired properties of the recursive function. This proof proceeds without any reference to $+$ or $<$. I found a satisfactory proof in Halmos' "Naive Set Theory" which I think is a canonical reference for this kind of thing.