[FOM] What does Peano arithmetic have to offer?

[Harvey Friedman]

On May 3, 2010, at 1:38 PM, Vaughan Pratt wrote:

> 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.

With regard to "normal mathematics", PA has enormous expressive power.  
Of course the language has very few primitives, so that this  
expressive power, when put into action, is rather ugly. But one can  
design what are called "strong conservative extensions of PA", where  
one adds lots of new primitives without changing the power, so that  
the expressive power, when put into action, is rather pretty.

If there is a serious part of algebraic number theory for which it is  
not obvious how to formulate the statements in PA, and there is no  
gratuitous generality involved, then that would make it far more  
likely that an incompetent algebraic number theorist like me could  
come up with statements of the kind in http://www.cs.nyu.edu/pipermail/fom/2010-May/014703.html 
  which are in the spirit and culture of algebraic number theory.

But I have my doubts as to whether the hypothesis in the previous  
paragraph is true. E.g., probably one is only really interested in  
finitely generated structures of good kinds, where homomorphisms are  
determined nicely based on finite information, etcetera. Then the  
formalization in PA is straightforward.

As for literally carrying over statements in ??? to algebraic number  
theory, this is possible, but more likely is that they have to be  
adapted.

Proving that something cannot be done in PA does not say that somebody  
can't do them. It just means that they can't do them in some "normal"  
fashion.

Of course, proving that something cannot be done in stronger fragments  
of ZFC, or even in full ZFC, is much much more powerful.

> What I don't see is whether Harvey's theorems 4 and 5 are sufficiently
> robust as to carry over to algebraic number theory in any form a  
> number
> theorist would understand.  If not then they would seem to be the sort
> of theorems that would appeal only to logicians and those number
> theorists still working inside PA.  Algebraic number theorists  
> consider
> that they're doing number theory, which raises the question, what can
> logicians tell number theorists they can't do?

"appeal only to logicians and those number theorists still working  
inside PA" makes no sense to me. There is such a thing as "general  
intellectual interest".

Would you say:

Beethoven's Fifth Symphony is the sort of thing that would appeal only  
to musicians and those number theorists who have children in orchestras?

> It seems to me that examples of this kind illustrate the non- 
> robustness
> of theorems of logic when brought to bear on mathematical subjects  
> that
> can be usefully treated in incomparable logical frameworks.  Each
> framework will have its limitations, but why should they carry over to
> other frameworks?

What incomparable logical frameworks? Aren't all of the usual  
reasonable logical frameworks for doing classical mathematics  
comparable?

Specifically, what reasonable logical framework do you have in mind  
which will not be sensitive to the special status of the statements in http://www.cs.nyu.edu/pipermail/fom/2010-May/014703.html

Harvey Friedman