1
$\begingroup$

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

$\endgroup$
3
  • $\begingroup$ It's not clear to me what you're asking for--how would "general rules about arithmetic" be used to compute $5\times 4=20$? $\endgroup$ – Eric Wofsey Mar 17 '18 at 19:22
  • 1
    $\begingroup$ Would showing $5\times 4 = 4+ (4+ (4+(4+4)))$ be enough? $\endgroup$ – Henry Mar 17 '18 at 19:25
  • $\begingroup$ Are you asking how to formulate decimal notation in the Peano axioms and prove the rules for decimal arithmetic work? (The rules for decimal arithmetic generally take the addition and multiplication of single-digit numbers as input, though, so they aren't much help for computing $5\times 4$...) $\endgroup$ – Eric Wofsey Mar 17 '18 at 19:25
1
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ I think you can write the "standard algorithms" as recursive functions to calculate digits - just mathematics. That's all "program verification" would amount to in this context. $\endgroup$ – Ethan Bolker Mar 17 '18 at 19:31
  • $\begingroup$ @EthanBolker Sure ... but showing that our typical methods of multiplying two multi-digit numbers are correct would still go a good bit beyond a mere proof that the product of two numbers is what it is. 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 always a hard thing to do in Peano Artihmetic; see Godel's Beta function. $\endgroup$ – Bram28 Mar 17 '18 at 19:33
  • $\begingroup$ OK. I'm beyond my depth and defer to your deeper knowledge. $\endgroup$ – Ethan Bolker Mar 17 '18 at 19:49
  • $\begingroup$ @EthanBolker It's not all that deep, really :) I just happen to know that sequences are not Peano Axioms' friends. $\endgroup$ – Bram28 Mar 17 '18 at 19:55
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.