On proofs and types in second order logic

Abstract

In questa tesi sono considerate alcune questioni riguardanti la teoria della dimostrazione della logica del secondo ordine e della sua controparte costruttiva, il Sistema F (Girard 1971). Le analisi sviluppate ruotano attorno al tema centrale della apparente “circolarità” delle dimostrazioni del secondo ordine, che si riflette nella possibilità di tipare nel Sistema F forme di auto-applicazione, laddove la diagnosi di Russell era che i tipi dovessero servire a eliminare i \circoli viziosi" (Poincaré 1900) che emergono dall'applicazione di una funzione a se stessa. Lo studio di tale sistema costituisce dunque il punto di partenza di una ricerca incentrata su risultati e prospettive logiche molto spesso ignorate dalla letteratura filosofica sul secondo ordine. L'analisi delle circolarità è condotta sulla base di una distinzione metodologica tra due approcci in teoria della dimostrazione: quello della giustificazione (“le pourquoi", Girard 2000), indirizzato alle dimostrazioni di coerenza e all'Hauptsatz, e quello della comprensione (“le comment", Girard 2000), indirizzato alla caratterizzazione della struttura combinatoria delle prove (viste come entità computazionali, o programmi). Particolare interesse è rivolto, in questa seconda prospettiva, all'analisi di prove scorrette o paradossi, come il paradosso di Girard. Nella prima parte della tesi, dedicata al “pourquoi", gli argomenti tradizionali sui “circoli viziosi" sono confrontati con la prospettiva che emerge dalla dimostrazione dell'Hauptsatz per la logica del secondo ordine (ottenuta in Girard 1971 attraverso la tecnica dei candidati di riducibilità). Nella seconda parte della tesi, dedicata al “comment", sono proposti due approcci combinatori ai “circoli viziosi", con alcuni risultati tecnici: il primo basato sulla teoria del polimorfismo parametrico, il secondo sull'analisi geometrica del tipaggio ottenuta attraverso la teoria dell'unificazione.