Selection method for interpretability logic IL with respect to Verbrugge semantics

Interpretability logic is a modal logic which formalizes the notion of relative interpretability between first-order arithmetical theories. Veltman semantics is the basic semantics for interpretability logic. Verbrugge semantics is a generalization of Veltman semantics. Selection is one of the methods to establish finite model property of a logical system, as a step towards showing that the system is decidable. In this paper we show that selection method can be applied to Verbrugge models, by adapting techniques used for Kripke models to this more complex setting.