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
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
Only the first condition is necessary for the first incompleteness theorem. (Gödel did in practice use a version of it)
All three are used in standard derivations of the second incompleteness theorem, but Jeroslow 1973 invented a trick which allows to drop the third (it the Wikipedia listing): Thus only 1-2 are really necessary.
See Section 3.2. in: https://plato.stanford.edu/entries/goedel-incompleteness/