 The main “modal” result about provability logic is the fixed point theorem, which D. de Jongh and G. Sambin independently proved in 1975 (Sambin 1976). Even though it is formulated and proved by strictly modal methods, the fixed point theorem still has great arithmetical significance. It says essentially that self-reference is not really necessary, in the following sense. Suppose that all occurrences of the propositional variable \(p\) in a given formula \(A(p)\) are under the scope of the provability operator, for example \(A(p) = \neg\Box p\), or \(A(p) = \Box(p \rightarrow q)\). Then there is a formula \(B\) in which \(p\) does not appear, such that all propositional variables that occur in \(B\) already appear in \(A(p)\), and such that