FOM: Truth of G

[Raatikainen Panu A K]

Avron's last posting raises some deep and difficult problems on the 
meaning of formalized languages.

I think that Avron points out some very good questions, at least. I agree 
with some of his comments, but disagree with others. I'll try to clarify both 
sides. 

Avron is not happy with my formulation "T is consistent -> G". 
He writes:
 
> 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)

PR: 1) Unfortunately I must disagree, for Goedel simply did not, in 
his proof of his FIRST theorem (1931), prove Cons(T) -> G, for this 
assumes that consistency has been formalized, and amounts to a 
proof of Goedel's second theorem - the latter requires the 
derivability conditions and raises the tricky question on "what it is 
for a formula to really express consistency"  (and that is why I tried 
to avoid the whole issue and used only the informal "T is 
consistent"). Such a proof was carried through only by Bernays 
(with some hints from Goedel) in the second vol. of 
Hilbert&Bernays (1939). I think that there are still many 
unanswered question concerning the latter issue (as Avron 
suggested in his earlier posting, if I interpret him correctly), but 
Goedel's first theorem is free from them. Its proof proceeds 
informally. One assumes that the basic proof-theoretical notions 
(derivation, derivability, theorem, consistency) are well-understood, 
and proceeds by assuming that T is consistent, and concludes 
that G. (This is admittedly a very rough description)

I also disagree that Goedel proved, in the metatheory, that
>  2)  "If T is consistent then G is true in the standard model of T"
>    (This is a proposition in the metalanguage of T).
Goedel himself never went of to formalize his proof in a metatheory. 
This has been done by Bernays, Loeb, Feferman, Smorynski, etc. 
But there is no mention of the standard model in any of these 
proofs.  
     If one formalizes the proof of Goedel's first theorem in a 
metatheory MT, one obtains either (only now; the above mentioned) 
Cons(T) -> G, 	 if MT is an extension of T;  or:
Cons(T) -> #G,  where #G is the translation of G in L(MT). 

MT might be, e.g., Second order arithmetic Z_2 or ZFC.

By the way, I don't find any problems in the case where L(T) is a 
part of L(MT); on the contrary, I think this is the most natural case.  
  
>   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".

PR: Certainly it can be argued that they have a different meaning. 
An arithmetical formula "(x) Ax" states a general fact about 
numbers, whereas "the sentence '(x) Ax' is true in the standard 
model" expresses something about the relation between a 
syntactical entity (formula) and a abstract mathematical structure. 
It would take us far to far to philosophy to pursue this truth issue 
properly, but I think this is enough to point out that they do not 
obviously mean the same ... 

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

PR: I borrowed this "proving G" from Avron's earlier posting - I did 
not intend it in the sense of "derivability in a formalized theory". But 
anyway, Avron's claim seems to be too strong, for it seems to 
imply that Goedel  did not (nor any standard proof of Goedels first 
theorem does) really establish G's truth, for he did not present 
explicitly a formalized metatheory but proceeded informally. 

But I think that it must be just admitted that Goedel managed to 
establish G (assuming the consistency of PA) informally, without 
either a strictly formalized metatheory or the notion of the standard 
model. 
 
> > 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).


PR: My remark referred to Avron's earlier, puzzling passage which 
went as follows:

> AVRON:  "What the pure proof-theoretical argument 
demonstrates is not G, but Con(T)->G. If one wants to go on and 
prove G (more accurately,  that G is *True*, because G cannot be 
proved in T) then I dont see how this can be done without
a reference to the standard model of T. "

I still find this statement most puzzling. His later remark makes 
more sense, but I still disagree. Fo certainly one can prove, in the 
metatheory, just G (or #G), instead of the much more involved "G is 
true in the standard model". Avron appears to think, for some 
reason, that the former is somehow impossible. 

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

PR. the basic point is correct, by there is a minor error: the Goedel 
sentence of T need not be in the language of PA ; that is, G (for T) 
is always in the language of T. But presumably Avron means that it 
can be interpreted as an arithmetical statement; and this is, of 
course, true. G is always, after such an interpretation, a Pi-0-1 
sentence.  

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

PR: The questions on what commits one to the totality of the 
natural numbers are difficult and deep, and highly controversial. I 
am myself less convinced that these notions in itself commit one 
to the standard structure of natural numbers ...
     It is indeed true that in a sense, the theory of basic syntax is 
equivalent to an elementary theory of arithmetic. But this is much 
weaker than PA. And if one then thinks that e.g. PRA  (and even 
HA) commits one only to the potential infinite (this is the received 
view), and only PA  to the completed, actual infinite, then one may 
think that these syntactical notions are on more safe grounding 
(than the notion of the standard model). And for all those who think 
so, Goedel's proof can be presented without any mention of the 
standard model - assuming these notions as definitely understood.
	If, on the other hand, one believes, as Avron does, that already 
these elementary proof-theoretical notions commit one to the 
existence of completed, actual infinite, there is indeed little point in 
prefering the proof-theoretical approach and avoid the model-
theoretical approach. I think that this is a consistent and perfectly 
respectable view for which can be argued. But it is good to see 
clearly the background assumptions of these differing views. 
    On the whole, I think that these issues have been insufficiently 
discussed in the literature of the field. Therefore I am grateful for 
Avron for presenting his views. Although I disagreed on some 
details, I hope that these final remark here have clarified where the 
source of the difference of views, in my mind, actually is.

Panu Raatikainen
Department of Philosophy
University of Helsinki