I was reading a Bachelor thesis on Peano Arithmetic (PA). PA has the following axioms (not including the induction schema):
$$\begin{align}
& (A1) ~~~~ \forall x \neg (x + 1 = 0) \nonumber \\
& (A2) ~~~~ \forall xy (x + 1 =y + 1 \to x = y) \nonumber \\
& (A3) ~~~~ \forall x (x + 0 = x) \nonumber \\
& (A4) ~~~~ \forall xy (x + (y +1) = (x + y ) + 1) \nonumber \\
& (A5) ~~~~ \forall x (x \cdot 0 = 0) \nonumber \\
& (A6) ~~~~ \forall xy (x \cdot (y + 1) = (x \cdot y) + x) \nonumber...