Filtrations of generalized Veltman models (Q2827954)

The paper is devoted to provability logic and its extension, i.e., the interpretability logic IL introduced by \textit{A. Visser} [in: Mathematical logic. Proceedings of the summer school and conference dedicated to the ninetieth anniversary of Arend Heyting (1898--1980), held in Chaika, Bulgaria, September 13--23, 1988. New York: Plenum Press. 175--209 (1990; Zbl 0793.03064)]. The author adapts the filtration method to the generalized Veltman semantics for interpretability logic. Bisimulations are used to define adequate filtrations -- this is done in order to preserve the defining properties of generalized Veltman models. The main results are: an alternative proof of the finite model property of interpretability logic IL with respect to Veltman models, the proof of the finite model property for the systems ILM and ILM\(_{0}\) with respect to generalized Veltman models.