Provability logic studies the properties of a formal provability predicate $\Box F$ interpreted as ‘F is provable’. This gives rise to modal logics kindred to K4 and its variations.

For the best known of these systems, the Gödel-Löb logic of provability $GL$, topological interpretations have been pioneered by H. Simmons and L. Esakia in the 1970s.

GL in Hilbert-style

The language of $GL$ has propositional variables $p_0,p_1,\dots$ and logical connectives $\to$, $\bot$, $\top$ and one unary modality $\Box$. Besides all tautologies of classical propositional logic, GL has the following axiom schemes:

$GL$ proves the transitivity rule$\Box\varphi\to\Box\Box\varphi$ but not the reflexivity rule$\Box\varphi\to\varphi$ whence it is an extension of $K4$ but not of $S4$.