[FOM] Godel Sentence

[Karlis Podnieks]

----- Original Message ----- 
From: "Arnon Avron" <aa at tau.ac.il>
To: <fom at cs.nyu.edu>
Cc: "Arnon Avron" <aa at tau.ac.il>
Sent: Monday, August 25, 2003 11:40 AM
Subject: [FOM] Godel Sentence


> ....
> Kanovei writes:
>
> > Those who believe  in the paradigm
> > *there exist true, but unprovable sentences of PA*
> > in its straightforward sense
> > are welcome to kindly present such a remarkable sentence
> > along with a demonstration of its desired properties.
>
> I just could not believe my eyes when I read this. Are you serious???
>
...
>
> Arnon Avron

I believe, he is. For me as a formalist, the problem in "believing Penrose"
is caused by the simple fact, that,  for any serious formal theory T,

PA proves Consis(T)->GodelSentence(T).

If T is inconsistent, then GodelSentence(T) is false. Hence, any proof of
GodelSentence(T) means proving the consistency of T.

If you have proved the consistency of T, then you have proved that
GodelSentence(T) is true.

If you simply "believe" in the consistency of T, then you simply "believe"
that GodelSentence(T) is true.

Sometimes, a theory T1 can prove Consis(T2) of some other theory T2. For
example, ZF proves Consis(PA). But, if T1 could prove Consis(T1), then T1
would be inconsistent.

Thus, since Godel never proved the consistency of a serious formal theory,
his results are useless when discussing "true, but unprovable" sentences.
And, at least, Godel sentences and consistency statements cannot be used as
examples of "true, but unprovable" sentences.

The above-mentioned facts are... trivial? Yes, they are. And I cannot
believe my eyes that the discussion of the "true, but unprovable" still
continues - 75 years after Hilbert and Ackermann published the axioms of the
first order functional calculus in 1928, and without any remarkable success!
A kind of perpetuum mobile?

Best wishes,
Karlis.Podnieks at mii.lu.lv
www.ltn.lv/~podnieks
Institute of Mathematics and Computer Science
University of Latvia