Fondazione della teoria delle categorie senza usare insiemi

[Nicolaus]

Stavo cercando delle introduzioni alla teoria delle categorie, ma ho notato che molte di loro si servono della nozione di insieme (o delle nozioni di conglomerati e collezioni). E' possibile fondare la teoria delle categorie senza ricorrere a questi concetti , che voi sappiate?

[Epimenide93]

La stessa teoria delle categorie può essere usata come fondamento della matematica al posto della teoria degli insiemi (che da questa può essere derivata). Qui puoi trovare una breve presentazione della questione e degli ottimi riferimenti da cui partire. Anche qui puoi trovare molti punti di partenza. Tale approccio è interessante anche perché porta dritto dritto alla teoria dei topoi ed alla natura fondazionale di quest'ultima.

So che la matematica può fondarsi anche sulla teoria dei tipi (vedi anche su Wikipedia), ma al riguardo non so dirti praticamente nulla.

Sono abbastanza sicuro che se attendi un tempo sufficientemente lungo un certo utente di questo forum con la tendenza a "introdurre Divinità nuove" e "colpevole di corrompere i giovani" potrebbe intervenire e spiegare ulteriormente la questione.

[vlander]

"Epimenide93":So che la matematica può fondarsi anche sulla teoria dei tipi (vedi anche su Wikipedia), ma al riguardo non so dirti praticamente nulla.

HoTT, capitolo 9.

[Epimenide93]

@vlander

You, Sir, just ruined my life

Scherzi a parte, benvenuto e grazie mille!

[Nicolaus]

Ero all'oscuro della teoria omotopica dei tipi. Sembra ancor più generale della teoria delle categorie. Alla fine sono riuscito a trovare googlando qua e là un modo di fondare la teoria delle categorie senza utilizzare il concetto di "insieme" , tuttavia occorre utilizzare la logica del primo ordine con uguaglianza. La teoria dei tipi che mi avete proposto sembra essere di per se un punto di partenza capace di fondare essa stessa la logica matematica (e tutto il resto). Piuttosto interessante, grazie mille.


http://ncatlab.org/nlab/show/fully+formal+ETCS#the_theory_of_categories (Teoria delle categorie senza il concetto di insieme)

[Epimenide93]

guarda che la prima parte del mio intervento era riferita proprio a ETCS.

[Nicolaus]

"Epimenide93"::| guarda che la prima parte del mio intervento era riferita proprio a ETCS.

Si ma ETCS può essere a sua volta ridotto. Vi è un nucleo di assiomi più fondamentali che possono essere specificati senza parlare di insiemi e che descrivono esclusivamente le categorie

[Epimenide93]

Temo tu stia facendo un po' di confusione. In ECTS il concetto di categoria precede logicamente quello di insieme, la definizione di categoria fa parte dell'assiomatica; in altre parole, non è necessario aver definito un insieme per definire una categoria. Quella che riporti è solo una parte della formulazione di ECTS in termini logici, in cui viene definita una categoria. Se ti fermi lì, non stai fondando niente, stai solo dando gli assiomi per una teoria del primo ordine. È la stessa differenza che passa tra la definizione di gruppo data solitamente in algebra (in termini di teoria degli insiemi) e l'assiomatizzazione come teoria del primo ordine[nota]o di ordine superiore al primo[/nota] (click).

Se il tuo scopo è descrivere semplicemente il comportamento di una categoria da un punto di vista logico va più che bene, se vuoi sviluppare la teoria delle categorie, quello che proponi non è sufficiente come "ambiente logico".

[Nicolaus]

Si hai ragione mi sono confuso. Mi interessava sapere se si poteva parlare di una categoria (e descriverne il comportamento logico) senza parlare di insiemi. Il link che ho messo chiamava questa prima porzione degli assiomi come Th(Cat) (teoria delle categorie) e mi ha tratto in inganno.

[killing_buddha]

C'è un modo di "interpretare" la teoria delle categorie in astratto anche senza usare HoTT. Alcune referenze buttate là, poi magari approfondisco (e se non le scrivo non ricordo più cosa volevo dire).

Il lavoro quasi misconosciuto di John Gray "Adjointness for 2-categories: Formal category theory"
Il lavoro di Shulman "Enriched Indexed categories" , che propone un connubio tra le due visuali con cui si può interpretare la teoria, ovvero internalizzazione (una categoria è il modello di uno sketch) VS arricchimento (una categoria è una struttura arricchita su una struttura monoidale).

[Nicolaus]

Siete stati tutti molto esaustivi, grazie mille.