FOM: Truth of G

[Arnon Avron]

In the message below I'll try to clarify once more things as I see them.
This, however, will be my last message on the subject.
 
> RE: Please see my first posting. There I myself emphasized that 
> the argument begins : ASSUME that T is consistent. One the 
> derives G. Hence, informally: T is consistent -> G.  
> (Formalizing this in T, one gets: Cons(T) -> G.) 

No. To my opinion this is a confusion of claims in the formal language of
T and in the metalanguage of T. Godel has proved that:

1) The sentence "Cons(T) -> G" (in the language of T) follows from T
   (and so, one can add, this sentence is true in all models of T).
2) "If T is consistent then G is true in the standard model of T"
   (This is a proposition in the metalanguage of T).

As for the hybrid "T is consistent -> G", I dont understand in what 
language this is written (unless you take the formal language to be a 
part of the metalanguage) and especially I dont understand
what it can possibly mean if by "G" you mean here something 
different than "G is true in the standard structure for T".
In general, I know two possible interprtations of "deriving a sentence A".
One is that A has been derived (or shown to be derivable) in some
axiom system T. The other is that A has somehow been shown to be true
in some structure. Your  "T is consistent -> G" has not been "derived"
according to either interpretation.

> If one then wants to prove G, it is sufficient to assume ... that T is 
> consistent, i.e. one cannot derive a contradiction in it.  By Modus 
> Ponens, one gets G. See, no models, standard or not ...

Again, it is beyond me what you mean here by "proving G". If 
in the background there is neither a formal theory, nor a specific 
structure then this is a meaningless expression.
 
> By the way, how on earth it is easier to prove in T, or in any theory, 
> "G is true" than G ?

In T one may try to prove G. In the metatheory one may try to prove that
"G is true". It is meaningless to try to prove "G is true" in T
(unless a truth definition for the language of T is available in that language,
and even in this case I have reservations).
 
> One should note that one can G_delize a highly non-sound theory 
> (extending Q) which does not even have a standard model - as long 
> as one assumes it is consistent (in the proof theoretical sense). 

T might not have a standard  model, but its Godel sentence G (which is
in the language of PA) does: the standard model of PA. And the claim 
that if T is consistent then G is true refers to this standard model. 

 By the way, I would prefer to talk about the "standard interpretion"
or the "standard structure" rather than the "Standard Model". The
word "model" usually means "model of some theory T" (though
regretably it is used in many textbooks as a synonym for "structure").
The Godel sentence of a consistent but unsound theory might be false
in any model of T, but it is true in the standard structure for the 
language of PA, and only in this sense one may claim that "if T is
consistent then G (is true)". Perhaps part of the misunderstanding
between us is caused by the double use of the word "Model".


> PLEASE NOTE: I did not intend to attack the notion of standard 
> model of PA - I personally find it well-defined and acceptable. 
> Further, I think that model-theoretic considerations greatly 
> illuminate what is really going on in G_del's theorem. 
>     My point was just to emphasize that G_del's proof does not as 
> such assume the notion of the standard model and truth in it  - 
> G_del took great pains to avoid it, in order to convince even those 
> who had postivistic, formalistic or finistitic convictions. 

Godel itself used the notion of omega-consistency, which to my
opinion assumes the totality of the natural numbers. Rosser's version
can indeed be formulated without any reference to truth in any first-order
structure for the language of PA (but the claim "T is consistent" 
itself assumes in fact
the infinite totality of all sentences of T and proofs in T,
with the standard interpretation
of "p is a proof of A" etc, so I dont see what is exactly gained by 
avoiding a reference to the standard interpretation of the language
of PA).

Arnon Avron