[FOM] Godel Sentence

[Torkel Franzen]

Arnon Avron says:

  >Your talk
  >about "any standard version" hides (I believe) the assumption that 
  >all the sentences that might be obtained by some "standard version"
  >are provably equivalent (in T, I guess).

  No, I was proposing a definition, not assuming anything. (As long as
the Sigma-formula defining the axioms of T is not fixed, we know that
the resulting Con(T) are not in general equivalent in T.) I make no
claims for the usefulness of my proposal.

  I have no contribution to make to the quest for a definition that would
allow us to decide whether there is any ground for assuming that
e.g. Goldbach's conjecture cannot be equivalent to a sentence which
we may take as naturally expressing Con(T). We know that Goldbach's
conjecture is equivalent in T to a Con(T) if we are allowed to choose
(unnaturally) the Sigma-formula defining the axioms of T. 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.

  >For example, suppose that we take as the underlying proof systems
  >Gentzen's formalizations of PA in which induction is a rule rather
  >than an axiom. There is a version with the cut rule, and another
  >one in which only inessential cuts are allowed. I think that both
  >can be justly used for "standard versions". Will the resulting sentences 
  >expressing the consistency of T be equivalent in T?

  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.

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

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

  >I will (seriously!) be glad to see this natural system of 
  >syntax and arithmetic in which this reduction can convincingly be
  >formalized. 

  The only actual formalization of syntax that I know of is Quine's
(in an appendix to his book _Mathematical Logic_), 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.

---
Torkel Franzen