[FOM] What does Peano arithmetic have to offer?

[Vaughan Pratt]

VP>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"?
>
MD>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.

1.  On which side of this divide (between free monoids and PA) does 
Andrej Bauer's post (of Thu Apr 29 18:02:31 EDT 2010 in the Falsify 
Platonism thread) fall, where he discusses the initial algebra with one 
constant 0 and one unary operation S?

If on the side of the free monoid on one generator, is he not then 
guilty of the same category error?

If on the other side, what is the difference between Andrej's initial 
algebra and my free monoid on one generator that makes Andrej innocent 
of this error?

2.  Had I asked what does PA *take away* from the naive Roman numerals I 
would have understood Martin's answer better---in fact it's roughly the 
answer I would have given myself to that question, albeit in somewhat 
less detail because it's not my area.

What PA has to "offer" mathematics seems more like what the tax code has 
to "offer" taxpayers.  If we identify these free and initial algebras 
with one's pretax salary, then the higher your grade of tax accountant 
(meaning the greater their familiarity with the tax code, auditors, law, 
precedents, courts, and judges) the more of your pretax salary you get 
to keep.  Inconsistency in PA has something of the flavor of your tax 
accountant overdoing things to the point where you get audited or worse, 
for which you and your accountant must divide up the blame between you. 
  The company that paid you your pretax salary did nothing wrong, having 
no incentive to fine tune its interpretation of the tax code (at least 
for employee salaries).

3.  While FOM has its misgivings about category theory as an alternative 
to elementary theories of mathematical domains, it seems to me that 
essentially the same misgivings ought to be triggered already by 
abstract algebra, which predates CT by quite a few decades.  (Not to be 
confused with elementary algebra, which is just quantifier-free 
equational logic, well inside the limits of first-order logic.)  The 
homomorphisms, quotients, products, tensor products, function spaces, 
etc. of abstract algebra fall well outside the scope of first order 
logic.  Yet even taken together they cannot be said to be anywhere near 
the power of full-blown second order logic, even though the instincts of 
a first order logician would be to classify abstract algebra as a second 
order system on the ground that it is not first order.

It seems to me that Martin's point applies to those mathematicians able 
to fit their proofs to the procrustean bed of first order logic.  Those 
who've drifted into the methodology of abstract algebra (and my 
impression is that they are a continually increasing number) would not 
appear to be well served by the tools that logic has developed and honed 
for their predecessors, since algebraists don't confine themselves to 
elementary language.  Yet neither do algebraists seem to fall afoul of 
the hazards of second order logic that first order logicians counsel 
vigilance against.

Vaughan