Paradigme de la logique catégorique

Concernant ce qu'est un topos, il y a pas mal de fils où de longues discussions ont eu lieu. Je ne pense pas que l'approche de la logique par les catégories puisse résoudre des problèmes généraux de logique (en tout cas, à ma connaissance, ce n'est jamais arrivé).

La raison en est que cette spécialité s'est surtout beaucoup développée en algèbre et ses plus gros succès sont le fait de chercheurs non logiciens. Il s'est trouvé des gens (peut-être voulant améliorer leur image ou leur carrière, je ne sais pas) qui ont plus ou moins navigué entre logique (prétendument, en fait ils n'y connaissent rien et font beaucoup de spectacle) et catégorie. Mais ceux-là ont surtout beaucoup apporté aux catégories. (Je pense à Benabou par exemple, que j'aime bien entendre parler de catégories mais qui n'est pas logicien tout en étant un peu ambigu (euphémisme) par moment sur l'aveu qu'il ne l'est pas.

Par ailleurs, il est faux de dire "qu'on peut faire de la logique avec les topoi". Plus précisément, dit comme ça, c'est faux. Ce qui est vrai c'est qu'on peut reproduire dans les topoi une partie (la partie bornée) de la théorie des ensembles. En particulier, les topoi ont un langage interne (le mot est bien plus impressionnant que ce qui se cache derrière) et le tout vérifie au moins la logique intuitionniste. Rien n'interdit aux gens ( par exemple, tu as Olivia Caramello qui a soutenu récemment devant deux médailles Field qui ont ensuite fait un discours au delà du dithyrambique sur ses travaux) après de revendiquer le mot "logique" et d'annoncer à la cantonnade qu'ils font de la logique, le mot "logique" n'est pas breveté.

Si ce n'était pas toi, je répondrais éventuellement autrement, mais dans l'idée que je me fais de ce que tu as en tête, il me semble que la manière la plus simple est de te dire ce qui précède. Ce n'est pas "de la logique" comme tu le penses. C'est beaucoup plus technique et beaucoup moins profond et général que tu ne l'imagines. En gros, "ce n'est pas de la philosophie sérieuse", c'est plutôt "des maths destinées à faire avancer l'algèbre abstraite".

Si tu veux te faire une idée de ce que c'est, je peux attendre que tu le demandes. Je connais disons les bases. Par contre, attention, avertissement: c'est un domaine où on redécouvre souvent l'eau chaude avec des mots savants. Ce n'est pas une critique (toutes les maths consistent à découvrir l'eau chaude par définition, puisque tout théorème est un cas particulier d'évidence), c'est juste pour dire que la relation entre logique et LC n'est pas encore bien établie et stabilisée.

Par exemple dès qu'un logicien "comprend" (après un galérien et chronophage décryptage) un théorème de machin-truc, démontré en 2000+n ou en 1990+n, il ressent un très fort énervement et une envie de taper les gens qui lui avaient vendu ces théorèmes, parce que son premier réflexe est de dire "c'était connu depuis longtemps sous la forme truc-bidule". Je ne sais pas si c'est le cas pour tous les théorèmes du domaine (je ne les ai évidemment pas tous lus), mais ce que je viens d'écrire est un témoignage de beaucoup de logiciens (s'il n'y avait que moi, je ne le signalerai pas). C'est dans l'ADN des maths de s'apercevoir (tout théorème étant une évidence dégradée) qu'in fine, le truc "était évident" (après avoir cherché à le prouver pendant 500 ans sans succès), ce n'est donc pas un défaut du domaine. C'est juste que les différents professionnels ont besoin de "s'ajuster".

Par exemple, le forcing est bien plus puissant que le point de vue catégorique (qui n'en est qu'un cas particulier très "dégénéré" (au sens où une réunion de deux droites peut être vue comme une conique) et les forcingueurs sont étonnés de croire voir refait les bases dans une autre langue. Mais en réalité ces derniers (les forcingueurs) se trompent car le forcing ne modifie l'univers qu'au dessus de $omega1^L$ alors que l'approche par les topos pourrait éventuellement permettre de prouver un jour des indécidabilités arithmétiques. (Il n'y a pas de "génériques" dans les topos). Bref.... J'ai essayé de te résumer ce que je sais de tout ça. Donc tout dépend: si tu veux jongler avec de l'infini non dénombrable, les catégories, les topos, tout ça, n'ont aucun intérêt. Si tu veux faire de l'algèbre et unifier ton approche des anneaux, ces objets te tendent les bras. Dans tous les cas, la logique y est très peu présente (le mot "logique" tel qu'utilisé par Olivia Caramello par exemple est substantiellement différent et plus naif que ce que les pros de la logique entendent: disons que c'est essentiellement le point de vue "théorie de modèles" qui habite les travaux de OC)