• The natural numbers are the algebraic structure generated by one constant and one unary function (with no relations).
• The natural numbers are the monoid with presentation $\langle 1 \mid \rangle$.

How could we prove that these two definitions are equivalent? One option, of course, is to take your favorite set theory, define both of the above objects formally, and use first-order logic to construct a proof.

However, it's also possible to prove these definitions equivalent without using set theory or logic at all. The method is essentially the same as using Tietze transformations to prove that two group presentations generate the same group.

Both of these presentations present the infinite cyclic group. If we want to prove this fact, then using set theory and first-order logic would be overkill. Instead, we can simply use Tietze transformations, as shown:

After all of these transformations have been completed, the only item remaining is item 5, which is the generator $c$.

Define a generic presentation as an algebraic theory. We refer to the free algebra of the theory as "the algebra generated by the presentation," and we informally consider two generic presentations to be equivalent if the algebras that they generate are essentially equivalent.

The first definition of the natural numbers above is formalized as this generic presentation:

And the second definition of the natural numbers is formalized like so:

Much as we did above, we can prove that these two definitions are equivalent using a sequence of transformations which are similar to the Tietze transformations. However, it is necessary to add additional kinds of transformations. In addition to adding (or removing) a constant along with a single equation defining it, I think we need to be able to add (or remove) a function symbol along with a set of equations defining it. I think we can require the set of equations to be a primitive recursive function definition; I haven't worked out the details. When it comes to adding or removing a relation, we need to be able to make use of inductive proofs as well as simple proofs by substitution.

In any case, below is the proof that the above two presentations are equivalent. Once again, the proof consists of a sequence of Tietze-like transformations, starting with the first presentation and ending with the second one.

Starting with items 1 and 2, we add items 3 through 10, and then we remove items 2, 4, 6 and 8, leaving items 1, 3, 5, 7, 9, and 10, which are identical to the second presentation above.

There are 6 "Tietze-like transformations" that we've used to prove that these two definitions of the natural numbers are equivalent:

• The natural numbers are the algebraic structure $\mathbb{N}_1$ generated by one constant, $0$ and one unary function, $S$ (and no relations).
• The natural numbers are the monoid $(\mathbb{N}_2, 0, +)$ with presentation $\langle 1 \mid \rangle$.

These two definitions are equivalent, in the sense that there exists a certain "nice" bijection between the structures they define: namely, the unique function $f : \mathbb{N}_1 \to \mathbb{N}_2$ with $f(0) = 0$ and $f(S(x)) = f(x) + 1$, which is a bijection.

How could we prove that the bijection $f$ satisfying those two equations really does exist? One option, of course, is to take your favorite set theory, define all of these objects formally, and use first-order logic to construct a proof.

However, it's also possible to show that this bijection exists without using set theory or logic at all. The method is essentially the same as using Tietze transformations to define an isomorphism between the groups generated by two group presentations.

Both of these presentations present the infinite cyclic group. If we want to construct an isomorphism, then using set theory and first-order logic would be overkill. Instead, we can simply use Tietze transformations, as shown:

After all of these transformations have been completed, the only item remaining is item 5, which is the generator $c$.

So, using the Tietze transformations, we have constructed an isomorphism $f$ from the first group to the second group, with $f(a) = c^2$ and $f(b) = c^3$.

Define a generic presentation as an algebraic theory. We refer to the free algebra of the theory as "the algebra generated by the presentation."

The first definition of the natural numbers above ($\mathbb{N}_1$) is formalized as this generic presentation:

And the second definition of the natural numbers ($\mathbb{N}_2$) is formalized like so:

As mentioned at the beginning of this question, there is a bijection $f : \mathbb{N}_1 \to \mathbb{N}_2$ with $f(0) = 0$ and $f(S(x)) = P(f(x), 1)$. How can we construct this bijection?

Much as we did with the infinite cyclic group above, we can construct this bijection using a sequence of transformations which are similar to the Tietze transformations. 

However, the Tietze transformations themselves are not quite sufficient for this purpose. In addition to the four Tietze transformations, we need to add two additional "Tietze-like transformations" to our toolbox. Specifically, in addition to adding (or removing) a constant along with a single equation defining it, I think we need to be able to add (or remove) a function symbol along with a set of equations defining it. (I think we can require the set of equations to be a primitive recursive function definition; I haven't worked out the details.)

Furthermore, two of the Tietze transformations need to be altered to make them more powerful. Specifically, the Tietze transformations allow us to add or remove a relation if we can prove that relation from the other relations using a simple proof by substitution. We need to alter these so that we are also permitted to use inductive proofs of equality. (Again, I haven't worked out the details.)

The resulting "toolset" consists of six Tietze-like transformations: adding or removing a (constant) generator; adding or removing a function; and adding or removing a relation (potentially using an inductive proof). These six transformations are sufficient to construct the desired bijection between $\mathbb{N}_1$ and $\mathbb{N}_2$.

Below is the construction. Once again, it consists of a sequence of Tietze-like transformations, starting with the first presentation and ending with the second one.

When we work through the above list of transformations, we start with items 1 and 2, and we add items 3 through 10, and then we remove items 2, 4, 6 and 8, leaving items 1, 3, 5, 7, 9, and 10. This list of items is identical to the second presentation above, so we have successfully constructed the bijection.

There are 6 "Tietze-like transformations" that we've used to construct the desired bijection between the two definitions of the natural numbers above: