[FOM] Is PA + ~Con(PA) a complete theory?
richard_heck at brown.edu
Tue Jun 4 18:17:40 EDT 2013
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
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.
More information about the FOM