Logiche sottostrutturali e calcolo di Lambek

Tese arquivada ao abrigo da Portaria nº 227/2017 de 25 de JulhoIn questa tesi si ha l’obiettivo di dare una breve idea del problema delle logiche sottostrutturali e gli strumenti per poterne parlare. Nella prima parte del primo capitolo introdurremo il calcolo delle sequenze per la logica classica, vedremo le sue regole e il suo formalismo, così da avere gli strumenti essenziali per poter entrare nel vivo del discorso. Nella seconda parte, invece, approccieremo da un punto di vista storico il problema delle logiche sottostrutturali, individuandone le origini e ripercorrendo, a grandi linee, la storia. Nel secondo capitolo tratteremo in maniera sistematica le regole strutturali. Inizialmente ci interrogheremo sul loro ruolo nella definizione delle caratteristiche di una logica, e del loro rapporto con le regole operazionali. Successivamente ci concentreremo su quali benefici (o meno) apportano al calcolo. Nel terzo capitolo faremo una carrellata di logiche sottostrutturali, e vedremo come i calcoli cambiano al variare dei postulati. Inoltre, vedremo come possiamo leggere le sequenze. Nel quarto capitolo vedremo metodi alternativi per reintrodurre le regole strutturali nel nostro calcolo. Infatti, se da una parte abbiamo buoni motivi per eliminarle, dall’altro è innegabile che esse aumentano il potere deduttivo del calcolo. Cercheremo quindi di reintrodurle ad un livello più alto. Considereremo soltanto quattro metodologie, in letteratura ne possiamo trovare molte altre, ma sicuramente, le più utilizzate sono le ipersequenze e i display calculi. Nel quinto e nel sesto capitolo ci occuperemo dell’algebra delle logiche sottostrutturali. In particolare, nel quinto capitolo forniremo tutti gli strumenti necessari a parlare della semantica algebrica (argomento del sesto capitolo). Partiremo dando, nella prima parte, le definizioni preliminari che serviranno a definire gli -reticoli, che saranno la struttura algebrica base, a partire dalla quale costruiremo i modelli algebrici per tutte le logiche sottostrutturali. Nell’ultimo capitolo ci concentreremo sul nostro case study: il calcolo di Lambek. Vedremo prima la variante originale e, successivamente, vedremo come estenderlo in quello che è noto come free Lambek’s calculus, ideato da Ono. Come già detto, questo lavoro rappresenta una breve e semplice introduzione ad una problematica che, negli ultimi venti anni (e forse più), è diventata uno degli argomenti più discussi della logica contemporanea. Sono infatti molti i logici che si dedicano allo studio di questa particolare classe di logiche. Le logiche sottostrutturali, oltre ad essere interessanti da un punto di vista filosofico e proof-teoretico, hanno molte applicazioni nell’algebra e, in particolare, con i calcoli di Lambek meglio, con la loro estensione, si è andata sviluppando un particolare settore della logica: l’algebraic proof theory. I padri di questa disciplina di confine sono A. Ciabattoni, N. Galatos e K. Terui