[FOM] What does Peano arithmetic have to offer?

[Martin Davis]

Vaughan Pratt wrote:

 >What does Peano arithmetic have to offer mathematics that isn't already
 > provided by the naive Roman numerals, suitably understood as forming the
 > free monoid on one generator "I"?

This would appear to be a simple category error. This free monoid 
provides a system of notation equivalent to e.g. the usual binary or 
even decimal notation. What PA (formal Peano arithmetic) provides is 
a *formalization* of elementary number theory incorporating 
mathematical induction with respect to any predicate definable in the 
language of arithmetic. As such it is part of an infinite chain of 
formal systems of increasing strength with respect to provability 
power. We could begin the chain with PRA (which permits induction 
only with respect to primitive recursive predicates)  or even 
Robinson's Q. Between the bottom and PA are systems permitting 
induction with respect to expressions with ever larger 
quantificational complexity. Above PA are systems allowing more and 
more set theory. Beyond the Zermelo axioms and ZFC are systems that 
incorporate large cardinal axioms. It should be emphasized that at 
each stage of this progression more and more statements of very 
simple number-theoretic form become provable. This form, the 
so-called Pi-0-1 sentences, can be thought of as asserting simply 
that some polynomial with integer coefficients has no zeros that are 
natural numbers.

Aspects of this progression have often been referred to on FOM. 
In  particular Harvey Friedman's extensive posts provide examples 
where large cardinal axioms are needed.

Martin, FOM moderator