[FOM] Rosser sentences

praatika@mappi.helsinki.fi praatika at mappi.helsinki.fi
Sat Jul 19 07:34:40 EDT 2003

Richard Grandy, commenting my query whether one could use the length of a 
proof instead of the size of the godel number of a proof to form a more 
invariant Rosser-like sentence, wrote:

> I don't think that will work because there are infinitely many 
> shorter proofs, whereas there are only finitely many proofs with 
> smaller Godel numbers and that is critical to the argument for the 
> Rosser theorem.

Actually, I don't think *this* is fatal (although I should have been more 
specific): it depends on how one defines the length of a proof; if one uses 
the number of lines, there are indeed infitely many shorter proofs, but if 
one rather uses the number of symbols, (with certain further 
qualifications) there are only finitely many proofs of a given length. It 
was obviously the latter notion I had in mind. 

Intuitively, it *seems* to me that the resulting provability predicate 
would work, but I find it difficult to get a satisfactory formalization of 
(I don't really have time now to think these issues in more detail. I am 
about to leave for some time away from my e-mail, so don't mind if I don't 
reply. But please feel free to continue the discussion.)



Panu Raatikainen

PhD., Docent in Theoretical Philosophy
Fellow, Helsinki Collegium for Advanced Studies
University of Helsinki
Helsinki Collegium for Advanced Studies
P.O. Box 4
FIN-00014 University of Helsinki

E-mail: panu.raatikainen at helsinki.fi

More information about the FOM mailing list