What formula of ZFC defines the set of natural numbers?

Let $\mathsf{ZFC}'$ be the extension of $\mathsf{ZFC}$ containing the constant symbol $\Bbb N$, which we take to represent the natural numbers. In order to say that $\mathsf{ZFC}'$ is a definitional extension of $\mathsf{ZFC}$ we need to find a formula $\phi$ in the language of $\mathsf{ZFC}$ with a single free variable $\upsilon$ such that $\mathsf{ZFC}\vdash\exists!\upsilon\phi$ and, for any formula $\psi$ containing $\Bbb N$, $\mathsf{ZFC}'\vdash\psi$ iff $\mathsf{ZFC}\vdash\exists!\upsilon(\phi\land\psi(\Bbb N\mapsto\upsilon))$ or equivalently $\mathsf{ZFC}\vdash \forall\upsilon(\phi\implies\psi(\Bbb N\mapsto\upsilon))$.

However, since there can be no recursive axiomatization of $\text{Th}(\Bbb N)$ - provided that $\Bbb N$ is truly the set of natural numbers - there can be no formula $\phi$ uniquely characterizing $\Bbb N$ (up to isomorphism). So either $\Bbb N$ is not the set of natural numbers, $\mathsf{ZFC}'$ is not an extension by definitions, or $\mathsf{ZFC}$ is inconsistent.


You write:

Since there can be no recursive axiomatization of $Th(\mathbb{N})$ - provided that $\mathbb{N}$ is truly the set of natural numbers - there can be no formula $\varphi$ uniquely characterizing $\mathbb{N}$ (up to isomorphism).

This is incorrect. Very broadly speaking, what we can say is that $\mathsf{ZFC}$ (being recursively axiomatizable) must not be able to settle all questions about $\varphi$. But this has nothing to do with $\mathsf{ZFC}$ proving that exactly one thing satisfying $\varphi$ exists or that thing corresponding appropriately to $\mathbb{N}$. For example, $\mathsf{ZFC}$ also proves "There is exactly one set $x$ which is $\emptyset$ iff $\mathsf{CH}$ holds and is $\{\emptyset\}$ iff $\mathsf{CH}$ fails," while not settling the question of whether this unique object is empty.

There are various senses in which $\mathbb{N}$ is "hard to pin down" and various other senses in which $\mathbb{N}$ is "easy to pin down;" you have to be very careful about which sense is being used when applying a given theorem.


I will argue that both are wrong.

First, the statement

Since there can be no recursive axiomatization of $Th(\mathbb{N})$ ... thre can be no formula $\phi$ uniquely characterizing $\mathbb{N}$ (up to isomorphism)

This is subtly wrong. There can be no first-order formula in the language of $\mathbb{N}$ where all quantifiers range over $\mathbb{N}$ which uniquely characterises $\mathbb{N}$.

But there can be a formula in the language of set theory which uniquely characterises $\mathbb{N}$. Let $\psi(v) := (\exists e . e \in v \land \forall y . \neg (y \in e)) \land \forall e . e \in v \to \exists k . k \in v \land \forall u . u \in k \iff (u = e \lor u \in e)$. Then let $\phi(v) := \psi(v) \land \forall u . \psi(u) \to \forall x . x \in v \to x \in u$. The axiom of infinity allows us to prove $\exists! v . \phi(v)$. This is what allows us to define $\mathbb{N}$ as a definitional extension.

Therefore, B is wrong. ZFC does have a notion of the "set of natural numbers" and can be definitionally extended to include such a set, as seen above.

However, A is potentially wrong in that A assumes that the set $\mathbb{N}$, defined in ZFC, has anything to do with the "actual natural numbers". If ZFC were inconsistent, then ZFC would prove statements like "$0 = 1$" (interpreted suitably in $\mathbb{N}$). Even if ZFC is consistent, how do we know that all statements it proves about $\mathbb{N}$ are actually true about the actual natural numbers? We would know that all $\Pi_1$ statements it proves about $\mathbb{N}$ actually hold, but we wouldn't necessarily know that all first-order statements proved about $\mathbb{N}$ are actually true.

If we adopt constructive logic and accept principles like "all functions are recursive", then we can actually come up with specific statements about $\mathbb{N}$ that ZFC proves (such as "for every general-recursive unary function $f$, either $f(0)$ exists or $f(0)$ does not exist") but which are not actually true about the natural numbers.