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)

In a recent paper, Montagna proved the undecidability of the first-order theory of diagonalisable algebras. This result is here refined — the set of finitely refutable sentences is shown effectively inseparable from the set of theorems. The proof is quite simple.

(No abstract is available for this citation).