Interpretability logic is a modal logic that can be used to describe relative interpretability between extensions of a given first-order arithmetical theory. Verbrugge semantics is a generalization of the basic semantics for interpretability logic. Bisimulation is the basic equivalence between models for modal logic. The Van Benthem Correspondence Theorem establishes modal logic as the bisimulation invariant fragment of first-order logic. In this paper we show that a special type of bisimulations, the so-called w-bisimulations, enable an analogue of the Van Benthem (...) Theorem for interpretability logic w.r.t. Verbrugge semantics. (shrink)

The interpretability logic ILP is the interpretability logic of all sufficiently strong |$\varSigma _1$|-sound finitely axiomatised theories, such as the Gödel-Bernays set theory. The interpretability logic IL is a strict subset of the intersection of the interpretability logics of all so-called reasonable theories, IL(All). It is known that both ILP and ILW are decidable, however their complexity has not been resolved previously. In [10] it was shown that the basic interpretability logic IL is PSPACE-complete. Here we prove the same for (...) ILP and ILW. (shrink)

Interpretability logic is a modal formalization of relative interpretability between first‐order arithmetical theories. Verbrugge semantics is a generalization of Veltman semantics, the basic semantics for interpretability logic. Bisimulation is the basic equivalence between models for modal logic. We study various notions of bisimulation between Verbrugge models and develop a new one, which we call w‐bisimulation. We show that the new notion, while keeping the basic property that bisimilarity implies modal equivalence, is weak enough to allow the converse to hold in (...) the finitary case. To do this, we develop and use an appropriate notion of bisimulation games between Verbrugge models. (shrink)