[FOM] Is PA + ~Con(PA) a complete theory?
meskew at math.uci.edu
meskew at math.uci.edu
Tue Jun 4 22:16:49 EDT 2013
> 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
More information about the FOM
mailing list