[FOM] Godel Sentences

[Arnon Avron]

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

A much more relevant paper of Feferman (to the current discussion) is "Finitary
Inductively Presented Logics" (Logic Colloquium 88, pp. 191-220. Reprinted
in "What is a Logical System", ed. by D. Gabay, Oxford Science publication,
1994).  This paper seeks to achieve much more generality
than The "Arithmetization of metamathematics", and it includes the only 
serious attempt that I am aware of 
to construct a system (FS_0) directly including both the arithmetics of the 
natural numbers and the theory of syntax (believed to be such an
easy task by Torkel Franzen),  But as far as I can judge even Feferman 
FS_0 is not sufficient for the tasks I raised in my previous postings.
 
> 
> The Hilbert Bernays "derivability conditions" were weakened in an important
> paper by Robert Jerosolow, I think in the 1970's (perhaps a bit later),
> which I don't have at my fingertips.

The Hilbert Bernays "derivability conditions"  are sufficient conditions 
for the applicability of Godel's second theorem to a 
*given formalization*  Pr of the provability predicate
and the corresponding sentence Con_T (whose 
identity depends on the choice of the provability  formula Pr).
As such they are not very relevant to the questions I have raised. 

> 
> I think there are at least 20 good references for the whole business.
> 
> Here is a not very imaginative presentation. One can be more general and
> more slick and much more complete in details.
> 
> Let T be any recursively axiomatizable theory containing a small amount of
> arithmetic, and let a reasonable Godel numbering of sentences in the
> language be given. Also let a reasonable formalization within T of the
> notion of "n is the Godel number of a sentence in the language of T that is
> not provable in T".

Again, you are talking about a "reaonable formalization", while I am asking
for a precise mathematical characterization of this notion,
and for a proof that all the   Godel sentences that corrspond to any 
"reasonable formalization" are equivalent (though even their equivalence
is not enough for concluding that they "say the same thing". I shall
not repeat what I have written about this). 

> (The Hilbert Bernays derivability conditions are basic adequacy conditions
> on the above setup. Jerosolow worked out a substantially more elemental
> treatment, with weaker conditions).
> 

All these facts are well-known to everyone who knows something about the 
topic, and I really dont need to be reminded about them. For themselves
they are however totally irrelevant to the topic(s) of the discussion.


> For this purpose, a Godel sentence for T is a sentence A in the language of
> T such that the following holds. Let n be the Godel number of A. Then T
> proves 
> 
> A if and only if "n is the Godel number of a sentence that is not provable
> in T". 

And this "definition" again refer to "the" Godel number of A, while
no such thing exits. Every number can serve as a Godel number of any formula
under some "reasonable" formalization.  So what are you talking about
is (at best) " A Godel sentence for T relative to some encoding E" 

Note that according to your definition the corresponding Con_T(E)
is itself a "Godel sentence for T relative to E". Fine. This excludes
any talks about "the Godel sentence talking about itself".

Arnon Avron