[FOM] PA Speed-up over HA?
sbuss at math.ucsd.edu
Mon Mar 29 13:33:06 EST 2004
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
This proof method is bit disappointing from a foundational
point of view, but nonetheless applies in many situations.
More information about the FOM