Sufficiently strong arithmetical theories such as PA can formalize their interpretability predicate. This predicate expresses the concept of relativized interpretability between finite extensions of the theory. Interpretability logics study the provable structural behaviour of the interpretability predicate. Interpretability logics extend the provability logic GL. As such, interpretability logics inherit a number of similarities from GL. For instance, the possibility to give relational semantics. In this thesis we focus on the study of two variations of relational semantics à la Kripke known as ordinary Veltman semantics and generalized Veltman semantics. In the literature we find various definitions of generalized Veltman semantics. In particular, there are several conditions of quasi-transitivity, a property that generalized frames must satisfy. We study the interrelations between all of these conditions and discuss their adequacy. In this thesis we compare the expressiveness of ordinary and generalized Veltman semantics. Furthermore, we give procedures that under some assumptions transform, while preserving modal theoremhood, ordinary models to generalized models and vice versa. We study the frame conditions of various relevant interpretability principles present in the literature. Moreover, we provide novel frame conditions for the the principle R1 and the Rn series of principles from [16] with respect to generalized Veltman semantics. We have formalized our findings in Agda, which is a state-of-the-art proof assistant based on an intuitionistic theory which features dependent types. Apart from giving a solid base to our claims, we hope that our Agda library will provide a rallying point for researchers willing to formalize theorems in the field of interpretability logics, or at least, to encourage more research in that direction. Our work is, to our knowledge, the first attempt at formalizing interpretability logics in any proof assistant.
