[FOM] Rosser sentences (fwd)

Thomas Forster T.Forster at dpmms.cam.ac.uk
Sat Jul 19 06:40:17 EDT 2003

---------- Forwarded message ----------
Date: Fri, 18 Jul 2003 17:47:35 +0100 (BST)
From: Thomas Forster <tf at dpmms.cam.ac.uk>
To: praatika at mappi.helsinki.fi
Cc: fom at cs.nyu.edu
Subject: Re: [FOM] Rosser sentences

On Fri, 18 Jul 2003 praatika at mappi.helsinki.fi wrote:

> Just a spontaneous thought I did not reflect that carefully (so feel free 
> to give criticism):
> I wonder whether one could use the length of a proof instead of the size of 
> its godel number to have a rosser-like sentence which is not depended on a 
> particular godel numbering?  At first sight, this seems to make the 
> sentence Pi-0-2, not Pi-0-1, but I wonder whether one can get around this...
> Intuitively, it seems to me that the resulting property is nevertheless co-
> r.e. (i.e. Pi-0-1).
> (Whether or not this is relevant: most actual godel numberings seem to have 
> the property that 
>      length(p1) < length(p2)   =>  gn(p1) < gn(p2)   
> and
>      gn(p1) < gn(p2)  =>    length(p1)<_ length(p2).
> (p1, p2 are proofs, gn's their godel numbers). 
> I wonder whether one could somehow utlize this issue?) 
> If anything like this is definitely impossible, I would be interested in 
> seeing clearly why exactly. 
> Best
> Panu

This is the kind of thing I had in mind.   What is needed is a criterion
of shortness or fragment-of which can be expressed in terms of the
structure of proofs and doesn't depend on the gnumbering.   Anything like
that should make the new Rosser sentence more invariant....

           Thomas Forster

More information about the FOM mailing list