From: Geoffrey Norman Watson 
Date: Mon, 2 Dec 1996 10:44:11 +1000
Organization: Computer Science Dept, University of Queensland



On 27 Nov 1996, Torkel Franzen wrote:

> Geoffrey Norman Watson  writes:
> 
>   >I believe that detailed versions of Goedel's second incompleteness theorem
>   >exhibit quite specifically the sentences which are true but which cannot
>   >be proved in the relevant system. Their truth is established by the law of
>   >the excluded middle and the meta-level relationship between statements 
>   >of arithmetic and sentences of the theory defined by the Goedel encoding.
> 
>   Your belief is mistaken, since the Godel sentence is sometimes false
> rather than true.
> 
  Reference to "THE Godel sentence" is a little misleading.  I have never seen
  Goedel's paper, presumably this specifies a sentence to which this description
  applies, but the theorem itself can be proved in a number of different ways, 
  using different sentences.

  For instance, Boolos and Jeffrey in "Computability and Logic" use a sentence
  equivalent to "we cannot prove that 0=1", since they are mainly concerned 
  with the consistency of arithmetic.  Whereas, if I recall correctly, Kleene
  in his textbook uses a more complicated sentence that "asserts its own 
  unprovability", since he is more concerned with general issues of provability
  and truth.

----------------------------------------------------------------------------
    Geoffrey Norman Watson                         gwat@cs.uq.edu.au