I am currently working with 'proof theory and logical complexity', a monograph on proof theory.

In the exercises of the first chapter one was asked to prove Löb's theorem (https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem) and two related/similar statements. (The first chapter essentially gives the setup to prove and proves both incompleteness theorems and some results around them.)

Searching the internet I came across the Hilbert-Bernays-Löb 'derivability conditions' (https://en.wikipedia.org/wiki/Hilbert%E2%80%93Bernays_provability_conditions), that are - apparently - necessary to prove Löb's theorem.

The author never mentions them explicitly, and while the first is very plausible and the second not unplausible, I read that the third's proof is tedious and difficult.

The author never gives a proof for them, and I don't recall that one would have been needed, so I ask myself whether it is possible to prove the incompleteness theorems without them, or if they follow easily from some result, especially since Löb's theorem is in this case an exercise, and would be quite hard if the author intends the student to have the idea and the proof of the derivability conditions all by himself. Or maybe Löb's theorem is itself provable without them?



PS: I added the question also on mathoverflow: https://mathoverflow.net/questions/319402/are-the-hbl-derivability-conditions-necessary-for-g%C3%B6dels-incompleteness-theorem


Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.