Characteristic classes and bisimulations of generalized Veltman models (Q2718477)

The basic interpretability logic IL proposed by Visser has been proved by de Jongh and Veltman to be complete with respect to so-called Veltman models. It is also known that there are several principles of interpretability which are not provable in IL. Among them Svejdar proved that one called W is properly stronger than another called F (of Feferman) on the base of IL but they are semantically equivalent in the framework of Veltman models. Thus the semantics is not sufficient for distinguishing the principles of interpretability. In this paper, the author shows that the generalized Veltman models introduced by de Jongh have indeed better characterizability than Veltman models. The author introduces also a bisimulation between generalized Veltman models and shows its basic properties.