By natural numbers $\mathbb{N}$ I understand any set satisfying Peano axioms:
- $0 \in \mathbb{N}$
- $\sigma : \mathbb{N} \to \mathbb{N}$
- $\forall n \in \mathbb{N} \; . \; \sigma(n) \neq 0$
- $\forall n,m \in \mathbb{N} \; . \; \sigma(n) = \sigma(m) \Rightarrow n=m$
- $\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.
Best Answer
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.