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

[Robert M. Solovay]

On Tue, 9 Jul 2002 friedman at mbi.math.ohio-state.edu wrote:

> Reply to Smith 7/8/02.
>
> > 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?
> >
> Here are two styles of examples, one metamthatical, and the other
> combinatorial.
>
> 1. Let n be an integer, and define A[n] = Con(Sigma-0-n induction). Then A[n]
> cannot be proved in PA without at least n bits. However, A[2^n], as normally
> formalized, can be proved in ACA_0 with at most a small constant times n bits.
> This is also true of A[2^2^n]. One formulation is that in order to prove A[2*n]
> in ACA_0, as normally formlaized, a small constant times n bits suffices. Here
> 2*n is 2^2^2^...^2, where there are n 2's.
>

	This is not quite correct. The following results are due to me
[unpublished]:

	There is a small positive constant c and a large positive constant
C [actually they are not that small or large resp.] such that:

	1) A[2*n] has a proof in ACA_0 of length at most Cn^2;

	2) A[2*n] has no proof in ACA_0 of length less than cn^2.

	It's been a while since I've done this and I have not stopped to
reconstruct the proofs. The proof of 2) involves a sharp quantitative form
of Herbrand's theorem.

	--Bob Solovay