FOM: Truth of G
Raatikainen Panu A K
Praatikainen at elo.helsinki.fi
Mon Nov 13 03:59:41 EST 2000
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
More information about the FOM
mailing list