# Are the natural numbers definable in ZFC-Inf

While reading up on the incompleteness theorems on this page, I came upon the statement that the incompletess theorems hold in ZFC-Inf. According to the page ZFC-Inf is 'proof-theoretically equivalent' to standard Peano Arithmetic.
This seems odd to me. Would that not mean that we can interpret the set of natural numbers together with the Successor-, Addition- and Multiplicationfunction within ZFC-Inf? To me the Axiom of infinity exists exactly because we would have no way of defining the set of natural numbers otherwise. So is there something I am misunderstanding, or is there really a formula $$\phi_\mathbb{N}$$ in ZFC-Inf that can define a set of natural numbers (it would not be a set in the model of course), as well as formulae $$\phi_{S}, \phi_+,\phi_\times$$ that define the arithmetic functions such that the axioms of PA are satisfied?

Yes. If $$\mathfrak{M}\models\mathsf{ZF}$$-$$\mathsf{Inf}$$, the "natural numbers of $$\mathfrak{M}$$" are the things which $$\mathfrak{M}$$ thinks satisfy the following formula:

$$\nu(x):\quad$$ $$x$$ is a hereditarily transitive set and for every nonempty $$y\in x$$ there is some $$z\in x$$ such that $$y=z\cup\{z\}$$.

Informally, this says "$$x$$ is a finite ordinal." In $$\mathsf{ZF}$$-$$\mathsf{Inf}$$ alone, the standard recursive definitions of addition and multiplication of natural numbers behave as we expect. (These are tedious, though, which is why I'm omitting them; the point is that the "recursion data" witnessing any specific instance of $$+$$ or $$\times$$ is itself a finite object.)

What we can't do in this weaker framework is argue that the class defined by $$\nu$$ above is a set. But that doesn't pose an issue here.

• How do you formalize '$x$ is hereditarily transitive'? Intuitively a hereditary property needs recursion to define. Or is there some characterization of hereditary transitivity that can be described with a simple formula? Jul 25, 2023 at 19:03
• @leon.fuchsler "$x$ is transitive and every element of $x$ is transitive" does the job - this is a fun exercise (and specific to transitivity). Jul 25, 2023 at 19:09
• @leon.fuchsler But note that we do have recursion here! Infinity isn't needed for recursion, the key driver for recursion is replacement. Jul 25, 2023 at 19:41
• could you clarify in what sense we have recursion here? I would think that after we introduce a notion of $\mathbb{N}$ we can prove some recursion theorem that justifies making recursive definitions. But surely defining $\mathbb{N}$ using recursion wouldn't be justified. Unsure if I am making sense. Jul 25, 2023 at 21:06
• @leon.fuchsler: It suffices to show that every nonempty definable class of ordinals has a least element. Jul 27, 2023 at 14:58