[FOM] PA and recursive saturation: correction

[Harvey Friedman]

On 3/23/06 6:17 AM, "Jeremy Avigad" <avigad at cmu.edu> wrote:

> Responding to a posting of Arhat Virdi, on March 19 Harvey Friedman wrote:
> 
>> Let T be any reasonable theory, finitely axiomatized like ISigma1, or
>> schematically like PA. We can form T(sat) as you indicate.
> 
> ...
> 
>> It also appears that for reasonable T, there is a superexponential blowup
>> here. Is this known?
> 
> I responded that this is straightforwardly provable using techniques
> described by Pudlak in his article in the Handbook of Proof Theory.
> 
> I was too glib. Harvey has pointed out to me that the argument I had in
> mind does not work when T is PA. In that case, I suspect the claim is
> false; with care, it should be possible to use reflection in PA and
> eliminate the sat predicate without significant blowup.
> 
> I think my argument works in the finitely axiomatized case, though. That
> is, I think the following theorem and sketch of a proof are correct. ...

Avigad goes on to sketch an argument. What he sketches appears to be exactly
my proof for the finitely axiomatized case, except I just simply quote my
finite Godel's theorem rather than redo that self reference argument at the
end. 

I thought I could probably also do this for (systems like) PA, but I will
think about this situation some more...

Harvey Friedman