Question d'un ignare
Question d’un ignare (et que donc il vous est loisible de balayer d’un revers de la main).
Je suis avec intérêt et admiration vos discussions, même si elles me passent bien évidemment au-dessus de la tête (et notamment votre capacité à évoluer dans une infinité d’infinis ...).
Mais avant ceci, je pensais que la TDE était quelque chose de démodé, supplanté par les catégories, puis les Topos, et que c‘était une des raisons (pas la seule), de l’« épuisement » du projet Bourbaki (par ailleurs tout à fait admirable (la critique est facile ...)).
Laurent Lafforgue a fait le 6 Novembre dernier (c’est donc récent) une conférence :
https://aroundtoposes.com/laurent-lafforgue-on-the-creative-power-of-categories/
Où, (dans son style assez peu diplomatique), il rend compte du peu d’intérêt de la communauté scientifique vis à vis des Topos, pendant longtemps (c’est en train de changer).
Il montre que les catégories ont un lien avec la logique :
Evidemment, pour moi qui est un grand admirateur de Patrick Dehornoy, il m’est difficile d’imaginer qu’il a passé la plus grande partie de sa vie à explorer une voie sans issue, aussi je serais intéressé par vos commentaires …..
En particulier, je vous entends dire que toutes les mathématiques peuvent être construites au-dessus de ZF (ou ZFC, ou …), et je comprends que cet objectif est une puissante motivation, mais n’existe-t-il pas une autre voie, au travers des catégories (comme l’a suggéré Lawvere) ?
Je suis avec intérêt et admiration vos discussions, même si elles me passent bien évidemment au-dessus de la tête (et notamment votre capacité à évoluer dans une infinité d’infinis ...).
Mais avant ceci, je pensais que la TDE était quelque chose de démodé, supplanté par les catégories, puis les Topos, et que c‘était une des raisons (pas la seule), de l’« épuisement » du projet Bourbaki (par ailleurs tout à fait admirable (la critique est facile ...)).
Laurent Lafforgue a fait le 6 Novembre dernier (c’est donc récent) une conférence :
https://aroundtoposes.com/laurent-lafforgue-on-the-creative-power-of-categories/
Où, (dans son style assez peu diplomatique), il rend compte du peu d’intérêt de la communauté scientifique vis à vis des Topos, pendant longtemps (c’est en train de changer).
Il montre que les catégories ont un lien avec la logique :
Evidemment, pour moi qui est un grand admirateur de Patrick Dehornoy, il m’est difficile d’imaginer qu’il a passé la plus grande partie de sa vie à explorer une voie sans issue, aussi je serais intéressé par vos commentaires …..
En particulier, je vous entends dire que toutes les mathématiques peuvent être construites au-dessus de ZF (ou ZFC, ou …), et je comprends que cet objectif est une puissante motivation, mais n’existe-t-il pas une autre voie, au travers des catégories (comme l’a suggéré Lawvere) ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Supplanté par les catégories et les topos, certainement pas. En fait, il y a un truc qui est très important à retenir c'est que pour la plupart des maths, les fondations précises n'importent pas ou du moins très peu. Ceci étant dit, si une personne a un doute sur ce qu'elle a "le droit" de faire etc., le dernier recours sera dans la plupart des cas ZF(C), et certainement pas les alternatives catégoriques (sauf rare exception). D'ailleurs, il est encore compliqué de nos jours de donner un sens à des fondations catégoriques, surtout puisque dans les formulations usuelles, les catégories sont fondées sur les ensembles.
Même s'il y avait d'autres fondations, cela ne signifierait pas que la TDE est une "voie sans issue" : une grosse partie de la TDE de nos jours n'est absolument pas fondationnelle (voire la plupart ? mais je ne m'y connais pas assez pour affirmer ça), donc même si la TDE n'était pas la théorie "du fondement", elle ne serait pas une "voie sans issue".
Pour ton dernier paragraphe, concernant Lawvere; oui, certainement on peut créer d'autres choses qui fonctionnent. La théorie ETCS de Lawvere est légèrement plus faible que ZFC mais suffisante en pratique.
Mais les topoi tels que Lafforgue les envisage n'ont pas cette vocation, si je ne m'abuse. En tout cas le programme de Caramello, qui a l'air d'être sa motivation principale, n'a pas cette vocation fondationnelle, c'est un programme orienté vers des applications (en maths pures, mais des applications tout de même). Donc c'est une question tout à fait différente.
Première anicroche : un mien ami, grand informaticien devant l'Eternel, a lu le chap 0 et n'y a pas tout compris. Il m'a écrit un mail, dans lequel il disait, entre autres : "si tu ne changes pas le titre, je vote Sarkozy aux prochaines élections, et je ne t'adresse plus la parole du restant de ma vie."
Du coup, j'ai changé le titre.
Deuxième anicroche : je me suis assez vite rendu compte que si un fraichement émoulu du bac S voulait lire mon livre, il me faudrait lui expliquer l'algèbre linéaire, la topologie, des rudiments d'analyse, lui donner des exemples d'ordres partiels pour qu'il comprenne l'énoncé du lemme de Zorn, etc. Bref, impossible.
Du coup, j'ai revu mes ambitions à la baisse et j'ai écrit dans la préface qu'un niveau L3 était souhaitable pour aborder la lecture.
Troisième anicroche : je voulais me démarquer des autres ouvrages du domaine en insistant sur l'aspect fondationnel de la TDE Là, j'y suis plus ou moins arrivé, mais seulement au début. Au chap 7 on a fini de construire $\mathbb{N}, \mathbb{Z}, \mathbb{Q}, \mathbb{R}, \mathbb{C}, \mathbb{H}, \mathbb{O}, \mathbb{S}$, etc, et après il n'y a plus grand chose de fondationnel. Tout au plus au chap 13, quand j'introduis la notion de rang, je montre que $V_{\omega + \omega}$, ou même un $V_{\omega + N}$ avec $N$ assez grand suffisent amplement pour faire toutes les maths hors TDE... et après, plus rien de fondationnel.
Alors, comme dit Max : fondationnel, oui, mais dès qu'on rentre dans la théorie avancée on ne parle plus que boutique, et il faut se mettre les mains dans le cambouis...
Des outils DE RECHERCHE permettent d'avancer dans des directions unifiantes pour des théories faibles (à peu de risque d'inconsistance). En particulier quand ça "type bien" (par exemple quand E inter P(E) est vide.
Ça a rien à voir avec LA RECHERCHE en TDE qui s'occupe de l'autre bout beaucoup plus en amont : bataille sur les axiomes forts et intuitifs
La TDE version recherche est plus dans "la recherche de l'inconnu, le scan de "la nature de Dieu", par exemple via les GC qui "touchent" 0=1.
C'est très complémentaire et différent. Par exemple l'axiome du choix a une place en amont completement unique dont la nature est pas encore très bien comprise. La TDE n'y est pour rien, car elle est sans "décodage". On dit les choses comme elles sont, il n'y a pas de modélisation. D'où l'extraction des "essentiels". Par contre le prix à payer est que "c'est donné".
Et encore, ce que tu ne sais pas c'est qu'au moment où il la rédige sur son téléphone elle est déjà complètement écrite dans sa tête...
Parler de ces choses c'est bien... Si on les maitrise...
Il veut dire quoi Lafforgue au juste, concrêtement?
La théorie des ensembles comme fondation, chacun son avis.
La théorie des ensembles comme discipline, il y a assez de problèmes ouverts pour occuper des chercheurs pendant encore pas mal de temps.
Ça fait 10 ans que j'entends parler des topos comme un remêde miracle. En 10 ans, je n'ai rien vu.
Tu connais le mien.
"La théorie des ensembles comme discipline, il y a assez de problèmes ouverts pour occuper des chercheurs pendant encore pas mal de temps."
Ouais, genre encore un millions d'années, au grand minimum !
Moi au sujet des fondations, je n'ai pas trop d'avis encore tranché, vu que je n'ai rien vu d'autres (si les topos, mais c'est une blague ce truc).
Edit: je laisse mon message, mais enlève de ma tête que les topos sont une blague.
(Médor mange) = (Médor \in mangeant)
De mon téléphone.
Je n'ai pas d'avis sur HoTT Max (je pense que c'est proche de ton domaine ou pas... mais si il y a quelqu'un pour donner son avis, ce n'est pas moi) par méconnaissance totale du sujet.
J'ai modifié mon avis sur les topos car ce n'est pas le mien mais j'ai laissé le message.
J'avais suivis un seul groupe de travail sur Paris en 2015 et c'est vraiment des souvenirs qui datent (j'attendais le groupe de travail sur les groupes) et le sud du sud du 13ème arrondissements n'est pas propice à la balade quand il pleut.
Il y a un premier problème selon (d'autres) lol c'est que l'on "confond" théorie des types et théorie des catégories.
Les 2 peuvent être considérées comme des théories de fonctions. Mais la théorie des catégories est plus dans la composition de fonctions, alors que la théorie des types va "capturer" une fonction.
Les deux types de théories peuvent être mises en relation par des procédés astucieux mais je n'ai(j'ai dû faire la faute 30 fois...@AD) pas envie de raconter trop de conneries lol. Les choses ont-elles changées depuis ?
Tout comme ZF+DC est plus forte que Z.
La théorie des types est plus forte de HoTT.
La théorie des topos est plus forte que la théorie des catégories.
Après je ne sais pas si quelqu'un aura un jour les outils pour comparer la force logique de HoTT, la théorie des catégories et ZF+DC ("reverse mathématique").
Perso, c'est ce qui m’intéresse.
Dans quel système (ZF, HoTT) on trouve la force minimal pour prouver un théorème T.
Inversement, HoTT "contient ZF" essentiellement comme son fragment discret (les types $X$ tels que $x=_X y$ est vide ou contractile) , je crois que certaines variantes permettent essentiellement de retrouver ZF donc il ne doit pas y avoit de grosse différence en consistency strength. En reverse mathematics, pas sûr, je pense qu'il faudrait déjà donner un sens à la question !
(Oui, HoTT c'est relativement lié à ce qui m'intéresse, on peut y faire de l'homotopie synthétique si je comprends boen. Mais je ne me suis pas plongé dans les détails, je ne crois pas par exemple qu'on ait déjà de notion satisfaisante de catégorie ou d'$\infty$-catégorie, et c'est ça qu'il me faudrait)
Benoît Monin va faire de janvier à mars un cours intitulé "Calculabilité : Outils classiques", dans le cadre du M2 LMFI, 2h/semaine (c'est crédité de 4 ECTS, c'est pour ça).
Il va parler de généralités au début, puis, selon les desiderata des étudiants, s'orienter, soit vers les mathématiques à rebours, soit vers j'sais plus quoi. (Je ne retiens que ce qui m'intéresse, et encore avec bien des difficultés).
Ceci dit je ne sais pas :
1) Si ça t'intéresse.
2) Quelle option vont choisir les étudiants.
3) Si tu habites en RP (je crois que non).
4) Si tu as la disponibilité nécessaire (je crois que non).
5) Si le cours va avoir lieu en présentiel ou par zoom (auquel cas tu pourrais demander à suivre le cours en auditeur libre à condition que tes horaires collent).
Concernant le point 5 je pense qu'à l'heure actuelle personne à Paris 7 n'en sait rien, et même Macron doit être dans le flou artistique le plus total.
Enfin, je t'aurai transmis l'info...
Merci Martial.
J'aimerais bien suivre quelques cours du semestre 2:
Grands cardinaux
Bitcoin
Types.
Je me suis farci le poly de Prouté, autant que cela serve à quelque chose lol.
Au niveau du cours que tu me proposes en tapant le nom de l'enseignant, je tombe sur un livre avec un chapitre entier sur les mathématiques à rebours. Je suis content, en Français c'est rare... (Pour Ramsey c'est bien).
Là on est dans le plaisir.
Niveau thèse à finir:
il y a un parcours logique à l'ENS de Lyon l'an prochain qui colle parfaitement avec la tournure que je veux donner au dernier chapitre de ma thèse, c'est quand même fou. Si un logicien de Lyon (normalement c'est bon) peut m'encadrer bénévolement 6-12 mois histoire que je la présente.
Les types de HoTT proprement dit correspondent à des $\infty$-groupoïdes (tous les chemins sont inversibles). Je pense que ce qui t'intéresse et ce que tu as en tête, c'est plutôt des $(\infty, 1)$-categories. Récemment, en effet, des variantes de HoTT (essentiellement des extensions, mais des points cruciaux comme le statut de l'axiome d'univalence ou l'existence d'univers sont encore assez obscurs, au moins pour moi) ont pour but d'être une théorie des types correspondant à des $(\infty, 1)$-categories mais je crois que c'est encore au stade de la recherche.
Riehl et Shulman y travaillent notamment, et c'est le cas de beaucoup de gens.
A vrai dire, un point qui n'est pas clair pour moi est pourquoi la définition naïve de "catégorie" qu'on pourrait donner en HoTT ne convient pas (pour modéliser des $(\infty,1)$-catégories), mais j'ai peur qu'il faille se plonger dans les détails pour avoir une réponse.
Tu aurais une explication rapidos (même si incomplète) de pourquoi le truc naïf ne marche pas ?
Dans HoTT, étant donné un type A et deux éléments a et a' de type A, tu peux former un type des chemins de a vers a', mais tous ces chemins sont inversibles. Dans Riehl et Shulman, tu as une construction (via des "extensions de types") qui permet de considérer le type hom_A(a, a') (et tu as une fonction canonique des chemins au sens de HoTT de a vers a' vers hom_A(a, a')) dans le but d'avoir une correspondance entre les types (au moins ceux qui sont Segal) et les $(\infty,1)$-catégories. Je crois que ce tu dis est que l'on pourrait définir un type des $(\infty,1)$-catégories dans HoTT (je ne suis pas sûr d'avoir bien compris), mais c'est différent d'avoir une correspondance entre types et $(\infty,1)$-catégories.
Opinion personnelle : même si ça ne change rien ke suis personnellement hostile au choix politique de JoTT d'avoir popularisé ses outils en présentant les ensembles comme des cas particuliers d'objet. Le niveau de la France est celui de la Roumanie en maths école, et berner les gens ne me paraît pas efficace même si je comprends les volontés d'accès aux crédits.
Il fait savoir qu'à peu près tout objet est un cas particulier de tout autre objet dès que des conditions très simples sont réunies. Les slogans de vente trompeurs ont comme inconvénients de faire oublier, voire de cacher ça et de faire partir les gens sur de mauvaises bases des le départ.
La différence OPERATOIREMENT essentielle entre le catégorisme qui étudie un fragment de science très consistant et l'ensemblsme qui spécule à la frontière de l'inconsistance (ie limites de Dieu) est que dans un cas fondamentalement on ne souhaite pas identifier A avec 1=>A. Alors que dans l'autre si.
Cette identification (qu'on pourrait qualifier de positionnement-en-platonisme) ne sert pas tant à étudier les théories faibles qu'à éviter la verbosite de qui risque de tout noter dans les théories fortes et speculantes.
Il est à noter que des les catégories CCC, sans être vraiment faite, elle est néanmoins partiellement importée. Les topos ne sont qu'une cerise sur gâteau du CCC-isme.
On a des intervenants célèbres sur le forum (je parle de fdp par exemple) qui, bien que certes ne connaissant pas ça, se rangeraient (au conditionnel) à l'option de traiter A,B d'une part et A=>B d'autre part comme d'une nature différente.
(Bon, s'il y a 150 mots je prends aussi).
Je n'avais pas vu ton message.
Je vais essayer de faire un petit résumé lisible pour un non spécialiste des 2 domaines. (L'intro de ma thèse quoi :-D)
Par MP par contre.
A propos de spécialistes, il y a un seul énoncé dont je suis convaincu :
$$\forall D, domaine(D) \Rightarrow \neg(\text{ je suis spécialiste de } D),$$
lol.
C'est une faute de frappe ou ça reflète la vérité ?
(T'es pas obligé de répondre , lol).
Mattar l'entretien bien aussi ;-).
Faute de frappe.
La majorité des personnes sur le forum, on se connait pas leur sexe...
Et c'est tant mieux lol.
C'est Christophe qui entrenenait le suspense sur le genre de Mattar (le boss de ce forum).
Et pour compliquer le tout, la personne dont je respecte le plus la thèse est transgenre...
Fin du HS.
Par contre tu penses changer la mise en page Latex de ton livre? Car j'ai l'impression qu'elle est différente de la standart.
Si c'est un choix, c'est ton livre, je n'ai pas à juger.
Tu as le temps pour répondre, l'éditeur c'est pas pour demain, lol.
-- Schnoebelen, Philippe
Pour l'instant je gère les chaps un par un, et c'est seulement à l'étape finale que je fusionnerai tout ça, donc ça ne serait pas un problème de tout recompiler... sauf évidemment si ça me nique complètement ma mise en page :