[FOM] Is PA + ~Con(PA) a complete theory?

[Richard Heck]

On 06/04/2013 08:46 AM, Andrew Polonsky wrote:
> Let T be the theory obtained by adding to PA the axiom
>
> Incon(PA) = exists n. n is a code of a PA-derivation of Falsum
>
> Since T is a consistent c.e. theory extending PA, one would expect to 
> have undecidable propositions in it. Are there any known examples of 
> such propositions?

By Rosser's version of the first incompleteness theorem, the Rosser 
sentence for this theory is not decidable in it, unless the theory is 
inconsistent. Did you have something else in mind?

Here's an interesting question along these same lines: Does PA + 
~Con(PA) proves its own Goedel sentence (as opposed to its own Rosser 
sentence)? Goedel's version of the first incompleteness theorem does not 
tell us, since this theory is omega-inconsistent. (This is one reason 
that Rosser's version is a real improvement over Goedel's.) And one 
might think it should since, as you note:

> (The obvious candidate might be
> Con(PA + Incon(PA))
> However, the negation of the above statement can be derived from an 
> axiom.)

and, typically, the Goedel sentence for a theory is provably equivalent, 
in that theory, to the statement that the theory is consistent. But I'm 
not sure if this holds for omega-inconsistent theories. And I'm not near 
the appropriate references at the moment to look this up.

Richard