[FOM] Sigma-1 Completeness

[Robert M. Solovay]

I've thought some more about the issue of Sigma-1 Completeness in weak 
theories. Contrary to what I said in my recent posting, it seems routine 
to get the strong version of provable Sigma_1 completeness in Buss's 
system S^1_2 provided the notion "Sigma_1 statement" is properly 
formulated. {Of course, the version I adopt will be equivalent in PA to 
the usual version of Sigma^1 statement. But in weak systems, careful 
formulation makes a difference.}

 	I give the basics of the definition of Sigma_1 I have in mind but 
do not spell out all the details. Code integers by strings of symbols from 
the two element alphabet {1,2} in some reasonable way. (Smullyan noptation 
is fine.) Code finite sequences of integers by strings on the three 
element alphabet {1,2,;} (Using ; as a separator between terms of the 
sequence.} Code one-tape TM's that operate on the alphabet {1, 2, ;, 
blank} in some reasonable way. Our prototypical Sigma one sentence has the 
form (exists y) such that TM with Godel # e halts on input x;y in less 
then length (x;y) steps. {If it needs saying length of x; y is about log x 
+ log y }

 	To see that Sigma_1 completeness hold in S^1_2 uses the following 
ingredients:

 	1) There is a good mechanism for coding finite sequences. 
(Established by Buss in his thesis.)

 	2) S^1_2 can reason about polynomial time computations in an 
efficient and effective manner. (Again cf. Buss's thesis.)

 	3) One can simulate TM computations by proofs in a PolyTime 
computable manner. (In my paper "Injectging inconsistencies into models of 
PA, http://shurl.net/505, I discussed the problem of efficiently 
simulating TM computations by proofs in PA. But the discussion would 
easily adopt to the weaker system S^1_2.)

 	As to weaker systems, the proofs I have in view really use closure 
under the function {n -> 2^ {(log n) ^ 2} }. And it's hard to see how one 
could prove anything without at least the amount of induction in S^1_2. So 
S^1_2 is looking like bedrock.

 	--Bob Solovay