Temi

In questo lavoro cercherò di presentare il tema delle logiche sottostrutturali.1 In particolare, inizieremo con l'introdurre il calcolo dei sequenti per la logica classica, LK, introdotto da Gerhard Gentzen negli anni '30 del secolo scorso. Vedremo come questo si sviluppa a partire dagli assiomi attraverso delle regole. Queste regole possono essere raggruppate in due insiemi disgiunti, le regole operazionali, che coinvolgono direttamente i connettivi logici, e quelle strutturali, che agiscono sulla struttura delle prove. Vedremo, quindi, come queste regole agiscono all'interno del calcolo, e qual è il significato, sia formale sia intuitivo, di ciascuna di esse. Una volta descritto il funzionamento del calcolo ci soffermeremo su ciascuna regola strutturale, cercando di capire quali siano le motivazioni tecniche e quelle pragmatiche, che si agganciano alla struttura del linguaggio naturale e della comunicazione quotidiana, che motivano la presenza della regola all'interno del calcolo. Cercherò quindi di illustrarne i "pro ed i contro" provando a descrivere quali siano le ragioni per limitare, in una possibile generalizzazione di LK, l'uso di una specifica regola.