# Are the HBL derivability conditions necessary for Gödel's incompleteness theorems? (For Löb's theorem?)

I've been working through a textbook, often encountering difficulties with the exercises. On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution.

As I understand, they might be not ideally phrased, but I don't know what should be changed, or I don't see a good possibility to rewrite them. If you miss some background information, I will try to provide it.

If it would cost too much time, maybe you like to leave hints for (better/more detailed) solutions or general, short descriptions how the solution 'looks like'.

In future I'll try to write in a way that can more easily be answered. Of course nobody should feel forced to answer, in the past it seemed people sometimes feel that way, to my surprise.

Here's a copy:

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?

Thanks,

Ettore

• By the fifth use, the phrase "in future I'll try to write in a way that can more easily be answered" is mostly an empty promise. It may be easier to ask in a way that gets answers by asking only one or two questions at a time. – Matt F. Dec 28 '18 at 15:45
• @MattF. I think it depends, Matt. I had a number of unsolved questions on mathstackexchange, so I wanted to copy them on mathoverflow. I didn't even copy all of them, only a few. I didn't see a reasonable way to rewrite them, although in the meantime I understood a bit why they where not answered yet, so I posted them like this. By the 'future' so I mean the really new questions I will have one day. Still I see your point. I'll do my best. Thanks for commenting! – Ettore Dec 30 '18 at 12:03