On the Goldblatt-Thomason theorem for interpretability logic

A theory U interprets a theory V in the sense of Tarski-Mostowski Robinson roughly when there is a structure preserving translation j so that under this translation any theorem of V becomes a theorem of U , in symbols: ∃j ∀ϕ(V ⊢ ϕ → U ⊢ ϕ_j ). Very similar to provability logic we can thus define the propositional interpretability logic of a theory IL(T ). Even though interpretability is a Σ⁰_3 complete notion, IL(T) is often a PSPACE decidable logic. Since its introduction in the 1980’s, the modal theory of interpretability logics and related has become a mature field with so-called Veltman frames and models being the predominant relational semantics. Contrary to the case of provability logic, different sound theories can have different corresponding interpretability logics. These different logics are typically defined by adding axiom schemes over a base logic IL and over IL-frames these schemes give rise to so-called frame conditions and correspondences. Not all frame conditions are however modally definable. Ad-hoc methods aside, a general way of characterising modal definability is given by a so-called Goldblatt-Thomason Theorem. In this paper we comment on the proof of such a new theorem in the realm of interpretability logic with a special focus on the new techniques required.