Even though "provability logic" did not come into its own until the early seventies, it has its roots in two older fields: metamathematics and modal logic. In metamathematics, we study what theories can say about themselves. The first—and most outstanding—results are Kurt Gödel's two incompleteness theorems.

If we take a sufficiently strong formal theory T—say, Peano arithmetic—we can use Gödel numbering to construct in a natural way a predicate Prov(x) in the language of T that expresses "x is the Gödel number of a sentence which is provable in T." About T we already know that it satisfies modus ponens:
If it is provable that A implies B, then, if A is provable, B is provable as well.

Now it turns out that, using Gödel numbering and the predicate Prov, we can express modus ponens in the...