FOM: ACA, Conservativeness, Speed-up, etc ....>

[Richard Zach]

> Date: Sat, 6 Jul 2002 09:47:33 +0000
> From: Peter Smith <peter.smith at phil.cam.ac.uk>
> Subject: FOM: ACA, Conservativeness, Speed-up, etc ....
> 
> The first question is short and simple: ACA_0 is conservative over 
> PA^1: but is there any first-order arithmetical truth which has a 
> much faster/nicer proof in ACA_0 than in PA^1 ?  If so, what is the 
> neatest/simplest example?

ACA_0 has non-elementary speedup over PA; the result is due to Solovay
and/or Pudlak, I believe.  

-- 
Richard Zach ...... http://www.ucalgary.ca/~rzach/
Assistant  Professor,   Department  of  Philosophy
University of Calgary, Calgary, AB T2N 1N4, Canada