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?