What is the connection between provability logic & Gödel's first incompleteness theorem?

Question

Ive already asked this qustion on philosophy.SE

Provability logic is a modal logic that interprets the modal operator of K as provability and an additional axiom derived from Löb's theorem.

Now the SEP shows that it's possible to derive Gödel's 2nd incompleteness theorem from this setup. However, what is its connection with Gödel's 1st incompleteness theorem? It seems unlikely that this is contained within Löb's theorem, as this answered a question by Henkin about sentences that assert their own provability, whereas Gödel investigated sentences that asserted their non-provability.

Answer 1

As you say, you can get the second incompleteness theorem from the Hilbert-Bernays-Löb derivability conditions on the provability predicate (which are what are reflected in the modal "provability logic") together with the diagonalization lemma which tells us that there is a fixed point for 'not provable'. But you need the diagonalization lemma for the standard proof of the second theorem using the derivability conditions (no?).

And that diagonalization lemma, of course, will give you the first theorem almost immediately.