Título: «PRK, una lógica constructiva clásica»
Director: Pablo Barenbaum
Jurado:
– Eduardo Bonelli (Stevens Institute of Technology)
– Santiago Figueira (ICC, CONICET)

Resumen:

Esta tesis presenta el sistema PRK, un sistema lógico en el cual las
nociones de prueba y refutación son duales. Este sistema extiende a la
lógica clásica y es constructivo en el sentido de que se lo puede
dotar de una interpretación computacional con buenas propiedades. Las
fórmulas de PRK se clasifican a lo largo de dos ejes, dependiendo de
su positividad (afirmación o negación) y su fuerza (fuerte o clásica).
Las proposiciones fuertes se demuestran, canónicamente, con reglas de
introducción, mientras que las proposiciones clásicas se demuestran
por reducción al absurdo. El sistema PRK resulta ser correcto y
completo con respecto a una clase de modelos de Kripke, definida en
este mismo trabajo. Siguiendo la correspondencia de Curry–Howard, se
formaliza un cálculo asociado a PRK, denominado λPRK, cuyo sistema de
tipos se corresponde con el sistema lógico PRK. Se establecen varias
propiedades sobre λPRK, incluyendo preservación de tipos, confluencia
y una caracterización de las formas normales de las pruebas y
refutaciones. La terminación fuerte del cálculo λPRK se demuestra a
través de una traducción a System F extendido con ecuaciones
recursivas entre tipos, y apoyándose en un resultado de Mendler. Por
último, se considera una extensión a segundo orden del sistema PRK,
junto con el cálculo correspondiente λPRK2. Se extienden a este marco
los resultados anteriormente mencionados, exceptuando la terminación
fuerte de λPRK2, que queda abierta como trabajo futuro.