[FOM] Godel Sentence

[Arnon Avron]

First and most impoerant: In my previous posting I asked for references 
to works on the following question:

1) How should the general concept of "A Godel sentence for a
theory T" be defined in 
exact, mathematical terms (so the question whether a given 
sentence is a Godel sentence will have a clear-cut answer,
even if we might not know that answer).

2) Is there an effective (or at least codification independent)
criterion for identifying Godel sentences?

3) Under what conditions are two different Godel sentences (obtained,
e.g., by two totally different methods of coding), equivalent,
and in what theory are they equivalent?

I got no reply to these questions (which are much more important
to me than a debate that is threatening not to be very productive).
Does this mean that no such work has ever been done?


Now to two short replies:


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

Well, some version of Consis_PA is a sentence like this (you may take
the version which is  more or less 
written in full in Girard's book "proof theory", in case you pretend
you dont know what sentence I am talking about). If you claim
otherwise than please supply a proof of it in PA (in case you claim
it is provable in PA) or explain what mistake have you found in 
the proof that it is true (using the standard model of PA).


Torkel says:

>>A Godel Sentence
>>is a sentence in the language of elementary arithmetics that expresses
>>a certain property of addition and multiplication of natural numbers.

>   You can say as much about any formalization in arithmetic of a
> mathematical statement, say one about the rational numbers. The Godel
> sentence "says of itself that it is unprovable" in a straightforward
> sense, just as the formalization in PA of the fundamental theorem of
> arithmetic "says that every natural number has a unique prime
> decomposition". A coding is always presupposed in such formalizations.

I find it as an abuse of the word "coding". Pehaps in English the same
word is used for what is done in Godel's proof and for what is done in 
this example. If so, then this is a shortcoming of the language,
that's all - because otherwise the connection is very small. As Smorynski has 
noted, what is done in Godel proof is very similar to what is done 
in word processors. This means a *real*` codification.
To describe in similar terms a reduction of a sentence in weak 
second-order logic to a first-order sentence which is obviously equivalent
to it (and this equivalence can straightforwardly be proved in any natural,
though incomplete, system for weak second-order logic) seems to me
totally inappropriate!,


Arnon Avron