Consider the following two definitions of the natural numbers:

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

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 prove this fact, 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$.

Generalizing

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:

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

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.

• 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)$

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.

Summary and question

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

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?