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?


1 Answer 1


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.

  • $\begingroup$ 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? $\endgroup$ Jul 25, 2023 at 19:03
  • 1
    $\begingroup$ @leon.fuchsler "$x$ is transitive and every element of $x$ is transitive" does the job - this is a fun exercise (and specific to transitivity). $\endgroup$ Jul 25, 2023 at 19:09
  • $\begingroup$ @leon.fuchsler But note that we do have recursion here! Infinity isn't needed for recursion, the key driver for recursion is replacement. $\endgroup$ Jul 25, 2023 at 19:41
  • $\begingroup$ 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. $\endgroup$ Jul 25, 2023 at 21:06
  • $\begingroup$ @leon.fuchsler: It suffices to show that every nonempty definable class of ordinals has a least element. $\endgroup$
    – tomasz
    Jul 27, 2023 at 14:58

You must log in to answer this question.

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