[FOM] (no subject)

[Artemov, Sergei]

Dear Tim, 

> I say that G2 … is about the unprovability of Con(PA), but it is *not* about the 
> unprovability of the consistency of PA.

I am glad that you agree with my principal point. I wish others will follow suit. 


> Note that to conclude that G2 is 
> not about the unprovability of the consistency of PA, there is no need for 
> any fancy observations about nonstandard models and such.  All one has to 
> do is look at G2 and see that it's a statement about the unprovability of 
> Con(PA) and not about the unprovability of the consistency of PA. 

I wish things were that simple, but they are not. There are overwhelming signs of misunderstanding of this matter. 

“In his second theorem, he <Goedel> showed that such a system could not prove its own consistency …. This refuted Hilbert's assumption that a finitistic system could be used to prove the consistency of itself, and therefore anything else.” (Wiki article “Hilbert's program”).  

“If there were a finitary proof of the consistency of T, its formalization would yield a derivation in T of ¬PrT(x,⌈0 = 1⌉), from which ConT can be derived in T by simple universal generalization on x. Yet, a derivation of ConT in T is ruled out by G2.” (SEP article “Hilbert’s Program”).

Etc., etc., etc.

This is the principal goal of my PoC paper to demolish this unfortunate misconception. I am glad to find understanding; but I am afraid we need more serious mathematical arguments than your kind suggestion “all one has to do is look at G2.”

On a more serious note, we need the nonstandard model analysis to offer an alternative to Con(PA) as an arithmetical formalization of Hilbert’s consistency. Since nonstandard numbers cause the distortion in Con(PA) we have to find legitimate logical ways to keep x’s in ~Proof(x,0=1) standard. As strange as it looks, the way to do it is by a scheme 
   ConS(PA) = {~Proof(n,0=1) | n=0,1,2,… }. 
At the second look, ConS(PA) is not more alien to PA than the induction scheme. Both are provable in PA case-by-case and neither can be converted to a single formula. 

Best,
Sergei