Proof in Peano Arithmetic I am trying to prove $S0 \times SS0$ using the axioms of Peano Arithmetic. The axioms are:

*

*$\forall x \hspace{0.05cm}0 \ne Sx$

*$\forall x \forall y \hspace{0.05cm} (Sx = Sy \rightarrow x = y)$

*$\forall x \hspace{0.05cm} x + 0 = x$

*$\forall x \forall y \hspace{0.05cm} x + Sy = S(x + y)$

*$\forall x \hspace{0.05cm} x \times 0 = 0$

*$ \forall x \forall y \hspace{0.05cm} x \times Sy = x \times y + x$
Two useful tools that are available to us (I have proven them) are the symmetry of identity and the transitivity of identity, respectively:
$\vdash \forall x \forall y \hspace{0.05cm} (x = y \rightarrow y = x)$
$\vdash \forall x \forall y \forall z \hspace{0.05cm} (x = y \wedge y = z \rightarrow x = z)$
We are using an axiomatic proof system for first-order logic, so all those logical axioms are also available to us. I have completely stalled on this proof. My hunch is that we are going to want to make use of the both symmetry and identity, but I've played around with the axioms and found no route forward. In particular, we can get:
$$S0 \times SS0 = S0 \times S0 + S0$$
from 6, and from here and 4 can get:
$$S0 \times S0 + S0 = S(S0 \times S0 + 0)$$
But we're no closer to $SS0$ from these. When you stare long enough at these ugly symbols, you are wont to get dizzy, which is what has happened to me. I wonder if anyone can shine a light on this issue so that I might get out of this hole?
Note: I have proven universal elimination, so we are fine for that.
 A: Maybe some intuition for how the addition and multiplication axioms work will help.
Axioms 3 and 4 are a recursive definition of addition: for evaluating $x+y$, they either tell you the answer (if $y=0$) or reduce the addition to a different addition with smaller $y$. Using the mysterious symbols "$1, 2, 3, 4$" as shorthand for "$S0, SS0, SSS0, SSSS0$", they tell you things like:
\begin{align}
   x + 0 &= x \\
   x + 1 &= S(x+0) \\
   x + 2 &= S(x+1) \\
   x + 3 &= S(x+2) \\
   x + 4 &= S(x+3) 
\end{align}
and so on. We are defining $x+1$ in terms of $x+0$, $x+2$ in terms of $x+1$, and so forth, recursively.
Axioms 5 and 6 are doing the same thing for multiplication. An expression $x \times y$ can be either evaluated directly (if $y=0$) or reduced to another multiplication with smaller $y$.
You will not really go wrong applying these axioms in just about any order you can, so in some sense all you have to do is just be patient and keep going the way you have been!
However, if you want to be systematic about it, you could first apply axioms 5 and 6 over and over (until you're left with only addition) then apply axioms 3 and 4 over and over (until you're left with no binary operations at all). Make sure to keep all parentheses intact as you substitute, because associativity is not one of the axioms.
A: You are going in the right direction. For your next step, note that $S0 \times S0$ is equal to $S0 \times 0 + S0$ by axiom 6, which in turn is equal to $0 + S0$ by axiom 5. Now you've gotten rid of all the multiplication, and the next step is to get rid of all the addition (and then you'll be done).
