Let and be r.e. theories in the language of arithmetic. Assume that is strong enough to binumerate all primitive recursive relations. This suffices to prove the fixed point lemma:
For any formula there is a sentence such that ,
moreover, can be chosen of the same complexity as .
The (Löb) Derivability conditions for are the following three statements:
- For any , if , then .
For example, suffices for the proof of the fixed point lemma and of the first derivability condition and suffices for the other two.
Gödel incompleteness theorems:
- Let be r.e. and strong enough to satisfy the fixed point lemma and the first derivability condition. Let be r.e. and consistent. Then there is a true sentence such that does not prove . If is -sound, then does not prove either.
- If in addition satisfies the other two derivability conditions, then does not prove , the statement asserting the consistency of .
As a corollary, is essentially undecidable: Not only it is undecidable, but any r.e. extension is undecidable as well. Gödel’s original statement replaced -soundness with the stronger assumption of –consistency.