Non conservatività dell'interpretazione di Curry-Howard-Martin-Lof della logica intuizionista con uguaglianza in teoria dei tipi

La teoria dei tipi, introdotta nei primi del Novecento da Bertrand Russell, è attualmente una branca sia della Matematica che dell’Informatica, in quanto fornisce paradigmi fondazionali di carattere matematico, logico e informatico. In particolare, la teoria dei tipi di Martin-Löf si può considerare sia una teoria degli insiemi che un paradigma di un linguaggio di programmazione funzionale. In questa tesi ci occuperemo di presentare il frammento MLTT_0 della teoria dei tipi di Martin-Löf sufficiente per interpretare la logica intuizionista predicativa con uguaglianza secondo l’interpretazione di Curry-Howard-Martin-Löf degli anni ’80. Nostro scopo è dimostrare la non conservatività dell’interpretazione di Curry-Howard-Martin-Löf della logica intuizionista con uguaglianza in MLTT_0 sulla logica stessa. Nello specifico, dopo aver descritto MLTT_0, descriveremo l’interpretazione di Curry-Howard-Martin-Löf, dimostrando che essa rende valida la deduzione naturale DNI= della logica intuizionista predicativa con uguaglianza. Poi proseguiremo con la dimostrazione in MLTT_0 dell’assioma di scelta. Infine, a conclusione del nostro studio, enunceremo e dimostreremo il teorema di non conservatività di MLTT_0 sopra la logica intuizionista con uguaglianza, provando in particolare che la formula detta choice approximation principle non è derivabile in DNI= ma lo è per l’interpretazione della logica in MLTT_0."