Ok, sono tornato. Andiamo con ordine.
La mia domanda era solo fine a sapere se usare un sistema di assiomi per valutarne altri non fosse un problema logico.
E' una buona domanda: sì, probabilmente lo è; ma non importa a nessun matematico, perché questo è visto come un problema di filosofia della matematica; questo dovrebbe farti capire
Non capisco cosa c'entra con la filosofia
Per il resto, torniamo alla tua domanda originaria:
attualmente esiste una teoria, o si sta costruendo una teoria, per fondare la matematica, che sia rigorosa come la teoria assiomatica degli insiemi, ma non sia "limitata" dai teoremi di incompletezza?
Qualsiasi teoria che sia abbastanza potente da esprimere l'aritmetica dei numeri interi subisce le conseguenze dei teoremi di incompletezza. Hai allora due scelte: o parli solo di cose talmente semplici da non descrivere nulla, o ti becchi l'incompletezza. Chiaramente, accettare la seconda cosa pur di parlare è un prezzo molto piccolo da pagare. Tanto più che l'incompletezza non è un limite, come ti hanno già spiegato (è quanto di più vicino all'ordine delle cose, se sposi una visione "linguistica" della matematica: va così e non puoi farci molto). Quando dico "visione linguistica" intendo che la filosofia -senza troppa distinzione tra est e ovest- ha riflettuto abbondantemente sul problema se esista un linguaggio capace di parlare compiutamente di sé;
la matematica è arrivata a una sorta di risposta.
Una domanda, dato che la teoria delle categorie è sempre fondata su assiomi, come fa a raggruppare diversi sistemi di assiomi.
Conosci la differenza tra linguaggio e metalinguaggio, e tra teoria e metateoria? La matematica, oggi, 2019, si fa così: si scrive una lista di assiomi, che sono ZF, e poi si decide di credere all'esistenza di un modello per questa teoria. Praticamente, decidi che esiste qualcosa che soddisfa quegli assiomi, che quindi vivono "da un'altra parte"; questa parte è la metateoria, laddove invece la teoria che ti metti a studiare è "più piccola". Si può fare di meglio? Si può cioè dimostrare che esiste un modello di ZF invece di crederci? No, purtroppo non si può, perlomeno non nel senso che speri quando lo chiedi. Il meglio che si può fare è prendere "tutte le cose che hai" e sperare che quello sia un modello di ZF; ops, però:
ci sono problemi.
Con le categorie è la stessa cosa: la domanda
quale teoria degli insiemi si può fare in CT? è interessante e piuttosto complessa da esaurire: c'è una fondazione, che si chiama
ETCS che cerca di rispondere al meglio che si può; è un sistema assiomatico strettamente meno potente di ZF, ma abbastanza potente da implementare la teoria della ricorsione -se ben ricordo, fu proprio per questo che Lawvere la inventò e diede quegli assiomi, e non altri- e quindi l'aritmetica. Quindi anche qui, incompletezza di qualche sorta.
Che si possa fare "tutta" l'aritmetica elementare semplicemente con una manciata di funzioni definite per ricorsione, è un teorema, che credo dimostrò Church, ti posso trovare un riferimento o ancora meglio -spero- un video di youtube dove viene implementata praticamente in functional Java tutta l'aritmetica degli interi "partendo dall'insieme vuoto".
Ci sono altre scelte, oltre a ZF ed ETCS: algebraic set theory, teoria dei tipi, teoria intuizionistica dei tipi,
semantica categoriale (che sarebbe la vera risposta alla tua domanda, ma richiede più spazio e tempo di quel che posso dedicare alla faccenda), basic picture, etc.
L'invito, ora è molteplice: a studiare molto, perché questi non sono problemi da poco; a non fidarti di chi li conclude in poche parole perché "sono seghe"; a non studiare solo logica, altrimenti la tua matematica non parla più di nulla; ad avere pazienza, perché prima di avere visto un po' di matematica, questi discorsi non hai modo di capire davvero di cosa parlino; e infine, quando li hai capiti, parlane ai filosofi, che ne hanno un bisogno cane.
