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

[Peter Smith]

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?

Generalizing to a more open-ended second question: Is there any 
reason for the pure arithmetician (as opposed to someone whose 
interest is in reconstructing large parts of classical analysis) to 
love ACA_0 ??

Thanks in advance!
-- 
_________________________________________________________________________
Dr Peter Smith
DoS in Philosophy and HPS
Jesus College
Cambridge CB5 8BL, UK
http://www.phil.cam.ac.uk/Smith
_________________________________________________________________________