Consider the following two definitions of the natural numbers:

* 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](https://en.wikipedia.org/wiki/Tietze_transformations) to define an isomorphism between the groups generated by two group presentations.

### Groups and Tietze transformations

Consider the following two group presentations (which I'm writing using deliberately bulky notation). First:

1. $a$
2. $b$
3. $ab$ = $ba$
4. $a^3 = b^2$

And second:

1. $c$

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:

* Add a generator $c$ with definition $c = b a^{-1}$ (5 and 6 below).
* Add a relation $c^3 = b$ (7 below). Proof: $c^3 = (b a^{-1})^3 = b^3 a^{-3} = b^3 b^{-2} = b$.
* Add a relation $c^2 = a$ (8 below). Proof: $c^2 = (b a^{-1})^2 = b^2 a^{-2} = a^3 a^{-2} = a$.
* Remove the relation $c = b a^{-1}$ (6 below). Proof: $c = c^3 c^{-2} = b a^{-1}$.
* Remove the relation $ab = ba$ (3 below). Proof: $ab = c^2 c^3 = c^3 c^2 = ba$.
* Remove the relation $a^3 = b^2$ (4 below). Proof: $a^3 = (c^2)^3 = (c^3)^2 = b^2$.
* Remove the generator $a$ with definition $a = c^2$ (1 and 8 below).
* Remove the generator $b$ with definition $b = c^3$ (2 and 7 below).

1. $a$
2. $b$
3. $ab = ba$
4. $a^3 = b^2$
5. $c$
6. $c = b a^{-1}$
7. $c^3 = b$
8. $c^2 = a$

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$.

### Generalizing

Define a **generic presentation** as an [algebraic theory](https://en.wikipedia.org/wiki/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:

1. $0$ (a generator which is a nullary operation)
2. $S(-)$ (a generator which is a unary operation)

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

1. $0$
2. $P(-,-)$
3. $P(0,x) = x$
4. $P(x,0) = x$
5. $P(x,P(y,z)) = P(P(x,y),z)$
6. $1$

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.

* Add a generator $1$ with definition $1 = S(0)$ (3 and 4 below).
* Add a generator $P(-,-)$ with definition $P(x,S(y)) = S(P(x,y))$ and $P(x,0) = x$ (5, 6, and 7 below).
* Add a relation $P(x,1) = S(x)$ (8 below). Proof: $P(x,1) = P(x,S(0)) = S(P(x,0)) = S(x)$.
* Add a relation $P(0,x) = x$ (9 below). The proof is by induction. The $0$ case: $P(0,0) = 0$. The $S$ case: $P(0,S(x)) = S(P(0,x)) = S(x)$.
* Add a relation $P(x,P(y,z)) = P(P(x,y),z)$ (10 below). The proof is by induction. The $0$ case: $P(x,P(y,0)) = P(x,y) = P(P(x,y),0)$. The $S$ case: $P(x,P(y,S(z))) = P(P(x,y),S(z))$ (details omitted).
* Remove the relation $1 = S(0)$ (4 below). Proof: $1 = P(0,1) = S(0)$.
* Remove the relation $P(x,S(y)) = S(P(x,y))$ (6 below). Proof: $P(x,S(y)) = P(x,P(y,1)) = P(P(x,y),1) = S(P(x,y))$.
* Remove the generator $S(-)$ with definition $S(x) = P(x,1)$ (2 and 8 below).

1. $0$
2. $S(-)$
3. $1$
4. $1 = S(0)$
5. $P(-,-)$
6. $P(x,S(y)) = S(P(x,y))$
7. $P(x,0) = x$
8. $P(x,1) = S(x)$
9. $P(0,x) = x$
10. $P(x,P(y,z)) = P(P(x,y),z)$

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.

### Summary and question

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

1. Adding a relation which can be proved from the other relations.
2. Removing a relation which can be proved from the other relations.
3. Adding a (nullary) generator along with a relation defining it.
4. Removing a (nullary) generator along with a relation defining it.
5. Adding a generator with any arity along with a set of equations constituting a primitive recursive definition of that generator.
6. Removing a generator with any arity along with a set of equations constituting a primitive recursive definition of that generator.

Transformations 1 through 4 are the Tietze transformations; 5 and 6 are new. (Of course, 3 and 4 are special cases of 5 and 6.)

I'm sure that I'm not the first person to come up with this idea. Have these "Tietze-like transformations" been studied before?