[FOM] What does Peano arithmetic have to offer?

[Harvey Friedman]

The key divide is whether one is interested in

#) *HAVING A SCIENTIFIC THEORY OF MATHEMATICAL PROOF*

as opposed to ad hoc observations. The ad hoc observations may well be  
deep, insightful, exciting, useful, etcetera. And also the ad hoc  
observations may not be YET amenable to scientific treatment. We  
always strive to incorporated more and deeper phenomena into our  
scientific theories.

Nevertheless, it was only until modern times that the very idea of #)  
was imaginable or plausible. After Goedel's completeness and  
incompleteness theorems, there was a general consensus that #) exists  
and is rather substantive. Later events strengthened this consensus.

Once one adopts #), scientific objects such as PA = Peano Arithmetic  
are inevitable from many directions.

I offer up some facts about PA of a certain kind that show PA "in  
action".

THEOREM 1. Let n >> k. For any x_1,x_2,...,x_n from {1,...,k}, there  
exists 1 <= i < j <= n/2 such that the block x_i,...,x_2i is a  
subsequence (allowing skips) of the block x_j,...,x_2j.

THEOREM 2. Let n >> k. For any f:{1,...,n}^k into {1,...,n} obeying  
f(x) <= max(x), there exists 1 <= x_1 < ... < x_k+1 <= n such that  
f(x_1,...,x_k) <= f(x_2,...,x_k+1).

THEOREM 3. Let n >> k. For any f:{1,...,n}^k into {1,...,n} obeying  
f(x) <= max(x), there exists x_1 < ... < x_k+2 such that  
f(x_1,...,x_k) <= f(x_2,...,x_k+1) <= f(x_3,...,x_k+1).

THEOREM 4. Theorem 1 is provable in PA(3) but not in PA(2). I.e., in  
PA with the 3 quantifier induction scheme, but not in PA with the 2  
quantifier induction scheme.

THEOREM 5. Theorem 2 is provable in PA, and in fact, in EFA =  
exponential function arithmetic. Theorem 3 is not provable in PA, but  
is provable in ACA', or even PA + 1-Con(PA).

Harvey Friedman