The Logic of Turing Progressions

Abstract

This dissertation is devoted to developing modal logical tools that can be used in the field of proof theory and ordinal analysis. More precisely, we focus on the relation between strictly positive modal logics and both Turing progressions and ordinal notation systems.

With respect to the former one, we introduce the system TSC that is tailored to generate exactly all relations that hold between different Turing progressions given a particular set of natural consistency notions. We also present an arithmetical interpretation for this modal system, named the Formalized Turing progressions interpretation. The logic is proven to be arithmetically sound and complete with respect to this interpretation. After exploring the arithmetical semantics of TSC, we investigate the relational semantics of this system. For this purpose, we make use of the universal model of the closed fragment of Go¨del-Lo¨b’s Polymodal Logic (GLP), namely Ignatiev’s universal frame. By slightly modifying the relations defined in this model, we obtain a new frame which is proven to be a universal model for TSC. Moreover, we show how the domain of this frame can be reduced to sequences with finite support while keeping the completeness of the system.

As for ordinal notations systems, we present the logic BC (for Bracket Calculus). Unlike other provability logics, BC is based on a purely modal signature that gives rise to an ordinal notation system instead of modalities indexed by some ordinal given a priori. Moreover, since the order between these notations can be established in terms of derivability within the calculus, the inferences in this system can be carried out without using any external property of ordinals. The presented logic is proven to be equivalent to Reflection Calculus (RCΓ0 ), that is, to the strictly positive fragment of GLPΓ0 .

El objetivo de esta tesis es desarrollar herramientas de lógica modal que puedan ser utilizadas en el campo de la teoría de la demostración y el análisis ordinal. Más precisamente, nos centramos en la relación entre las lógicas modales estrictamente positivas y las progresiones de Turing, y entre dichas lógicas y los sistemas de notación ordinal que surgen de ellas.

Con respecto a la primera parte, hemos introducido el sistema TSC, diseñado para generar exactamente todas las relaciones válidas entre las diferentes progresiones de Turing, dado un conjunto particular de nociones de consistencia naturales. También presentamos una interpretación aritmética para este sistema modal, denominada interpretación de las Progresiones de Turing formalizadas. Demostramos que la lógica es aritméticamente correcta y completa con respecto a esta interpretación. Tras de estudiar la semántica aritmética de TSC, investigamos la semántica relacional de este sistema. Para este propósito, hacemos uso del modelo universal para el fragmento cerrado de Gödel-Löb’s Polymodal Logic (GLP), a saber, el marco universal de Ignatiev. Modificando ligeramente las relaciones definidas en este modelo, obtenemos un nuevo marco. Demostramos que éste es un modelo universal para TSC. Asimismo, mostramos cómo el dominio de este marco puede reducirse a secuencias con soporte finito manteniendo la completud del sistema. Respecto a los sistemas de notación ordinal, presentamos la lógica BC (por Bracket Calculus). A diferencia de otras lógicas de la demostrabilidad, BC se basa en un lenguaje puramente modal que da lugar a un sistema de notación ordinal, en lugar de estar construido mediante modalidades indexadas por algún ordinal dado a priori. Además, ya que el orden entre estas notaciones puede establecerse en términos de derivabilidad dentro del cálculo, las inferencias en este sistema pueden llevarse a cabo sin usar ninguna propiedad externa de los ordinales. Demostramos que la lógica presentada es equivalente al Reflection Calculus (RCΓ0 ), es decir, al fragmento estrictamente positivo de GLPΓ0 .