 The modal completeness theorem by Segerberg was an important first step in Solovay’s proof of arithmetical completeness of GL with respect to Peano Arithmetic. Suppose that GL does not prove the modal formula \(A\). Then, by modal completeness, there is a finite transitive irreflexive tree such that \(A\) is false at the root of that tree. Now Solovay devised an ingenious way to simulate such a finite tree in the language of Peano Arithmetic. Thus he found a realization \(f\) from modal formulas to sentences of arithmetic, such that Peano Arithmetic does not prove \(f(A)\).