[FOM] Modified Rosser sentences
Thomas Forster
T.Forster at dpmms.cam.ac.uk
Tue Jul 15 04:24:53 EDT 2003
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
More information about the FOM
mailing list