El Área de Matemática del PEDECIBA invita a la defensa de tesis de
Doctorado del estudiante Félix Castro
Título: La jerarquía analítica ramificada en lógica de segundo orden
Directores de tesis: Alexandre Miquel y Hugo Herbelin
Fecha de la defensa: 17 de diciembre a las 13.00 hs. (hora Uruguay)
Enlace
https://salavirtual-udelar.
Tribunal:
Laurent Regnier (Universidad U. Aix-Marseille), Colin Riba (ENS-Lyon), Hugo Herbelin (U. Paris-Cité & INRIA), Alexandre Miquel (UdelaR), Laura Fontanella (U. Paris-Est Créteil), Guillaume Geoffroy (U. Paris-Cité), Walter Ferrer (UdelaR), Christine Tasson (ISAE SUPAERO)
Resumen :
En su primera parte, esta tesis se centra en el estudio de la jerarquía analítica ramificada (RAH) en aritmética de segundo orden (PA2). La jerarquía analítica ramificada fue definida por Kleene en 1960. Se trata de una adaptación de la noción de constructibilidad (introducida por Gödel para la teoría de conjuntos) al marco de la aritmética de segundo orden. Las propiedades de esta jerarquía, en relación con la computabilidad y con el estudio de los modelos de PA2, han sido estudiadas en profundidad. Parece natural formalizar RAH en PA2 en un intento de demostrar que añadir el axioma de elección o (una variante de) el axioma de constructibilidad a la aritmética de segundo orden no conlleva contradicción.
Sin embargo, el único rastro escrito de tal formalización parece ser incorrecto. En esta tesis, queremos trabajar sobre esta formalización.
Para ello, trabajaremos en una versión de la aritmética obtenida eliminando el axioma de inducción de los axiomas de PA2. En este sistema, aparece una nueva variante del axioma de elección: lo llamamos axioma de colección, en referencia al axioma homónimo de la teoría de conjuntos. Parece que este axioma nunca se ha considerado en el contexto de la lógica de segundo orden. Demostramos que tiene buenas propiedades computacionales: su contrapositivo se realiza por la identidad en la realizabilidad clásica, mientras que él mismo se realiza por la identidad en la realizabilidad intuicionista. Además, mostramos que es equivalente a un axioma que se comporta bien con respecto a una traducción negativa de la lógica clásica a la lógica intuicionista. Finalmente, mostramos que una variante del axioma de colección es más débil que una variante del axioma de elección en lógica intuicionista.
Por tanto, trabajamos en una teoría sin inducción pero que contiene el axioma de colección para estudiar la jerarquía analítica ramificada. Demostramos que es un modelo de PA2 que satisface una versión fuerte del axioma de elección: el principio del universo bien ordenado. Parece que el axioma de colección es necesario para demostrar este resultado y explicaremos a fondo esta intuición.
En la segunda parte de la tesis, más breve que la primera, estudiamos la igualdad extensional en aritmética de tipo finito (HAw). La aritmética de tipo finito es una teoría de primer orden. Es una extensión conservativa de la Aritmética de Heyting que se obtiene extendiendo la sintaxis de los términos a todo el Sistema T: los objetos de interés aquí son los funcionales de tipos superiores. Mientras que la igualdad entre números naturales está especificada por los axiomas de Peano, cómo puede definirse la igualdad entre funcionales? A partir de esta pregunta, surgen diferentes versiones de HAw, como una versión extensional (E-HAw) y una versión intencional (I-HAw). En este trabajo veremos cómo el estudio de unas relaciones de equivalencia parciales nos lleva a diseñar una traducción por parametricidad de E-HAw a HAw.