[FOM] Godel Sentences

[Harvey Friedman]

Response to Avron and also others who have been writing about Godel's
theorem recently on the FOM.

I have already answered Kanovei, I guess satisfactorily, because he has not
since responded. 

All such issues raised have long been resolved - decades ago. I'm sure that
Godel knew exactly how to handle them already in the 1930's. One has to be
creative to think of some issue that needs to be addressed that hasn't
already (see below).

On 8/26/03 4:56 PM, "Arnon Avron" <aa at tau.ac.il> wrote:

> Harvey Friedman writes:
>> 
>> The well known demonstrable provable equivalence of all Godel sentences of
>> any reasonable theory within that same theory is perhaps implicit in Godel -
>> at least for PA - probably explicit in Hilbert Bernays, and surely given a
>> modern polished treatment in
>> 
>> S. Feferman, Arithmetization of metamathematics in a general setting,
>> Fundamenta Mathematicae 49, 35-92, 1960.
> 
> This is simply FALSE. Please read Feferman's paper again and you will see
> that everything he is doing there is *relative to a given method* of
> coding (the one that Feferman is using there for the sake of definiteness
> is not very efficient, in fact  - Smullyan's method is far better -
> but this is really not a significant matter). Feferman does
> not discuss at all (in this paper, at least) the relationships between
> consistency statements corresponding to two different methods of encoding
> the syntax, or two different proof systems for PA (say).
> The general setting  is in allowing different
> ways of enumerating the axioms of a theory T (given all the other factors).

I'll take your word for it about Feferman, but the whole matter is quite
trivial, and from my personal experience COMPLETELY KNOWN to Feferman
probably in the 50's.

In particular, it is well known how to give very minimal conditions on an
encoding of syntax so that any Godel sentence relative to any such encoding
is equivalent to any Godel sentence relative to any other encoding. This is
most well known and most obvious in the case of extensions of PA = Peano
Arithmetic. 

The conditions needed are extremely weak and well known. End of story!?

Now for the creative objection.

One can insist that it is not reasonable to have any numbering of formulas
at all. One should just talk directly about them, with no intermediary. So
in particular, any system that only talks about numbers has no formalization
of its consistency, in this sense.

This is also handled by Jerosolow. I have already indicated ways to handle
this objection on the FOM some time ago.

Harvey Friedman