(How) can we derive "primary school rules of arithmetic" from the peano axioms? The Peano axioms are intended to be able to prove very general statements about arithmetic, such as "all natural numbers can be written as the sum of two primes".
However, how can we use the peano axioms to mathematically derive all the rules that are being taught to primary school children, about how to add and multiply?
e.g., can we derive general rules about arithmetic, which then allow us to compute $5\times4=20$? (you may assume that we've defined the symbols $5$, $4$ and $20$ in terms of the successor function of zero).
 A: I would say there is a big difference between arithmetical theorems that you can derive from the Peano axioms, and the algorithms (i.e. computations) that we are taught in elementary school to do things like multiplication or long division. 
I suppose you could still show that those algorithms are correct using the Peano axioms, but that would go a good bit beyond just a proof that $5 \times 4 = 20$.  Indeed, to prove that the general method works for numbers of any length (written in decimal notation), we'd need to prove things about arbitrary length sequences of decimal digits, which is not an easy thing to do in Peano Artihmetic; see Godel's Beta function.
Of course, I am talking about the addition and multiplication of multiple multi-digit numbers here ... when it comes to just two single digit numbers, the basic addition and multiplication table is pretty much drilled into our heads ... so I don't think there is much 'computation' going on there. So for something like $5 \times 4 = 20$, maybe a Peano axiom based proof that this is in fact the case would in fact capture that aspect of our arithmetical 'belief'.
A: Computing $5\times 4$ would take a little space. Instead here's a proof from the axioms that $2\times 2=4$. 
Note first that the definitions of $2$ and $4$ are $$2=SS0,\quad 4=SSSS0.$$
So $$2\times  2=(SS0)(SS0)=(S0)(SS0)+SS0=SS0+SS0=SSS0+S0=SSSS0.$$
A: Yes, those rules do indeed follow from the Peano axioms. Your use of "$20$" suggests that those rules are about calculation (algorithms) in base $10$. You would have first to define and prove what you need about expressing numbers in any base.
I assume you meant your question literally - can we prove? - rather than asking for actual proofs.
