Semantica categoriale delle logiche intuizionista e classica

In questa tesi facciamo uso di nozioni di Teoria delle Categorie per affinare e approfondire lo studio dei collegamenti tra sintassi e semantica delle logiche Intuizionista e Classica proposizionale. Dopo aver enunciato la semantica categoriale di entrambe le logiche in termini di particolari funtori aggiunti, le Connessioni di Galois, enunciamo e dimostriamo per entrambe le logiche non solo il teorema di Validità e Completezza ma anche il Teorema del Linguaggio Interno, mostrando un legame astratto tra teorie logiche ed algebre ad esse corrispondenti. Passiamo poi ad applicare tale teorema per ottenere una Riflessione e unaCoriflessione della categoria delle algebre di Heyting in quella delle algebre di Boole. Infine applichiamo il teorema del linguaggio interno per estendere la logica intuizionista propo- sizionale con le regole corrispondenti al connettivo sottrazione di una bi-Heyting algebra. Concludiamo infine dimostrando un teorema di Validità e Completezza per co-Heyting algebre e per il calcolo dei sequenti di G. Restall rispetto alle bi-Heyting algebre