  holds. However, there is no realization which makes all  three \(\Box\) s in (5) explicit. In fact, the set of  realizable provability principles is the intersection of  \(\mathsf{GL}\) and  \(\mathsf{S4}\) (Goris 2007).