[FOM] Godel Sentence

[Torkel Franzen]

Arnon Avron says:

  >Perhaps so. A proof?

  Sorry, I don't follow - a proof of what?
 
  >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).

  In speaking of PA, we usually have in mind a first order theory, with
one of several standard (by which I only mean commonly used) formalizations
of predicate logic and a collection of axioms. These axioms have a
canonical description - a formula is an axiom if it is one of the formulas
A1,..,An or an instance of the induction schema - and we get a canonical
formalization of "PA is consistent" by a straightforward formalization of
"no contradiction can be derived from the axioms using predicate logic".
The various Con(PA) obtained in this way, using any of the standard
(again, commonly used) arithmetizations of syntax, are equivalent in PA.

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

  What is "less particular" about a choice of representation of finite
sequences and sets of natural numbers as numbers, or a representation
of numbers of various kinds as sets?

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

  I don't know what you have in mind in speaking of a "code for a translation".
A Godel sentence (in the language of PA) is the translation into primitive
notation of a formula G' in an extension by definitions of PA. This G'
is a straightforward formalization of a mathematical statement about the
syntax of PA.

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

  It's unclear what you have in mind here. Obviously we don't
recognize anything about what an enormous formula of PA expresses,
given such a formula in primitive form. Is it possible for a formula
in the primitive language of PA to express the fundamental theorem of
arithmetic? If so, what does this mean? (What I take it to mean is
that it is the translation into primitive notation of a formula in an
extension by definitions of PA that we recognize, on the basis of our
knowledge of arithmetic, as a formalization of the fundamental theorem
of arithmetic.)
  
  >Suppose this is an accurate description. Then what?

  A Godel sentence G is in fact not "only equivalent" to a sentence
expressing the unprovability of G. It intensionally expresses "G is
unprovable in T", whereas Con(T) does not intensionally express "Con(T) is
unprovable in T", even though it is equivalent in T to "Con(T) is
unprovable in T".

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

  Here I'm puzzled. What difficulty do you see that I'm missing?

---
Torkel Franzen