[FOM] Godel Sentence (a reply to Podnieks)

[Arnon Avron]

I find myself engaged much more than I have intended in this discussion,
and the reason I am still continuing is that I am really amazed of what 
is going on. Obviously I fail to explain what has  seemed to me as obvious and
known to every expert. But what really shocks me is that it seems that
some responses I get, and from great logicans, simply ignore what is actually
written. If logicans cannot or dont want to read what they are replying to,
then what can be expected from other people (and how can there ever be peace 
in the middle-east or anywhere else?).

Thus Podnieks Write (I have to repeat it all. Sorry):

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

Kanovei did not ask for an example of a "true, but unprovable" sentence.
You have quoted yourself what he was asking for. It was (and it is emphasized
between two stars in his message!) "true, but unprovable sentences of PA".
Need I really explain that these are totally different things???
It is evident that even though "true, but unprovable" arithmetical sentences
might well exist, nobody will ever be able to come with a concrete example
together with a convincing argument that it is indeed an example - because
this would mean proving the unprovable sentence. 
On the under hand any reasonable version of Consis_PA is a true 
arithmetical sentence which is not provable *in PA*. You may protest
as a formalist and say that "truth" is meaningless here. But Kanovei
was explicitly asking for a "true, but unprovable sentences of PA" -
and such thing can be asked only if it is accepted that it is meaningful
to say that sentences in the language of PA might be true or false.
(if someone think that by definition nobody can come with an example of a true
sentence of PA then it would be dishonest of her/him
to ask for an example of a sentence which
in addition to being true has other interesting properties as well).
Now the only reasonable notion of "truth of sentences of PA" is truth
in the structure of the Natural numbers (the "standard model"). And
I simply cannot see that one can accept the Natural numbers and still
honestly doubt the consistency of PA. So if arithmetical truth has 
any meaning at all, then PA is consistent, and from this one can infer
that Consis_PA is true (the last step of showing that if 
PA is consistent then Consis_PA is a true arithmetical sentence
requires proof and a lot of work, but the proof has been given by Godel).
Consis_PA is of course also not provable *in PA* (I am sure that 
Podnieks knows this as well as I do. What I cannot understand is
why he seems to ignore this knowledge in his reply).

One more comment that is *irrelevant to my answer to Kanovei*: I have certain
formalist tendencies myself, especially with respect to Set Theory. But it
seems to me that even a formalist has no choice but to accept that 
the notion of truth in certain domains is meaningful and necessary 
(it seems to me necessary for a coherent formalist to accept that
the question whether a given formal sentence has a formal proof
in a given formal system  has an absolute "yes" or "no" answer).
And once syntactical truth is accepted as meaningful and absolute,
I see no honest alternative to accepting that arithmetical truth
in N (at least of Pi-0-1 and Sigma-0-1 sentences, in order not
to enter  further debates) is meaningful and absolute.