 The modal logic K is valid in all Kripke models. Its extension GL however, is not: we need to restrict the class of possible worlds models to a more suitable one. Let us say that a formula \(A\) is valid in frame \(F\), notation \(F \models A\), iff \(A\) is true in all worlds in Kripke models \(M\) based on \(F\). It turns out that the new axiom (GL) of provability logic corresponds to a condition on frames, as follows: