Each closed (i.e. variable free) formula of interpretability logic is equivalent in ILF to a closed formula of the provability logic G, thus to a Boolean combination of formulas of the form n.

The proof of the Second Incompleteness Theorem consists essentially of proving the uniqueness and explicit definability of the sentence asserting its own unprovability. This turns out to be a rather general phenomenon: Every instance of self-reference describable in the modal logic of the standard proof predicate obeys a similar uniqueness and explicit definability law. The efficient determination of the explicit definitions of formulae satisfying a given instance of self-reference reduces to a simple algebraic problem-that of solving the corresponding fixed-point equation (...) in the modal logic. We survey techniques for the efficient calculation of such fixed-points. (shrink)