Logica della dimostrabilità

Il lavoro parte da un'introduzione della logica modale, e nello specifico concentrandosi sui sistemi K4 e GL. Dopo aver fatto un breve accenno all'aritmetica di Peano(PA) e al lavoro di Goedel dell'aritmetizzazione della sintassi (e dimostrando, attraverso il teorema di Loeb, il secondo teorema di incompletezza), giunge a enunciare e dimostrare il teorema di Solovay, o teorema di completezza aritmetica. Questo teorema permette non soltanto di poter attribure all'operatore modale Box il significato di "dimostrare", ma mostra una forte corrispondenza tra GL e PA, ossia, che sotto un'opportuna traduzione del linguaggio di GL in quello di PA, i due sistemi hanno gli stessi teoremi.