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

[meskew at math.uci.edu]

> 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 Church's theorem, if T is a consistent recursive extension of
Robinson's Q, then the set of Godel numbers of theorems of T is not
recursive.  If T is complete and recursive, then the set of theorems of T
is recursive, as witnessed by the following function:  Given a number of a
sentence n, exhaustively search for a proof that decides n. If the first
one found proves n, return 1, and if the first one found proves not-n,
return 0.  Hence any consistent recursive extension of Q is incomplete.

Your question asked for an example, so let's construct one.  Godel's fixed
point lemma gives a way of constructing from any formula R(x), a sentence
S such that Q proves (S iff R(#S)).  Assume T is a consistent recursive
extension of Q, and let F be the partial recursive function described in
the previous paragraph that searches for a proof or disproof of n in T and
halts at the least one.  Let P(n) be the statement: "F(n) = 1."  Let S be
given by the fixed point lemma with respect to not-P(n).

If T proves S, then F returns 1 on #S, so Q proves P(#S) and thus not-S. 
If T proves not-S, then F returns 0 on #S, so Q proves not-P(#S) and thus
S.

Either case results in contradiction, so S is independent of T.

-Monroe