Proof that the elements are distinct with Peano's axioms.

Question

Consider the function successor function $s: \mathbb{N} \to \mathbb{N}$ and the Peano's axioms:

P1) $s: \mathbb{N} \to \mathbb{N}$ is injective.

P1) $\mathbb{N} \setminus s(\mathbb{N})$ has only one element. That is, there is a single natural number that is not a successor to any other. It is represented by 1.

P3) (Induction principe) If $X \subset \mathbb{N}$ is such that $1 \in X$ and, for all $n \in X$ we have $s(n) \in X$ too, then $X = \mathbb{N}$.

Defining the n-fold composition $s^n= s \underbrace{\circ \ldots \circ}_{n \quad \text{times}} s$.

I would like to just use the axioms to show that the elements of set $$A = \{1, s(1), s^2(1), \ldots, s^n(1),\ldots\}$$ are distinct two to two distinct.

Comments: My first idea was to take two elements in $A$, one with an $m$ amount of compositions and the other an $n$ amount, but that doesn't seem to make much sense as the set is infinite and I think I would have to do induction (ie, use P3) somewhere.

Another idea is to call it $A_n=\{1, s(1), s^2(1), \ldots, s^{n-1}(1)\}$. Then, $s(A_n) \cup \{1\} = A_{n+1}$ and show by P3 that each $A_n$ have all elements distincts. But I don't know how I would write the $A$ from that.

Answer 1

The Peano Axioms imply the following statement:

There is an element $0 \in \mathbb{N}$ and a function $s : \mathbb{N} \to \mathbb{N}$ such that for all sets $A$, elements $a \in A$, and functions $t : A \to A$, there exists a unique function $f : \mathbb{N} \to A$ such that $f(0) = a$ and $f \circ s = t \circ f$.

Note: I'm using $0$ as the non-successor element rather than 1. This can be viewed as a purely notational difference, but in light of notation to be introduced shortly, I think it's the more natural choice.

Proof: Suppose the Peano Axioms, and consider $A, a \in A$, and $t : A \to A$. A partial function $g : S \to A$, where $S \subseteq \mathbb{N}$, is said to be an "attempt" if (1) for all $n \in \mathbb{N}$, if $s(n) \in S$ then $n \in S$, (2) if $0 \in S$ then $g(0) = a$, and (3) for all $n \in \mathbb{N}$, if $s(n) \in S$ then $g(s(n)) = t(g(n))$.

Claim: For all $x \in \mathbb{N}$, there exists a unique $y \in A$ such that there is some attempt $g : S \to A$ for which $x \in S$ and $g(x) = y$.

Proof: we proceed by induction on $x$.

Base case: $x = 0$. Take $y = a$. We see that the attempt $g : \{0\} \to A$ defined by $g(0) = a$. And by the definition of an attempt, if $g : S \to \mathbb{N}$ is an attempt and $0 \in S$, then $g(0) = a$.

Inductive step: suppose true for $n$. Let $q$ be the unique $q$ such that there is some attempt $g : S \to A$ with $n \in S$ and $g(n) = q$. Take some such $g$. Take $y = t(q)$. Define $g' : S \cup \{s(n)\} \to A$ by $g'(k) = g(k)$ if $k \in S$, and $g'(s(n)) = t(q)$. Note that in the event that $s(n) \in S$, we see that $g(s(n)) = t(g(n)) = t(q)$, so $g'$ is well-defined. And note that for any attempt $h : R \to A$ such that $s(n) \in R$, we have $n \in R$, thus $h(n) = q$, thus $h(s(n)) = t(h(n)) = t(q)$.

Now define $f(x)$ to be the unique $y$ such that for some attempt $g : S \to A$, $x \in S$ and $g(x) = y$. Note that $f(0) = a$ and that $f \circ s = t \circ f$. Finally, suppose we had some $f' : \mathbb{N} \to A$ also satisfying $f'(0) = a$ and $f' \circ s = t \circ f'$. Then $f'$ is an attempt, so for all $n$, $f(n) = f'(n)$. $\square$

With this in mind, we make the following definition:

Suppose that $a \in A$, $t : A \to A$, and $n \in \mathbb{N}$. Let $f : \mathbb{N} \to A$ be the unique function such that $f(0) = a$ and $f \circ s = t \circ f$. We define $t^n(a)$ to be $f(n)$.

With this in mind, we can now prove

Theorem: the map $f(n) = s^n(0)$ is injective.

Proof: Consider the map $f(n) = s^n(0)$. This is the unique map satisfying $f(0) = 0$ and $f \circ s = s \circ f$. But there is also the map $1_\mathbb{N}$, defined by $1_\mathbb{N}(n) = n$, which satisfies $1_\mathbb{N}(0) = 0$ and $1_\mathbb{N} \circ s = s \circ 1_\mathbb{N}$. Therefore, $f = 1_\mathbb{N}$. And clearly, $1_\mathbb{N}$ is injective. So $f$ is injective.