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

[friedman@mbi.math.ohio-state.edu]

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. 

It is of interest to do some careful estimates on this, using standard Hilbert 
style presentations of PA and ACA_0. I suspect that A[1,000,000] may already 
have a striking actual real world speedup.

2. Let (forall k)(forall n)(therexists m)(B(k,n,m)) be any of your favorite Pi-
0-2 sentences known to be equivalent to the 1-consistency of PA. The first one 
that was established was due to Paris/Harrington, but I developed quite a 
number of others, later. E.g., see my Annals of Math paper in 1998. And some 
others have been the subject of FOM postings. Here k is the dimension or arity 
of the statement. 

For each integer k, let C[k] = (forall n)(therexists m)(B(k,n,m)). Then C[k] 
cannot be proved in PA without at least k bits. However the same comments apply 
to C[2^k], C[2^2^k], even C[2*k].

> 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 ??
>
Pure number theorists routinely use complex variable theory and other higher 
order theories in their work. So if they are interested in whether their stuff 
is provable in PA - and I collaborate with one who does - then ACA_0 is a good, 
easy, tool for this. However, for more delicate issues like provability in EFA 
(exponential function arithmetic), it is a useless overgrown sledge hammer. A 
few years back, I developed such things as set theories conservative over EFA. 
But much more work is needed to forge more delicate tools in useful form. Of 
course, the fundamental base theory of reverse mathematics, RCA_0, as well as 
the stronger WKL_0, are quite useful for quickly reading off that some things 
are provable in PRA (primitive recursive arithmetic), as they are conservative 
over PRA. And here we have the same speed up phenomenom. It boils down there to 
the speedups involving Sigma-0-1 induction over PRA.