117b – Undecidability and incompleteness – Lecture 9

Let S and T be r.e. theories in the language of arithmetic. Assume that S is strong enough to binumerate all primitive recursive relations. This suffices to prove the fixed point lemma:

For any formula gamma(x) there is a sentence varphi  such that Svdash(varphileftrightarrowgamma(varphi)),

moreover, varphi can be chosen of the same complexity as gamma.

The (Löb) Derivability conditions for S,T are the following three statements:

  • For any varphi, if Tvdashvarphi, then Svdash{rm Pr}_T(varphi).
  • Svdashforallvarphi,psi,({rm Pr}_T(varphitopsi)land {rm Pr}_T(varphi)longrightarrow{rm Pr}_T(psi)). 
  • Svdashforallvarphi,({rm Pr}_T(varphi)to{rm Pr}_T({rm Pr}_T(varphi))).

For example, S={sf Q} suffices for the proof of the fixed point lemma and of the first derivability condition and S={sf PA} suffices for the other two.

Gödel incompleteness theorems:

  1. Let S be r.e. and strong enough to satisfy the fixed point lemma and the first derivability condition. Let Tvdash S be r.e. and consistent. Then there is a true Pi^0_1 sentence varphi such that T does not prove varphi. If T is Sigma^0_1-sound, then T does not prove lnotvarphi either.
  2. If in addition S satisfies the other two derivability conditions, then T does not prove {rm Con}(T), the statement asserting the consistency of T.

As a corollary, {sf Q} is essentially undecidable: Not only it is undecidable, but any r.e. extension is undecidable as well. Gödel’s original statement replaced Sigma^0_1-soundness with the stronger assumption of omegaconsistency.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: