 In recent years, topological semantics for provability logic has seen a veritable revival, especially in the study of Japaridze’s bimodal provability logic GLB, an extension of GL (Japaridze 1986). The logic GLB turns out to be modally incomplete with respect to its possible worlds semantics, in the sense that it does not correspond to any class of frames. This feature places bimodal GLB in sharp contrast with unimodal GL, which corresponds to the class of finite transitive irreflexive trees, as mentioned above. Beklemishev et al. (2009) showed that GLB is, however, complete with respect to its topological semantics (see also Beklemishev 2009, Icard 2011). Intriguing reverberations of Esakia’s correspondence between GL and scattered topological spaces can even be found in recent topological studies of spatial and epistemic logics (see Aiello et al. 2007). (See  Section 5.4  for further discussion about GLB).