[FOM] PA Speed-up over HA?

[Sam Buss]

  Yes, there is speedup of PA over HA.  The Statman method should
work fine.   This is from his paper "Speedup by theories with infinite
models, Proc. AMS 81 (1981) 465-469.

  Another way to learn the Statman method is to read my
account of the application of the Statman method to
higher order versions of PA in the final section 3 of the paper:
"On Godel's theorems on lengths of proofs I:
Number of lines and speedups for arithmetic." 
Journal of Symbolic Logic 39 (1994) 737-756.
available at http://www.math.ucsd.edu/~sbuss/ResearchWeb/godelone/paper.ps
(or .../paper.pdf).

  This proof method is bit disappointing from a foundational 
point of view, but nonetheless applies in many situations.

 -- Sam