Interpretability logics and generalized Veltman semantics in Agda

Abstract

[eng] 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.

[cat] Teories aritmètiques suficientment fortes tals com PA poden formalitzar el seu predicat d’interpretabilitat. Aquest predicat expressa el concepte d’interpretabilitat relativitzada entre extensions finites de la teoria. Les lògiques d’interpretabilitat estudien el comportament estructural demostrable del predicat d’interpretabilitat. Les lògiques d’interpretabilitat estenen la lògica de demostrabilitat GL. Com a tals, hereten algunes semblances de GL. Per exemple, la possibilitat de definir una semàntica relacional. En aquesta tesi ens centrem en l’estudi de dues variacions de semàntiques relacionals a l’estil Kripke que es coneixen com semàntica ordinària Veltman i semàntica generalitzada Veltman. En la literatura trobem vàries definicions de semàntica generalitzada Veltman. En particular, hi ha diverses condicions de quasi-transitivitat, una propietat que els marcs generalitzats de Veltman han de satisfer. Estudiem les interrelacions entre aquestes condicions i comentem la seva pertinència. En aquesta tesi comparem l’expressivitat de les semàntiques Veltman ordinàries i generalitzades. A més, descrivim procediments que sota certes hipòtesis transformen, preservant els teoremes modals, models ordinaris Veltman a models generalitzats Veltman i viceversa. Estudiem les condicions de marc per diversos principis d’interpretabilitat que es troben a la literatura. A més, donem noves condicions de marc pel principi R1 i la sèrie de principis Rn presentats en [16] respecte semàntica generalitzada Veltman. Hem formalitzat les nostres aportacions en Agda, que és un assistent de demostració modern basat en una lògica intuïcionista amb tipus dependents. A banda de donar solidesa als nostres avenços, esperem que la nostra llibreria d’Agda pugui ser un punt de trobada pels investigadors que desitgin formalitzar teoremes en el camp de les lògiques d’interpretabilitat, o si més no, que encoratgi més investigació en aquesta direcció. La nostra llibreria és, que sapiguem, el primer intent de formalitzar lògiques d’interpretabilitat en algun assistent de la demostració.