# 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.

• minor typo: should be Lob's theorem. – Hunan Rostomyan Aug 18 '13 at 7:43

(2 years later) I stumbled across a very nice and clean answer, here goes:

First, let's suppose arithmetic is consistent. If it isn't, Gödel/Rosser is trivially valid since their result is of form "if PA is consistent, then ...".

Assume that you can prove F, or prove ¬F, for each formula F (contrary to Gödel/Rosser's theorem).

If you can prove a certain arbitrary but fixed formula F, then you can also prove Bew([F]), Bew being the standard provability predicate and [] coding (meta)operator. If you can prove ¬F, then you can prove Bew([¬F]). Thus, regardless whether F is provable or ¬F is provable, you can prove (Bew([¬F]) or Bew([F])) for each formula F.

But by Solovay's completeness theorem for provability logic (system GL), formula ([]F or []¬F) should then be a theorem of GL. However, it isn't. Counterexample Kripke model: l[p] <- w -> r[¬p], model is transitive and converse well-founded, but w |=/= ([]p or []¬p).

• Great! It's as clean and understandable as you suggest. – Mozibur Ullah Jul 26 '15 at 15:46

edit: see my other answer (below or above this one).

The second theorem would actually be (ASCII art since we lack LaTeX here):

``````GL |- ~[]_|_ => GL |- _|_,
``````

and not what SEP gives a proof of, which is:

``````GL |- []~[]_|_ -> []_|_
``````

which is actually a "formalized" version of the second incompleteness theorem (PA talking about itself, again). I don't think the first version given above makes any sense (the "actual" 2. I. T.), since we know `GL |-/- _|_` (that is, that GL is consistent)

So, my guess is that the best you could look for in GL is a formalized version of the first incompleteness theorem.

Perhaps this is a good place to start (the formula below is indeed a theorem, you can check that by trees or direct proof given in Boolos' The Logic of Provability):

``````GL |- [](p <-> ~[]p) -> [](p <-> ~[]_|_)
``````

Which can be (roughly) translated as "If (it's provable that) P says that P is unprovable, then P is provable if and only if you can prove consistency".

``````If you assume:
[](p <-> ~[]p)
then
[](p <-> ~[]_|_),
and if []p, then:
[]~[]_|_, then
[]_|_, while if []~p, then
[]~~[]_|_, that is: [][]_|_
``````

So:

``````GL |- ([](p <-> ~[]p) && ([]p or []~p))  -> ([]_|_ or [][]_|_)
``````

Perhaps there is even a more direct way to represent the first theorem, I'm not sure. (This would have been a comment if I was allowed to post one. :) ).

• apparently there is :), see my answer (which isn't mine but Peter Smiths). – Mozibur Ullah Aug 24 '13 at 20:31
• If I understood his answer correctly, that's exactly the method I used above (the theorem above states that if P is a fixed point for ~[], in other words if P is a Gödel sentence for PA, than if either P or ~P is provable, either []_|_ or [][]_|_). I'll post a comment there just to be sure! – Luka Mikec Aug 25 '13 at 22:21
• @Mikec: Ok, I just found the ascii 'art' a little bit confusing since modal logic is not something I'm comfortable with, though appreciate there is no latex facilities here. – Mozibur Ullah Aug 25 '13 at 23:14
• No problem (I'm still not sure, we'll see). Btw Peter Smith wrote a great intro to these topics, it even includes a bit of GL: logicmatters.net/igt/further-notes/godel-without-tears – Luka Mikec Aug 25 '13 at 23:24

According to this answer by Peter Smith:

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.