[FOM] Modified Rosser sentences

[Thomas Forster]

On Mon, 14 Jul 2003 JoeShipman at aol.com wrote (inter alia):

> 
> Does the notion of a "coding-independent Rosser sentence" make sense? 
> If such a thing exists, then a more "mathematical" version of it would
> provide the desired type of independence; if not, then we still have an
> annoying asymmetry in the known "mathematical incompletenesses". 
> 
> -- JS
> 



I suspect there is quite a lot that can be said about this.  I have been
trying to get Harold Simmons to prove a theorem about it, along the
following lines.  The (sic) Rosser sentence says ``there is a proof of me
s.t. no proof with lower gnumber is a proof of not-me''.  Now if we
replace ``proof with lower gnumber'' by ``proof that is a fragment of me''
then we have a predicate that one would expect to be much less sensitive
to choice of gnumbering.  I conjecture that for tweaked versions along
these lines it should be possible to show that all such Rosser sentences
are equivalent.

      The reason why i believe this is that, altho' all these diagonal
arguments (at least those underlying what Ramsey called the `semantic'
paradoxes in contrast to the `logical' paradoxes - at least i *think*
those were the two words he used) depend on a kind of type violation:
regarding a gnumber both as data and as program, for example.  The kind of
type-violation involved in my modification of Rosser sentences is less
brutal than that in the original (and is like that in G\"odel sentence) in
a way that i haven't yet worked out but which i suspect that anyone who
has ever had to program in a typed language will immediately recognise.

          Thomas Forster