[FOM] What does Peano arithmetic have to offer?
Vaughan Pratt
pratt at cs.stanford.edu
Sat May 1 00:21:29 EDT 2010
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
More information about the FOM
mailing list