[FOM] What does Peano arithmetic have to offer?

[Vaughan Pratt]

On 5/1/2010 11:25 AM, Harvey Friedman wrote:
> The key divide is whether one is interested in
>
> #) *HAVING A SCIENTIFIC THEORY OF MATHEMATICAL PROOF*
>
> I offer up some facts about PA of a certain kind that show PA "in
> action".
>
> [THEOREMs 1-5]

While these very nice theorems strikingly address limitations of 
elementary arguments about numbers, do they carry over for example to 
algebraic number theory as described at 
http://en.wikipedia.org/wiki/Algebraic_number_theory , or they specific 
to the proof theory of the elementary theory of numbers?

While I have no problem with the idea that *any* theory of a domain such 
as numbers (whether in a finitary or infinitary language) will have 
limitations of one kind or another, as a sort of Heisenberg-Goedel 
uncertainty principle for mathematics, what evidence is there that the 
limitations of a suitably sharply defined formulation of algebraic 
number theory will bear any resemblance to those of PA?  This was the 
point of item 3 in my response to Martin, about abstract algebra being 
just as problematic for FOM as category theory.

(And Andrej Bauer and I would both like to see a representative sample 
of answers to my question 1 in that response, about whether there's any 
important difference beween the free monoid on one generator and the 
initial successor-zero algebra.)

Perhaps Andreas Blass has some thoughts on this sort of thing since he's 
closer to the elementary-vs-algebraic boundary than many on this list.

Vaughan