Armonie classiche per connettivi computazionali

Speaker:
Mattia Petrolo
Quando:
14/05/2010 - 11:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, Via Ostiense 234
Abstract

La teoria antirealista del significato sviluppata a partire dagli anni '70 da Dummett, Prawitz e Martin-Löf, stabilisce diversi desiderata che le regole logiche devono soddisfare affinché esse possano caratterizzare adeguatamente i connettivi logici. In particolare, il requisito di armonia impone un "equilibrio deduttivo" che apparentemente non può essere soddisfatto che dalle regole della logica intuizionista.

Nella prima parte del talk, mostriamo in che senso l'isomorfismo di Curry-Howard rispecchia fedelmente tali condizioni richieste ad un calcolo logico. All'interno di questo quadro teorico, analizziamo alcuni limiti degli approcci tradizionali alla nozione di armonia e proponiamo un criterio sufficiente per definire un connettivo logico. Tale criterio rende conto del fatto che le proprietà dei connettivi intuizionisti hanno una natura fondamentalmente computazionale.

Nella seconda parte del talk, esaminiamo alcune possibili strategie per estendere alla logica classica il criterio proposto. Questo costituisce un primo passo verso la possibilità di valutare l´importanza filosofica della "costruttivizzazione" della logica classica.