[FOM] Godel Sentence

[Arnon Avron]

Torkel Franzen writes:
> 
>   If we don't seek any intensional characterization, we can define a
> Gödel sentence for T as a sentence A for which there exists a
> standard formalization Con(T) of "T is consistent" such that Con(T)
> is equivalent to A in T. Here everything about Con(T) is fixed
> (including the Gödel numbering used, which is any standard version)

Fixing Con(T) is begging the question. As I wrote in a previous message,
I would like to know, e.g,, whether there is any ground to assume that
something like (say) Goldbach conjecture cannot be equivalent
to a sentence that we may take as naturally expressing Con_T. Your talk
about "any standard version" hides (I believe) the assumption that 
all the sentences that might be obtained by some "standard version"
are provably equivalent (in T, I guess). Perhaps this is the case -
and references for works which investigate this problem is precisely
what I was asking. On the other hand, some conditions should be imposed.
For example, suppose that we take as the underlying proof systems
Gentzen's formalizations of PA in which induction is a rule rather
than an axiom. There is a version with the cut rule, and another
one in which only inessential cuts are allowed. I think that both
can be ijustly used for "standard versions". Will the resulting sentences 
expressing the consistency of T be equivalent in T?


>   >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!,
> 
>   So can you indicate in what sense a Gödel sentence is, but a formalization
> of the fundamental theorem of arithmetic is not, "a sentence...that expresses
> a certain property of addition and multiplication of natural numbers"?

Of course both of them express properties of addition and 
multiplication of natural numbers. But with the second nobody has to be 
reminded about this fact, and nobody claims that it says something different
from what it actually says. What I was protesting is your description
of both as being of the same type of "coding".
 
>   I can't extract any such sense from your comments. It's not as though
> an ordinary formalization in the language of arithmetic of the FTA,
> written out in full, would in the least strike us as "saying that
> every natural number has a unique prime decomposition". 

I dont think so, but of course if given a version in which it will not
strike me that it is equivalent to FTA, then I will not say that it 
is a sentence that express FTA,
but only that it is a sentence which  is equivalent to FTA - and
demand a proof  of that equivalence (both the equivalence and proof 
should of course be formulated, at least in principle,
in a natural system for the language in which the real FTA can be formulated).
In fact, also a Godel-sentence G is only *equivalent* to a sentence
"expressing the unprovability of G" - at least in all books I have seen
the claim is that G<-> -Pr_T([G]) is a theorem of T, not that G is *identical*
to -Pr_T([G]) (which clearly cannot be the case). But G is also equivalent
to Con_T. So does G express/formalizes/says that T is consistent? The 
answer (which I am NOT dismissing) might be that the equivalnce of 
G<-> -Pr([G]) is easy to prove while the other is not. So just equivalence
(even in T) is not enough for saying that two sentences express
the same mathematical fact. Factors like naturalness, length of proof(?),
difficulty of the proof and others are important here. Can these
factors be made precise? I admit that I dont know. 

> Gödel sentence is obtained through a reduction of a sentence in the
> language of syntax to an arithmetical sentence which is obviously
> equivalent to it (and this equivalence can straightforwardly be
> proved in any natural, though incomplete, system of syntax and arithmetic).

I will (seriously!) be glad to see this natural system of 
syntax and arithmetic in which this reduction can convincingly be
formalized. Can you give me any reference? (I am sure that I dont need 
to give you references to natural systems for second-order logic,
even weak second-order logic, in which the reduction of FTA you
have in mind can easily be proved).
 

Arnon Avron