1. Below we will present a more detailed proof sketch of GL \(\vdash \Box\Diamond A \rightarrow \Box B\), a simple but surprising theorem that was suggested to us by Nils Kurbis. Let us first gather some ingredients. Note that in the modal logic K, so certainly in GL, we have that for each formula \( C \), the two formulas \( C \rightarrow \bot\) and \(\neg C\) are logically equivalent and may be replaced by each other. The same holds for the two formulas \(\Diamond C\) and \(\neg\Box\neg C\). Moreover, by the Generalization Rule, the Distribution Axiom, and the Modus Ponens rule, we have the following derived rule for all formulas \(C, D\): If GL \(\vdash C \rightarrow D\), then GL \(\vdash \Box C \rightarrow \Box D\). Here follows the promised proof sketch.

1. GL \(\vdash \bot \rightarrow \neg A\) (tautology of propositional logic)
2. GL \(\vdash \Box \bot \rightarrow \Box\neg A\) (from line 1 by the derived rule above)
3. GL \(\vdash \bot \rightarrow B\) (tautology of propositional logic)
4. GL \(\vdash \Box\bot \rightarrow \Box B\) (from line 3 by the derived rule above)
5. GL \(\vdash \Box(\Box \bot \rightarrow \bot) \rightarrow \Box\bot \) (axiom GL)
6. GL \(\vdash \Box(\Box \bot \rightarrow \bot) \rightarrow \Box B \) (from lines 4, 5 by hypothetical syllogism)
7. GL \(\vdash \Diamond A \rightarrow (\Box \bot \rightarrow \bot) \) (from line 2 by contraposition and the above-mentioned equivalences)
8. GL \(\vdash \Box\Diamond A \rightarrow \Box(\Box \bot \rightarrow \bot) \) (from line 7 by the derived rule above)
9. GL \(\vdash \Box\Diamond A \rightarrow \Box B \) (from lines 6, 8 by hypothetical syllogism).

Note that semantically, it is easy to see that the formula \(\Box\Diamond A \rightarrow \Box B \) is valid on transitive, conversely well-founded frames (see Section 3). After all, each formula of the form \(\Box\Diamond A\) can only hold in the end-points of transitive, conversely well-founded frames; and in all the end-points of such frames, we also have \(\Box\bot\), and therefore \(\Box B\) for every formula \(B\).

2. It turns out that almost the same counterexample works for intuitionistic provability logic, even for the version without \(\Diamond\), which was proved by Ian Shillito (2023, Theorem 13.2.1). As suggested by Rosalie Iemhoff, one only needs to replace each \(\Diamond\) in the example above by \(\neg\Box\neg\).

3. Holliday and Litak (2019) strengthened this result by showing that GLB is not only Kripke frame incomplete, but even incomplete with respect to Boolean algebras for which the \(\Diamond\) operator is completely additive, that is, for any set \(X\) of elements, if \(\bigvee X\) exists, then \(\bigvee\{\Diamond x \mid x \in X \}\) also exists and \(\Diamond\bigvee X = \bigvee\{\Diamond x \mid x \in X \}\). One of the nice aspects of their result is that the bimodal provability logic GLB is the first naturally occurring modal logic that shows such incompleteness with respect to completely additive Boolean algebras. Note that the logic that Van Benthem (1979) originally used to show the existence of a modally incomplete logic was also a (slightly artificial) variation on provability logic, namely, \(K\) with the extra axiom \(\Box\Diamond\top\rightarrow \Box(\Box(\Box p \rightarrow p) \rightarrow p)\), a weakening of GL.