Defining Addition of Natural Numbers as the Algebra of ‘Push-Along’ Functions

Let $$N$$ be a set containing an element $$1$$ and $$\sigma: N \to N$$ an injective function satisfying the following two properties:

$$\tag 1 1 \notin \sigma(N)$$

$$\tag 2 (\forall M \subset N) \;\text{If } [\; 1 \in M \land (\sigma(M) \subset M) \;] \text{ Then } M = N$$

We call $$(N, \sigma)$$ a Peano system.

The set of all injective functions on $$N$$ form a semigroup under composition.

Let $$\mathcal C$$ denote the set of all injective functions on $$N$$ that commute with $$\sigma$$. It is easy to see that $$\mathcal C$$ is a semigroup containing the identity transformation.

Theorem 1: If $$\mu,\nu \in \mathcal C$$ and $$\mu(1) = \nu(1)$$ then $$\mu = \nu$$.
Proof
Let $$M$$ be the set of all elements in $$N$$ where the two functions agree. Applying induction with $$\text{(2)}$$, it is immediately evident that $$M = N$$. $$\quad \blacksquare$$

Theorem 2: For any $$m \in N$$, there exist a $$\mu \in \mathcal C$$ such that $$\mu(1) = m$$.
Proof
Again, simply apply induction. $$\quad \blacksquare$$

So $$\mathcal C$$ is in bijective correspondence with $$N$$.

Theorem 3: Let $$(N, \sigma)$$ and $$(N’, \sigma’)$$ be two Peano systems and $$\mathcal C$$ and $$\mathcal C’$$ the corresponding semigroups. Then there exist one and only one bijective correspondence $$\beta: N \to N’$$ satisfying

$$\tag 3 \beta(1) = 1’$$

$$\tag 4 \beta \circ \sigma = \sigma’ \circ \beta$$

Proof
The function $$\beta$$ is defined using recursion. Induction is used to show that $$\beta$$ is injective. Induction is used to show that $$\beta$$ is surjective. $$\quad \blacksquare$$

Using the above an argument can be supplied to prove the following.

Theorem 4: Let $$(N, \sigma)$$ and $$(N’, \sigma’)$$ be two Peano systems and $$\mathcal C$$ and $$\mathcal C’$$ the corresponding semigroups. Then the mapping $$\sigma \mapsto \sigma’$$ can be extended to an algebraic isomorphism between $$\mathcal C$$ and $$\mathcal C’$$.

We reserve the symbol $$\mathbb N$$ to denote $$\mathcal C$$ and use the symbol $$+$$ to denote the binary operation of composition.

Using the axioms of $$ZF$$, the existence of Peano systems is no problem.

I couldn’t find this technique here or on wikipedia, prompting

Is the theory described above coherent?

If it is it would certainly appeal to students who like to see some ‘motion/action’ when studying mathematical constructions, say somebody born to be a functional analyst.

Also, it is interesting to see how $$\mathbb N$$ obtained in this way can be viewed in some sense as the ‘dual’ of the Peano system.