Sulle logiche dell'interpretabilità debole

Abstract

Questa tesi indaga i fondamenti semantici e teorico-dimostrativi delle logiche deboli dell'interpretabilità. Per isolare i meccanismi di tali strutture relazionali, abbandoniamo il tradizionale focus sulla complessità dei sistemi standard, come IL e le sue estensioni principali. Adottiamo invece una rigorosa metodologia bottom-up basata sull'analisi di sottosistemi indeboliti: ciò permette di isolare con precisione il comportamento relazionale di base, al riparo dalle interferenze di interazioni assiomatiche più complesse.

Il Capitolo 1 definisce il quadro teorico. Partendo dalla logica della dimostrabilità, introduciamo la logica dell'interpretabilità standard IL, esplorandone le profonde connessioni aritmetiche, i legami con i fenomeni di conservatività e la necessità metamatematica che motiva lo studio di questi sistemi formali più deboli.

Il Capitolo 2 propone un'analisi sistematica della logica di base minimale IL- e delle sue estensioni intermedie. Ne illustriamo le formulazioni assiomatiche e la semantica, esaminando aspetti metamatematici cruciali come la completezza e l'incompletezza rispetto a frame appropriati, le proprietà di punto fisso e l'interpolazione.

Infine, il Capitolo 3 presenta il principale contributo tecnico del lavoro: basandoci sugli impianti consolidati per IL, sviluppiamo un calcolo dei sequenti etichettato, modulare e in stile G3 per IL- e le sue estensioni. Questa struttura sintattica internalizza le complesse condizioni semantiche dei frame sotto forma di regole d'inferenza puramente geometriche. Dopo averne stabilito le proprietà strutturali, dimostriamo la correttezza e la completezza dei sistemi proposti. Il capitolo si conclude delineando i problemi aperti e le future direzioni di ricerca.

This thesis provides an investigation into the semantic and proof-theoretic foundations of weak interpretability logics. Driven by the need to isolate the fundamental mechanisms governing these relational structures, we deliberately shift the traditional focus away from the structural complexity of standard systems such as IL and its principal extensions. Instead, we adopt a strict bottom-up methodology centered on the analysis of weakened subsystems, a strategy that allows for a precise isolation of the core relational behavior, free from the interference of more complex axiomatic interactions.

In Chapter 1, we establish the theoretical background. Starting from provability logic, we introduce the standard interpretability logic IL, exploring its profound arithmetical connections, its relationship with conservativity phenomena, and the exact metamathematical necessity that motivates the study of such weaker formal systems.

Following this trajectory, in Chapter 2, we narrow our focus to conduct a systematic analysis of the minimal base logic IL- and its intermediate extensions. We detail both their axiomatic formulations and semantics, examining crucial metamathematical features such as completeness and incompleteness with respect to appropriate frames, fixed-point properties, and interpolation.

Finally, Chapter 3 presents the primary technical contribution of this work: building upon established frameworks for IL, we develop a modular, G3-style labelled sequent calculus for IL- and its extensions. This syntactic framework is constructed by internalizing complex semantic frame conditions as purely geometric inference rules. We establish the core structural properties of the calculus, ultimately proving the soundness and completeness of the proposed proof systems. The chapter concludes by outlining open problems and future research directions in the field of interpretability logics.