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. Aug 18, 2013 at 7:43

3 Answers 3


(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).

  • 1
    Great! It's as clean and understandable as you suggest. Jul 26, 2015 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)
[](p <-> ~[]_|_),
and if []p, then:
[]~[]_|_, then
[]_|_, while if []~p, then
[]~~[]_|_, that is: [][]_|_


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). Aug 24, 2013 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, 2013 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. Aug 25, 2013 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, 2013 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.

So, the answer is yes.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .