Solution

ID: past-exam-of-the-model-theory-and-godel-s-incompleteness-theorems-course-of-the-university-of-oxford/2009/a/1/b/solution

The Hilbert-Bernays-Löb derivability conditions are: if then ; ; and . The first is an external rule about provability; the latter two are internal theorems. Standard numerical correctness and the stipulated form accompany the predicate in this question. These conditions do not include reflection .
Choose a fixed refutable sentence and identify with . Different fixed refutable choices have provably equivalent consistency sentences, because proves their equivalence to a contradiction. From , necessitation and distribution give . Since , this yields .
For the converse, necessitate and distribute to get . Positive introspection also gives . The two boxed contradictories imply by formalized propositional reasoning. Thus , and contraposition gives . Consequently
Finally the deduction theorem says that is inconsistent exactly when . The internal equivalence identifies and in their deductive consequences. Hence exactly when is consistent. Consistency of alone need not ensure this stronger consistency condition.

New to topics? Read the docs here!