• teoria dei topos
• intuizionismo

Il progetto di questa tesi nasce con l’intento di mettere in luce alcuni rapporti fra teoria dei topos e intuizionismo. I due ambiti, molto distanti per tradizioni e interessi, hanno trovato negli ultimi 40 anni, da quando cioè esiste una presentazione assiomatica della teoria dei topos elementari, diversi punti di contatto. Al fine di chiarire in che termini possano essere
sanciti rapporti fra queste due teorie, può essere utile accennare allo status epistemologico delle due teorie coinvolte: se la teoria dei topos può essere presentata in termini puramente matematici, l’intuizionismo appare piuttosto come una riflessione che coinvolge istanze sia logico-matematiche, che filosofiche. Non e' nostra ambizione tentare una presentazione dell’intuizionismo; limiti di spazio e tempo ci porterebbero al di la' delle nostre iniziali intenzioni; nello sviluppo della tesi daremo, invece, una sintesi di quelli che sono i prodromi della teoria matematica dei topos. E’ tuttavia naturale domandarsi se i legami fra teoria dei topos e intuizionismo siano da collocarsi in ambito logico-matematico o se vi siano piuttosto aspetti filosofici che sanciscono rapporti fra le due teorie.
In questa tesi gettiamo le basi per un’analisi logica di questi rapporti, tralasciando sostanzialmente quelli che possono essere considerati gli aspetti filosofici della questione: a livello metodologico è sempre necessario - ad avviso dell’autore - chiarire in primo luogo gli aspetti ‘certi’ di un determinato problema prima di offrirlo ad una discussione di pi` ampio respiro come puo essere un’analisi filosofica dello stesso.
I rapporti che metteremo in luce non hanno alcuna pretesa di esaustivita' e rappresentano solo un abbozzo di una riflessione non ancora matura: nel selezionare gli argomenti che avvicinano le due teorie sono stati omessi capitoli rilevanti della letteratura che corroborano in maniera ancor più profonda le ambizioni del presente lavoro.
Dopo aver introdotto nel capitolo 1 la teoria assiomatica degli insiemi ZF, motivati dalla richiesta di un fondamento chiaro e non ambiguo per la discussione che si vuole affrontare, nel capitolo 2 si danno le definizioni categoriali fondamentali per la comprensione della nozione di topos; una volta definiti i topos elementari si passa quindi ad un’analisi di esempi fondamentali che mostrano come alcune categorie note ricadano effettivamente nella definizione di topos elementare (paragrafo 2.3). Nel paragrafo 2.4 vengono sintetizzate le prime proprieta' topos-teoretiche, con particolare attenzione agli aspetti insiemistici e logici (paragrafi 2.4.2 e 2.4.3).
Nel paragrafo 2.5 si introducono le algebre di Heyting, strutture fondamentali per la semantica algebrica del calcolo proposizionale intuizionista; successivamente si mostra il primo e piu' semplice aspetto che lega teoria dei topos e intuizionismo: ogni algebra dei sottoggetti di un dato oggetto in un topos e' in generale, un’algebra di Heyting.
Nel capitolo 3 si definisce un opportuno sistema deduttivo, il calcolo di Joyal,
che permette l’interpretazione della logica (intuizionista) di ordine superiore in un topos; il calcolo logico usato e' un calcolo dei sequenti del secondo ordine, tipato, con assiomi di estensionalita' e comprensione; in letteratura
sono stati proposti sistemi simili con il nome di local set theory e higher order intuitionistic type theory.
Il teorema fondamentale che dimostriamo in questo lavoro -al quale e' dedicato per intero il capitolo 4- e' un teorema di completezza per l’interpretazione del calcolo di Joyal in un topos. La dimostrazione di un teorema di completezza per un tale sistema corrobora l’affermazione, spesso non giustificata o data per assunta in letteratura, secondo la quale la logica propria di un topos e', in generale, intuizionista.
Nel capitolo 5 si esamina la costruzione del linguaggio interno associato ad un topos E; a partire da questo e' possibile definire un topos sintattico, Top(Γ), equivalente ad E, giustificando la prospettiva secondo cui e' possibile considerare un topos come una teoria oltre che come una struttura. Si introduce quindi una semantica ‘locale’, la semantica di Kripke-Joyal, che sancisce un ulteriore punto di contatto con l’intuizionismo: le regole di forcing date possono essere opportunamente riadattate per un topos di prefasci su un insieme
parzialmente ordinato in modo da ritrovare la semantica a mondi possibili, descritta da Kripke, per la logica intuizionista.
Infine nel paragrafo 5.3 mostriamo che esiste un topos in cui ogni funzione reale a valori reali e' continua, ritrovando cosi' un celebre teorema di matematica intuizionista dimostrato da Brouwer.
Nella presentazione dei risultati abbiamo privilegiato un’esposizione attenta ai contenuti: per non appesantire la lettura si e' preferito rimandare il lettore alla bibliografia (puntualmente segnalata) per le dimostrazioni, a parte per i teoremi fondamentali discussi nella tesi.