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

Richard Heck richard_heck at brown.edu
Sun Jun 9 11:05:29 EDT 2013

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

```