Existence of Natural Numbers as an Axiom

By natural numbers $\mathbb{N}$ I understand any set satisfying Peano axioms:

1. $0 \in \mathbb{N}$
2. $\sigma : \mathbb{N} \to \mathbb{N}$
3. $\forall n \in \mathbb{N} \; . \; \sigma(n) \neq 0$
4. $\forall n,m \in \mathbb{N} \; . \; \sigma(n) = \sigma(m) \Rightarrow n=m$
5. $\forall A \subset \mathbb{N} : \Big(0 \in A \text{ and } \forall a \in A \; . \; \sigma(a) \in A \Big) \Rightarrow A =\mathbb{N}$

In ZF existence of natural numbers $\mathbb{N}$ is deduced from the axiom infinity. The said axiom states that there exists an inductive set $X$ such that $\emptyset \in X$ and $\forall x \in X \; . \; x \cup \{ x \} \in X$ (INF).

But I don't think that the abstract inductive set $X$ is very useful by itself and what I actually want from it is a set of natural numbers. And if I don't care about exact construction of natural numbers, why not to replace axiom of infinity by the new axiom: a set of natural numbers $\mathbb{N}$ exists (NAT)?

These axioms seems to equivalent at first, as by virtue of axiom of induction $\mathbb{N}$ seems to be inductive, but the inductivity of $X$ is far more concrete than one of $\mathbb{N}$. So, the abstract natural numbers $\mathbb{N}$ can not replace $X$ from axiom of infinity. Оn the other hand I think that if I have $\mathbb{N}$, than I can define $X$ as

$$X = \bigcup_{n \in \mathbb{N}} P^n(\emptyset),$$ where $P(A) = A \cup \{ A \}$, $P^0(a) = a$ and $P^{\sigma(n)}(a) = P^{n}(P(a))$. So, assuming ZF $-$ INF we have equivalence (NAT) $\iff$ (INF) .

Am I wrong?

Are there any systems of foundations which use axiom similar to (NAT) instead of (INF)? Is (NAT) strictly weaker than (INF)? If this is not the case why not to use (NAT) instead of (INF)?

I think I have seen something like that done by type theorists, but I don't remember exact name of the theory. But, in type theory, It is better to speak about introduction and elimination rules instead of axioms.

This is a somewhat common mistake.

The axiom of infinity does not say "Oh, this is an infinite set and this is the set of natural numbers". It says "Oh, there is a Dedekind-infinite set". From the existence of such set, we can prove that there exists a set which satisfies the properties of the natural numbers as we perceive them: a linear order which is infinite, but every proper initial segment is finite (and from that we can construct the rest of the structure of the natural numbers).

The axiom of infinity does not posit that $\omega$, the least inductive set, is the set of natural numbers. This is just a factor of convenience, since $\in$ is used to model $<$ and everything is somehow fairly canonical to construct there. But nobody forces you to use that one with that particular structure.

Ultimately, the axiom of infinity simply states "There exists a Dedekind-infinite set", in the simplest possible way. If you want to state this in a more complicated way, this is also fine. And it ends up equivalent over the rest of the axioms of Zermelo–Fraenkel.

The problem is when you consider the language of set theory has only free variables and $\in$ to work with. So for more complicated constructions you may need a more complicated language, or a far more complicated axiom which includes somehow the notions of functions, first/second order interpretation of a language, etc.

Even then, you might have it worse off, since when you declare "$\bf Nat$" as some sort of constant symbol in your language, or even a predicate, it becomes a fixed set. Whereas in the usual foundation of set theory you are free to use whatever set you'd like, once you have this fixed into your language you've made a commitment to a particular set in your universe which is now the set of natural numbers.

So to some extent, it seems to me that if you "don't care which set", then the current foundations are perfect.

Outside the ZFC set theoretic, you might want to consider second/third order arithmetic, or categorical foundations which may or may not include something like ETCS.

• I understand that there are multitude of sets that can be natural numbers in ZF. So the reason why the axiom of infinity is stated as it is stated is the simplicity of the language of set theory and that Peano axioms themselves are to verbose in this language. I asked this question, because I was looking for consistent and concise way to define and prove existence of natural numbers. Peano axioms do the job for the definition, but I wanted to avoid set theoretical construction of natural numbers, and treat them more as an universal entity (this is vague). – Nik Pronko Sep 4 '18 at 16:05
• Well, the thing is that if you want to think about the natural numbers as some sort of universal object, whose underlying set is "irrelevant" you either need to abandon material set theory, where ultimately something is this set of another (and you can simply prove a theorem that it doesn't matter if it's this set of the other, so WLOG it's that one), or you need to accept that the axiom of infinity gives you exactly the tools you need to construct the natural numbers. – Asaf Karagila Sep 4 '18 at 16:10
• I have nothing against axiom of infinity. My only intention was to skip the proof by modification of the axiom. However, I wasn't sure if I'm am 'breaking' something by this modification. – Nik Pronko Sep 4 '18 at 16:21
• I'm not saying that you have something against it. I'm just saying, in material set theory, "things" are concrete. At the end of the day, you need to choose what is that object which is "the natural numbers". The best you can do to avoid it to prove theorems of the form "For every set X which has a structure Y, we can prove Z". But this too is generally proved by taking some set X, endowing it with structure Y, and proving Z. That's the whole point of constructing the natural numbers in the first place... – Asaf Karagila Sep 4 '18 at 16:24