# [FOM] Sigma-1 Completeness

Robert M. Solovay solovay at Math.Berkeley.EDU
Sat Aug 4 19:49:27 EDT 2007

```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

```