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

[William Tait]

At 9:47 AM +0000 7/6/02, Peter Smith wrote:
>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?

I have no particular example; but a good way to look for one might be 
this: the principle of induction up to epsilon_0 is provable in PA^1 
for every arithmetic formula phi(x) with just x free. The simplest 
proof of this is in ACA_0, where one proves for a set variable U and 
free numerical variable y that the validity of induction up to 
omega_{y+1} = omega^{omega_{y}} for {x | psi(x, U)} implies induction 
up to omega_{y+2} for U (where omega_0 is 1 and psi(x,U) is a certain 
formula arithmetic in U).

Bill Tait