Logique + catégories / topos : éclaircissements "vus de loin" pour un non spécialiste

f_g
f_g
Modifié (November 2023) dans Fondements et Logique
Bonjour à tous.
Je lis depuis plusieurs mois énormément de choses sur la logique mathématique et ses développements post Gödel en théorie de la démonstration. Je précise que je ne suis pas mathématicien mais plutôt physicien.
Je pensais avoir bien compris les différentes visions globales possibles de la logique moderne, en me frottant à Cori/Lascar, en lisant pas mal (en essayant) Jean-Yves Girard, Giuseppe Longo etc... J'avais aussi entendu parler des liens faits dans la logique moderne avec la notion de topos. Mais récemment la lecture d'un livre de Badiou (qui traite beaucoup de la logique interne des topoi : le Court traité d'Ontologie transitoire) a beaucoup perturbé ma compréhension globale : j'ai réalisé que Jean-Yves Girard (que je crois pourtant être en France l'un des plus avancés en matière de logique mathématique) n'utilise pas une seule fois le terme "topos" (il parle d'interprétation catégorique, de catégorie cartésienne fermée, dont je sais qu'on peut les obtenir à partir de topoi mais... il ne parle pas à ma connaissance de topoi... ). L'argument de Badiou étant qu'une approche par les topoi implique qu'une décision ontologique quant à l'univers mathématique que l'on se fixe implique une logique immanente à cet univers (j'ai lu ici et là qu'un topos avait bien sa logique interne. Donc mon sentiment est que Badiou, non mathématicien certes, ne délire pas).
Je suis donc un peu perdu. Est-ce que quelqu'un saurait m'expliquer ce paradoxe apparent, qui veut que l'un des logiciens les plus en pointe n'utilise jamais la notion ? Est-ce que sa vision en est très proche mais pas tout à fait identique ? Quelles sont les différences majeures entre l'approche par la théorie des topoi et une approche à la Girard par les catégories, les catégories cartésiennes fermées, les algèbres de Von Neumann & co ?
Merci par avance

Réponses

  • Alesha
    Modifié (November 2023)
    f_g : Bonjour, Girard s'intéresse à la théorie des démonstrations, c'est-à-dire qu'il ne s'intéresse pas tant à la prouvabilité d'un énoncé qu'à ses preuves et souhaite pouvoir distinguer des preuves "différentes" (la notion de "preuves différentes" ne va pas forcément de soi). La notion de topos n'internalise pas la notion de preuve donc on ne va pas pouvoir en faire grand chose si on s'intéresse aux preuves en tant qu'objets mathématiques.  
  • Médiat_Suprème
    Modifié (November 2023)
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Médiat_Suprème : bonjour. Pour ma part, je voudrais bien avoir accès aux textes d'Alain Prouté, mais il semble, sauf erreur, ne plus être disponibles. Sais-tu où les trouver ?
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • @Thierry Poma Sur la WayBackMachine. Par exemple, le cours d'introduction à la logique catégorique peut se trouver ici.
  • Médiat_Suprème
    Modifié (November 2023)
    Les liens que j'ai donnés sont en accès libre…
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Oui, mais le lien de la WaybackMachine que j’ai donné se fait vers une sauvegarde de la page d’Alain Prouté : on y trouve tous ses écrits.
  • @dp : bonsoir. Je te remercie beaucoup.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • Comme le dit Alesha, Jean-Yves Girard fait de la théorie de la démonstration. La logique des topos, c'est plutôt du côté théorie des modèles, notamment avec la notion de topos classifiant et de modèle générique.
    Bien sûr, ce n'est pas entièrement disjoint, mais ce n'est tout de même pas la même chose.
  • Merci pour vos réponses. Le cours de Mr Prouté semble extrêmement complet et d'une remarquable pédagogie (quoique très complexe pour quelqu'un qui n'est pas du métier...). Ma curiosité en ressort grandie puisque ce que j'y lis (en diagonal) semble tout de même bien être que les outils les plus fondamentaux de la théorie de la démonstration (par exemple le calcul des séquents et l'interprétation de tous les connecteurs logiques qui vont avec etc...) semble être codable de façon extrêmement générale dans la théorie des topoi. Il y a même un chapitre sur les preuves.

    Donc ma question serait la suivante : est-ce que la raison pour laquelle certains théoriciens ne l'utilisent pas est simplement qu'elle est trop puissante ou encore peu pratique/naturelle? Ou est-ce qu'il y aurait au contraire (ou en plus) le fait que l'on ait besoin en théorie de la démonstration de structures simples mais qui ne sont pas des topoi? (en effet, c'est toujours surprenant pour un béotien de voir des structures d'une aussi fantastique généralité, puis de lire qu'une algèbre de Boole à deux éléments n'est pas un topos ^^)
  • Alesha
    Modifié (November 2023)
    @f_g : Je vais essayer de reformuler ce que GaBuZoMeu et moi-même avons écrit ci-dessus. Les textes de Prouté sont très intéressants mais ils sont hors-sujet et après les avoir lus, en effet, tu ne serais pas plus avancé sur la raison pour laquelle Girard n'utilise pas la notion de topos. Un topos est une catégorie, c'est-à-dire que tu as des objets et des morphismes : pour simplifier, au lieu de parler topos, catégories, objets et morphismes, tu peux voir le cours de Prouté ou les topos comme une généralisation de la théorie des ensembles, c'est-à-dire que tu as juste des ensembles et des fonctions (donc rien qui correspond aux preuves au sujet de ces ensembles et ces fonctions). Ce que fait Prouté avec son calcul des séquents, c'est qu'il montre que si tu peux prouver un énoncé dans un certain calcul des séquents (un calcul intuitionniste), alors l'interprétation de cet énoncé est vraie dans n'importe quel topos. Tout ce qui intéresse Prouté ici, c'est si un énoncé est prouvable ou non.
    Ce qui intéresse Girard, c'est de prendre un énoncé (par exemple A /\ A => A) et de regarder les différentes preuves de cet énoncé et les considérer comme des objets mathématiques (ici, par exemple, il y a deux preuves complètement différentes de A /\ A => A : l'une part de A => A et en déduit  A /\ A => A du fait que tu peux toujours "affaiblir à gauche" du connecteur de la conjonction - c'est-à-dire que si tu as une preuve de C => D alors tu as une preuve de B /\ C => D pour tout B - et l'autre part de  A => A et en déduit  A /\ A => A du fait que tu peux toujours "affaiblir à droite" du connecteur de la conjonction - Girard veut considérer les deux preuves comme deux objets mathématiques différents) : il n'y a rien qui correspond à ces preuves dans un topos, ce qu'il y a dans un topos c'est ce qui correspond aux énoncés prouvables (je me répète un peu).
    En outre, si tu commences à avoir des objets mathématiques correspondant à des preuves différentes d'un même énoncé, alors ces objets mathématiques peuvent eux-mêmes se substituer à des objets qui vont être des choses primitives dans un topos. Par exemple, souvent on veut considérer des topos avec un objet des entiers naturels, c'est-à-dire que les entiers naturels sont donnés et tu peux exprimer des énoncés très compliqués (ce que montre le cours de Prouté, c'est que tu peux exprimer tous les énoncés habituels que tu as en mathématiques). Ce que va faire Girard, c'est au contraire considérer des preuves différentes d'un même énoncé comme des entiers naturels mais ces entiers naturels eux-mêmes ne font pas partie du langage pour exprimer des énoncés : tu auras un énoncé qui correspond au type des entiers naturels - on dit "objet" quand on fait des topos et "ensemble" quand on fait de la théorie des ensembles - et on dit "type" quand on fait du Girard), les entiers naturels seront (des quotients) des preuves de cet énoncé. 

    En conclusion, plutôt que de voir un domaine qui s'appelle "logique", il vaut mieux considérer qu'il y a des domaines distincts : la théorie de la démonstration (ce que fait Girard), où les topos ne jouent pas un rôle prééminent et, par ailleurs la théorie des modèles, où les topos peuvent jouer un rôle important; tu as aussi la théorie des ensembles et tu peux voir aussi les topos comme une généralisation de la théorie des ensembles. Ceux qui font de la théorie des modèles ou de la théorie des ensembles ne s'intéressent pas aux preuves (en tant qu'objets mathématiques) mais à la prouvabilité (le fait qu'il y ait deux preuves distinctes de A /\ A => A ne les intéresse pas, ce qui les intéresse qu'il y en ait au moins une) tandis que ceux qui font de la théorie de la démonstration (Girard, par exemple) vont s'intéresser aux différentes preuves d'un même énoncé.
    Si tu regardes d'autres textes de Prouté, tu verras, à titre de confirmation, qu'il ne fait pas de la théorie de la démonstration (au sens de Girard); par exemple : "This is of course equivalent to saying that proofs have no semantics at all, and by the way it entails the proof irrelevance principle (and is actually much more radical, since all proofs of all statements appear to be “equal”)." https://smimram.gitlabpages.inria.fr/lhc/slides/2023/proute.pdf

    Ta dernière phrase est un peu curieuse : c'est quand même assez contraignant pour une catégorie d'être un topos, ce qui n'a rien d'étonnant puisque tu dois pouvoir y interpréter n'importe quel énoncé habituel (du moins quand on a un objet des entiers naturels), tu vois bien que tu risques d'avoir du mal à faire de l'analyse dans une algèbre de Boole à deux éléments!

    N. B. J'aime bien la définition 17 page 67 de la notion de catégorie dans le cours de Prouté : "Une « catégorie » C est la donnée de (...)". Sur une autre fil, un intervenant prétendait qu'écrire "est la donnée de" ne veut rien dire!
  • "N. B. J'aime bien la définition 17 page 67 de la notion de catégorie dans le cours de Prouté"

    À noter que c'est bien la définition classique, qui postule l'unicité de la source et du but des morphismes, contrairement à la définition de Foys / Adamek, Herrlich, et Strecker.
  • @GG : Tu fais référence à quel livre? Dans The Joy of cats par Adamek, Herrlich et Strecker, on a la définition habituelle : "Observe that condition (c) guarantees that each A-morphism has a unique domain and a unique codomain." De même pour les fonctions : "A function with domain $X$ and codomain $Y$ is a triple $(X, f, Y )$, where $f \subseteq X \times Y$ is a relation such that for each $x \in X$ there exists a unique $y \in Y$ with $(x,y) \in f$".

  • GG
    GG
    Modifié (November 2023)
    @Alesha, c'est bien ce livre. Mais dans mon édition de 2004, (as-tu la même ?), la phrase d'après est :

    However, this condition is given for technical convenience only, because whenever all other conditions are satisfied, it is easy to "force" condition (c) by simply replacing each morphism [...] For this reason, when verifying that an entity is a category, we will disgard condition (c).

    J'en avais conclu, à tort je m'en rends compte maintenant en relisant, que pour les auteurs, une catégorie était définie sans la condition (c) (ce que tu appelles une protocategory ?). En fait, il semble qu'ils veuillent dire que (c) fait vraiment partie de la définition, mais qu'il n'y a pas besoin de la vérifier ! :)

    En conclusion et jusqu'à preuve du contraire, tout le monde s'accorde sur une définition des catégories (et de deux, trois autres équivalentes, dont l'une  qui permet de n'envisager que les morphismes comme notion primitive). Il en résulte, si l'on veut être précis et c'est la moindre des choses en mathématiques, que les fonctions considérées comme synonymes des graphes fonctionnels ne sont pas les morphismes de la catégorie des ensembles, définitivement.
  • Foys
    Modifié (November 2023)
    N. B. J'aime bien la définition 17 page 67 de la notion de catégorie dans le cours de Prouté : "Une « catégorie » C est la donnée de (...)". Sur une autre fil, un intervenant prétendait qu'écrire "est la donnée de" ne veut rien dire!

    @Alesha il y a une différence entre "c'est la donnée d'un $d-uplet$" suivi de propos explictes et implémentables (comme une structure en C ou un record en COQ) qui sont précis et adressés à des matheux de niveau DEA/master 2 et ceci:

    "Une fonction, c'est juste la donnée d'un ensemble de départ 𝐴, d'un ensemble d'arrivée 𝐵 et de la donnée d'un élément 𝑓(𝑥) de 𝐵 pour tout élément de 𝑥 de 𝐴,"
     Adressé à des enfants (sous le préjugé hallucinant qu'un débutant a plus de facilités à comprendre un énoncé vague et imprécis - qu'un pro refuserait - qu'un énoncé précis) Se donner "f(x) pour tout x dans A" ne veut rien dire. C'est rigolo de se faire l'avocat du diable mais de là à être de mauvaise foi (c'était une digression HS; je n'interviendrai pas plus dans ce fil où les intervenants ont déjà dit plus haut tout ce que j'aurais pu dire).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Alesha
    Modifié (November 2023)
    C'est pénible qu'un intervenant de mauvaise foi vienne accuser les autres d'être de mauvaise foi. Ignorons ce troll!

    @GG: Je n'ai pas trouvé où, dans ce livre, s'applique cette remarque qu'on peut se dispenser de vérifier la condition (c). La notion de protocategory sert uniquement à décrire la catégorie qu'elle engendre, on pourrait sûrement reformuler cette remarque ainsi : pour vérifier qu'on.a bien affaire à une catégorie, il suffira de vérifier qu'on a affaire à une protocategory qui l'engendre. Il faudrait trouver un exemple dans le livre pour s'en convaincre.
  • @Alesha, ok, d'accord.
  • @Alesha merci pour la reformulation, je vois mieux l'idée. Cela dit Girard fait tout de même une utilisation assez massive de la théorie des catégories, en particulier dans ce qu'il appelle son niveau -2, d'où ce qui me perturbait (en revanche, c'est vrai que lorsqu'il parle de "dynamique" des preuves, il fait référence à son "niveau -3", jugeant le -2 insatisfaisant). S'il pouvait être aussi pédagogue que Prouté, cela m'aiderait beaucoup... J'en profite pour dire que je suis preneur pour n'importe quelle référence bien faite sur le sujet (pour la théorie de la démonstration classique, j'avais été impressionné par la clarté du bouquin de Takeuti, Proof Theory, entre autres).
    c'est quand même assez contraignant pour une catégorie d'être un topos, ce qui n'a rien d'étonnant puisque tu dois pouvoir y interpréter n'importe quel énoncé habituel (du moins quand on a un objet des entiers naturels)
    Effectivement dit comme ça, je suis d'accord. Mais quand on tombe "de l'extérieur" devant la définition d'un topos (catégorie dotée de limites et colimites finies, exponentielles etc...), ça n'est pas évident en soi que l'on peut y interpréter n'importe quel énoncé habituel^^ Je vais continuer à bosser, en somme^^

  • Alesha
    Modifié (November 2023)
    @f_g: Le texte de Girard auquel tu fais allusion et le texte et Prouté ne sont pas de même nature. Je n'ai pas regardé en détail, mais il n'y a peut-être rien dans le contenu du cours de Prouté que GaBuZoMeu ne connaissait déjà il y a 50 ans, c'est plus facile d'être pédagogue quand on enseigne des choses classiques, bien connues, sur lesquelles on a du recul. L'approche de la théorie de la démonstration qui consiste à voir les types comme des objets de catégories (mais pas des topos) et les preuves comme des morphismes est classique et il y a sûrement des références bien écrites à ce sujet (maintenant, rien ne me vient à l'esprit, mais ça me viendra peut-être plus tard), mais le texte de Girard ici se veut iconoclaste, c'est-à-dire qu'il veut sortir de ce cadre classique (qu'il a lui-même longtemps respecté) : c'est une approche nouvelle, personnelle, sur laquelle on n'a pas le même recul. Si tu veux comprendre l'approche classique avec les catégories, tu trouveras sûrement des références pédagogues, si tu veux comprendre l'approche personnelle de Girard "dépassant" le cadre des catégories, tu devras sûrement te contenter des textes de Girard ou d'articles de recherches. Dans ce dernier cas, il sera sûrement vain de chercher un lien, même ténu, avec les topos. 

     En un mot, si ça t'aide pour essayer de comprendre où Girard veut en venir (quitte à le trahir) : la vision "classique" de la théorie de la démonstration avec les catégories, c'est qu'on ne distingue pas une preuve de sa forme normale donc on oublie la "dynamique" de l'élimination des coupures, or "au niveau -3", on garde cette distinction (je ne prétends pas résumer son approche en une phrase, c'est juste au cas où ça t'aide à comprendre les enjeux).

  • Je remets ici des notes d'exposés que j'avais fait, il y a bien longtemps, pour des théoriciens des modèles sur l'interprétation des formules dans un topos et la construction du topos classifiant d'une théorie géométrique. Ça ne parle que de topos de Gothendieck, pas de topos élémentaires.
  • Ok, effectivement c'est plus clair, merci !
Connectez-vous ou Inscrivez-vous pour répondre.