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.


2 Answers 2


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.

  • $\begingroup$ I'm not familiar with the transitive closure yet. Regarding "impredicativity" of the "top down" approach: Do you say that this approach has some impredicativity because it requires you to define a superset of the function $F$ from which $F$ is extracted rather than defining $F$ "directly"? $\endgroup$
    – Jagerber48
    Dec 29, 2022 at 2:22
  • $\begingroup$ Impredicativity means we are defining a kind of thing by referring to all things of that type, including the thing we define. Here, we would define the transitive closure as the smallest transitive relation containing $R$. There are some versions of set theory which don’t let you do this because they don’t include the axiom of power sets or the axiom scheme of separation. The top-down approach is similarly impredicative - we define $F$ to be the smallest subset of $P \times X$ containing $(0, x)$ and closed under $(n, w) \mapsto (s(n), f(w))$. $\endgroup$ Dec 29, 2022 at 2:52
  • $\begingroup$ I think I've decided I'm ok with impredicativity as long as the definition of $F$ doesn't involve $F$ directly. That is (at least until the recursion theorem is proved) something like $n! = n \times (n-1)!$ is unacceptable, but defining $\cdot !$ as the function resulting from the recursion theorem is ok, even if the factorial function is extracted "impredicatively" from a larger collection of relations. $\endgroup$
    – Jagerber48
    Dec 29, 2022 at 16:26

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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .