La lógica de la demostrabilidad

Abstract

Our main goal in this work is the study of the arithmetical completeness theorem for GL (presented for first time by Solovay in [Sol76]), based on the book The logic of provability by G. Boolos. To reach our goal, we will introduce the formal language of arithmetic toghether with the Peano Arithmetic system, in order to study the provability formula P rov(x) along with L¨ob’s derivability conditions. Moreover we will do a brief study on modal logic, focusing on the main system used in provability logic, GL (for G¨odel-L¨ob) with the purpose of linking GL and Peano Arithmetic. This relationship between these two systems will be achieved by interpreting the box ⇤ as P rov, and then we will be able to prove the arithmetical completeness theorem for GL. In the last chapter, the fixed point theorem for GL will be presented along with a proper algorithm for calculating them.

Nuestro objetivo en esta memoria es el estudio del teorema de completitud aritmética para GL demostrado por primera vez por Solovay en [Sol76], basándonos en el libro The logic of provability de G. Boolos. Para alcanzar dicho objetivo, introduciremos el lenguaje de la aritmética y haremos un estudio sobre el sistema de la Aritmética de Peano, usando funciones recursivas y codificación de la sintaxis de la aritmética para definir el predicado Prov junto a las condiciones de derivabilidad de Löb. A continuación haremos un breve estudio de lógica modal, centrándonos en el sistema por excelencia de la lógica de la demostrabilidad, GL (por Gödel-Löb), con el propósito de crear una relación entre la Aritmética de Peano y GL. Esta correspondencia la conseguiremos interpretando la caja ⇤ como el predicado P rov, y de esta forma poder demostrar el teorema objetivo. Para concluir, demostraremos el teorema de punto fijo para GL, unos de los resultados modales más importantes, junto con un algoritmo para calcularlos.