This post works through some technical details in the Gödel-Löb provability logic , especially as they are relevant to a paper by LaVictoire et al discussed in the previous post. Subsection 4.2 of that post explores as a useful tool for the task at hand, deferring some standard technical details until this post.

After reviewing some definitions in Section 1, Section 2 covers the normal form theorem, from which it follows that sentences of without propositional variables can be algorithmically classified as true or false in the standard model of arithmetic. By contrast, the Kripke semantics covered in the final Section 4 allows any formula (with or without variables) to be algorithmically classified as provable or unprovable in . My main source for these sections is George Boolos’ *The Logic of Provability*.

(Another point of contrast: Solovay’s completeness theorem, which we do not cover here, establishes that the formulas proved in are exactly those which whose every instance is provable in Peano Arithmetic, with propositional variables replaced by Gödel numbers of arithmetical sentences, and the modality replaced by ‘s provability predicate. It is the right-to-left implication that is non-trivial.)

Section 3 gives Per Lindström’s simple proof of the fixed point theorem for as in his article *Provability Logic: A Short Introduction*. The fixed point theorem is analogous to Gödel’s diagonal lemma for constructing self-referential sentences, and is actually the main result needed by LaVictoire et al.