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 S\vdash(\varphi\leftrightarrow\gamma(\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 T\vdash\varphi, then S\vdash{\rm Pr}_T(\varphi).
  • S\vdash\forall\varphi,\psi\,({\rm Pr}_T(\varphi\to\psi)\land {\rm Pr}_T(\varphi)\longrightarrow{\rm Pr}_T(\psi)). 
  • S\vdash\forall\varphi\,({\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 T\vdash 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 \lnot\varphi 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.

Advertisements

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: