[FOM] What does Peano arithmetic have to offer?

[Martin Davis]

On 5/2/2010 7:56 PM, Monroe Eskew (replying to Vaughan Pratt) wrote:
 > I don't understand; abstract algebra can be done within set theory
 > which is a first order theory.

Vaughan Pratt replied:

 >Sorry, I should have been more specific: by "first order logic" I had in
 >mind first order number theory in the sense of quantifying over numbers.
 >  An algebraic number theorist might indeed use a first order theory
 >quantifying over say rings and their homomorphisms, which would look
 >like second order logic to a number theorist accustomed to quantifying
 >over numbers.

Although I can't claim any expertise in these matters, I would expect 
that most of text-book algebraic number theory can easily be 
formalized in a conservative extension of PA. The idea is that the 
ring of integers of a finite extension of the rational number field 
is a finite dimensional vector space over the ring of rational 
integers and the ideals of such rings have a finite basis. Typically 
in such cases, it can all even be done in PA itself via some ugly but 
routine coding.

I would like to add, regarding the use of the powerful methods of 
category theory, the fact that those methods are used in proving an 
important theorem does not in any way diminish the interest of those 
truly interested in foundations of mathematics in the question of how 
much (if any) set theory is required for the proof. I believe that 
this question in the case of FLT remains unsettled.

Martin