[FOM] Godel Sentence

[Arnon Avron]

> In the case
> of e.g. PA I would claim that no formula not equivalent to the canonical
> Con(PA) can be held to "naturally express Con(PA)", so the question
> reduces to whether Goldbach's conjecture (or whatever sentence we pick)
> is provable equivalent to the canonical Con(PA) in PA.

Perhaps so. A proof?
 
>   We can certainly introduce logical formalisms in formulating a theory T
> which are not provably equivalent in T. But there is no apparent
> justification for regarding Con(T) and Con(T'), with these two different
> formalisms used, to be formulations of the same assertion.

So which of them (and why) is Con(PA), and what is the general criteia?
And what do you take as the Canonical PA (to say nothing about the
canonical Con(PA), of which I really dont know what you are talking
about, especially the "the" in this term).
 
>   >Of course both of them express properties of addition and 
>   >multiplication of natural numbers. But with the second nobody has to be 
>   >reminded about this fact, and nobody claims that it says something different
>   >from what it actually says. What I was protesting is your description
>   >of both as being of the same type of "coding".
> 
>   I didn't say anything about the same type of coding - I don't know of
> any such typology. My claim was only that "a Godel Sentence
> is a sentence in the language of elementary arithmetics that expresses
> a certain property of addition and multiplication of natural numbers"
> doesn't tell us anything about Godel sentences that doesn't apply
> equally to any formalization of a mathematical statement in the language
> of elementary arithmetic.

If you dont see the difference between a formalization
of  a mathematical statement
which is directly about the natural numbers, and  an arithmetical
sentance that can be thought of 
as a propsition about *syntax* only through some very particular choice of 
coding, then I can do nothing about it. I, for one, see no similarity whatever.
>  
>   >I dont think so, but of course if given a version in which it will not
>   >strike me that it is equivalent to FTA, then I will not say that it 
>   >is a sentence that express FTA, but only that it is a sentence
>   >which is equivalent to FTA -
> 
>   We are not "given" these enormous formulas at all, except through
> descriptions of the form "the translation into primitive notation of ...".

And this is another difference: we are not given a Godel sentence
as a "the translation into primitive notation of" but as a roundabout
*construction* that can be shown to be *equivalent in T* to 
a *code* for a translation into primitive notations (of what language?
English?) of a proposition concerning formulas of a certain formal language.

> If we introduce a terminology whereby a formula in the primitive
> language of PA expresses a certain statement A only if we recognize it
> as expressing A when presented with it, there will be very few cases
> of formulas in the primitive language of PA expressing anything at all.

??? Every formula of PA expresses exactly what it says, and recognition
that a formula expresses a certain statement is the most basic
pre-condition for using any formal system!
 
>   >In fact, also a Godel-sentence G is only *equivalent* to a sentence
>   >"expressing the unprovability of G" -
> 
>   The proof of Gödel's theorem only uses the fact that G is a fixpoint
> for "x is not provable in T", i.e. that such an equivalence is
> provable in T. However, we know of the existence of such fixpoints
> (Con(T) being another such) only through the diagonal construction,
> which yields a statement G that "says of itself that it is unprovable"
> in the sense of being the translation into primitive notation of a
> formula G of the form "t is not provable in T", where t is a closed
> term the value of which is (the Gödel number of) G.

Suppose this is an accurate description. Then what? 

> but I submit that
> there is no difficulty in formulating a theory, with the logical
> strength of arithmetic, in which the usual proofs of Gödel's theorem
> are "easily" formalizable.

Perhaps so (I doubt that it will be free from paradoxes). A proof?

Arnon Avron