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

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.

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.

• Would this be the first incompleteness theorem, formalized in GL (provability logic)? (_|_ falsum, [] box) ([](p <-> ~[]p) and ([]p or []~p)) -> ([]_|_ or [][]_|_) It definitely is a theorem of GL, but tbe [][]_|_ part is a bit weird; does it have to do with the omega-consistency requirement? If yes, which I assume is the case since ([](p <-> ~[]p) and []p) -> []_|_ is also a theorem of GL (and the omega consistency is for the []~p part), could that requirement be spelt out within the GL (and inserted into the antecedent of the formula above) so that the formula ends with []_|_? Commented Aug 25, 2013 at 22:34