[FOM] T + ~Con(T) Refutes Its Goedel Sentence

[Richard Heck]

The purpose of this post is simply to make something explicit that 
emerged from the discussion last week of PA + ~Con(PA), and to correct 
something silly that I said.

The general observation, which is presumably well-known, but which I've 
never seen mentioned in the textbooks from which I've taught, is that, 
for sufficiently strong T, T + ~Con(T) proves the negation of that 
theory's Goedel sentence. This gives a nice example of why 
omega-consistency really is needed for Goedel's proof of the first 
incompleteness theorem and therefore of why Rosser's improvement really 
is an improvement.

To fill in a few details, let T be an r.e. theory containing R, and let 
G(T) be its Goedel sentence (for some choice of a provability 
predicate). Recall that Goedel's proof of G1 divides into two parts:

(i) If T is consistent, then T does not prove G(T).
(ii) If T is omega-consistent, then T does not prove ~G(T).

Let T~ be T + ~Con(T). Then since T~ is consistent if T is, T~ never 
proves G(T~), if T is consistent. However, since T~ is 
omega-inconsistent, Goedel's proof leaves open the possibility that T~ 
proves ~G(T). Which, as we shall now see, it will, if T is sufficiently 
strong (and "contains I\Sigma_1" will be more than sufficient).

Proof: As Arnon observed, if T is sufficiently strong, then T will prove 
G(T) <--> Con(T). Now T~ proves ~Con(T), trivially. But it also proves 
Con(T~) --> Con(T), almost equally trivially. So T~ proves ~Con(T~). But 
then, if T is sufficiently strong, so is T~, so T~ proves G(T~) <--> 
Con(T~) and so proves ~G(T~).

As I said, nothing terribly surprising, really, but a nice example.

Just historically: Does anyone know if this was known, say, before Rosser?

One related question: If I am not mistaken, the claims made right before 
the proof, that are central to G2, can be strengthened: If T is 
sufficiently strong, then T proves G(U) <--> Con(U), for ANY r.e. theory 
U. Right?

Richard Heck