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