But right now I'm poking through "Modal Logic" by Blackburn, de Rijke, and Venema in E&S. I like the presentation style a lot. It's very thorough and careful. There's a lot of meat in chapter 4, with various completeness theorems and such. I think I will have to check it out.

---

Ooh! A lucky find searching for Löb's theorem, paper #5 therein looks suspiciously and interestingly 2-categorical.

---

If you're thinking to yourself, "What the hell is Löb's theorem, and what does it have to do with modal logic?", and I'm sure you are, here's the answer I just found, distilling down from these notes here. Well, the connection to modal logic isn't in those notes, it's from the book I mentioned above. If you add the axiom

[]([]p -> p) -> p

to the modal logic K, it is weakly complete with respect to frames which are finite transitive trees, and it conspicuously

*isn't*strongly complete for any class of frames. What this funny-looking axiom is, is the translation of Löb's theorem into modal logic, where box is provability. That is, the theorem says that if, reasoning in some formal system, we can prove that p being provable implies p, then in fact p holds.

How do we prove this? One way is via Gödel's second incompleteness theorem. Remember that it says that a system is consistent just in case it doesn't prove its own consistency. So let's take a p, and assume []([]p -> p) (that is, assume we have a proof of provable-p implies p) and adjoin the negation of p to whichever system S we were working in in the first place, and think about the system S+~p. Now S proved that []p -> p, so certainly S+~p does also. What's the contrapositive of that implication? Hmm, S+~p proves ~p -> ~[]p. And S+~p has ~p as an axiom. Uh-oh! That means that S+~p proves ~[]p. Remember that []q in general means S proves q, so what S+~p is telling us is that S can't prove p. In other words, adjoining p's negation can't result in a contradiction. S+~p proves its own consistency! So it must, by Gödel's 2nd, be inconsistent. A proof of falsehood from S+~p is tantamount to a proof of p from S, so we're done.