[FOM] Rosser sentences (fwd)

[Thomas Forster]

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