Illustration de la théorie des catégories : logique (2021)

 (abuseofnotation.github.io)
2 points par GN⁺ 2024-10-27 | 1 commentaires | Partager sur WhatsApp
  • La logique part de propositions atomiques tenues pour vraies, puis construit des propositions plus grandes avec des opérateurs comme and, or et implies, et, comme en théorie des catégories, la composition y est essentielle
  • La logique classique interprète les propositions comme des valeurs booléennes vrai/faux, les opérateurs logiques comme des fonctions booléennes, et traite négation, conjonction, disjonction, implication et équivalence à l’aide de tables de vérité
  • L’interprétation BHK de la logique intuitionniste voit les propositions comme des objets munis de preuves ; A ∧ B s’interprète comme une paire de preuves, et A → B comme une fonction transformant une preuve de A en preuve de B
  • Dans certaines catégories, les objets correspondent aux propositions et les morphismes aux preuves ; dans un ordre, A ≤ B représente A → B sous la forme d’un preorder ou d’un ordre partiel
  • La logique intuitionniste correspond, du point de vue de l’ordre, à une algèbre de Heyting, et, plus généralement en théorie des catégories, à une catégorie bicartésienne fermée ; conjonction, disjonction, vrai, faux et implication y correspondent respectivement à meet/join, objet terminal/initial et objet exponentiel

La logique à partir des propositions

  • La logique traite de règles formelles cohérentes avec elles-mêmes, indépendamment de l’observation, et constitue un système permettant de conclure ou de prouver qu’une chose est vraie à partir d’une autre connue
  • Une théorie mathématique peut être vue comme de la logique à laquelle on ajoute des définitions supplémentaires
    • La théorie des ensembles peut être définie en ajoutant aux axiomes logiques standard le concept primitif de relation d’appartenance à un ensemble
  • Pour démarrer la logique, il faut un ensemble initial de propositions admises comme vraies ou fausses
    • On les appelle prémisses, propositions atomiques ou primary propositions
  • Deux propositions ou plus deviennent une proposition composée à l’aide d’opérateurs logiques comme and, or et implies/entails
    • ∧ signifie and
    • ∨ signifie or
    • → signifie follows, ou l’implication
  • Une proposition composée peut à son tour être recomposée avec d’autres propositions, comme une proposition atomique

Modus ponens et tautologies

  • Le modus ponens est un ancien schéma logique selon lequel, si A est vrai et A → B est vrai, alors B est aussi vrai
    • Sa forme est (A ∧ (A ⇒ B)) → B
    • On peut l’exprimer avec un exemple comme : « Socrate est un homme, et si un homme est mortel, alors Socrate est mortel »
  • La logique ne traite pas seulement d’opérations isolées, mais aussi de combinaisons de plusieurs opérateurs logiques et de leurs relations
    • La relation entre and et implies apparaît dans le modus ponens
    • La distributivité de and et or est également un sujet majeur
  • Une tautologie est une proposition toujours vraie, quelle que soit la valeur de vérité de ses propositions constitutives
    • Pour le modus ponens, que A et B soient vrais ou faux, la formule entière reste toujours vraie
    • Une proposition toujours fausse s’appelle une contradiction
    • Si l’on applique not à une tautologie, on obtient une contradiction ; si l’on applique not à une contradiction, on obtient une tautologie
  • Une proposition dont la vérité ou la fausseté dépend des valeurs prises s’appelle un contingent statement et sort du champ principal d’intérêt de la logique
  • La tautologie la plus simple est le principe d’identité, selon lequel chaque proposition implique elle-même

Schémas d’axiomes et systèmes logiques

  • Les tautologies servent de base aux schémas d’axiomes et aux règles d’inférence
  • Un schéma d’axiome est une formule contenant des variables de position, que l’on peut remplacer par des propositions pour produire une proposition concrète
    • Si l’on retire les couleurs ou les propositions concrètes du modus ponens, il en reste la structure générale
    • On peut insérer dans cette structure des propositions atomiques ou composées pour obtenir un énoncé particulier de modus ponens
  • Les règles d’inférence peuvent être écrites presque de la même façon que les schémas d’axiomes, et les schémas d’axiomes peuvent aussi s’appliquer comme des règles d’inférence
  • Toute tautologie peut servir de schéma d’axiome
  • Un système logique, ou système formel, est un ensemble de schémas d’axiomes et de règles d’inférence qui permet de générer toutes les propositions possibles
    • Un exemple présente un système composé de cinq schémas d’axiomes et de la règle d’inférence du modus ponens
    • Le fait qu’un tel système logique soit complet est lié au théorème de complétude de Gödel

Interprétation en fonctions de vérité de la logique classique

  • La logique classique repose sur la dichotomie selon laquelle toute proposition est soit vraie, soit fausse
  • Dans l’interprétation classique, les propositions et les opérateurs sont définis ainsi
    • Les propositions sont des valeurs booléennes, vraies ou fausses
    • Les opérateurs logiques sont des fonctions qui prennent une ou plusieurs valeurs booléennes et renvoient une valeur booléenne
  • La négation ¬p est une opération unaire qui transforme le vrai en faux et le faux en vrai
    • On peut exprimer la même chose avec une table de vérité
    • L’élimination de la double négation se démontre par le fait qu’appliquer deux fois la négation ramène à la valeur de départ
  • and prend deux valeurs booléennes et ne renvoie vrai que si les deux sont vraies
    • p ∧ q → p
    • p ∧ q → q
  • or renvoie vrai si au moins une des deux valeurs booléennes est vraie
    • p → p ∨ q
    • q → p ∨ q
  • implies, ou condition matérielle, s’écrit p → q et n’est faux que lorsque p est vrai et q est faux
    • En logique classique, p → q équivaut au cas où ¬p ∨ q est vrai
  • if and only if, ou iff, est vrai lorsque deux propositions ont la même valeur
    • P ↔ Q est équivalent à P → Q ∧ Q → P
  • On peut démontrer l’équivalence entre p → q et ¬p ∨ q non seulement avec des tables de vérité, mais aussi avec des axiomes et des règles d’inférence
    • Une démonstration complète de l’équivalence exige une preuve dans les deux sens

Logique intuitionniste et interprétation BHK

  • La logique intuitionniste considère la preuve non comme la découverte d’une vérité universelle, mais comme une construction
  • Dans cette perspective, on ne peut pas utiliser la dichotomie selon laquelle toute proposition est nécessairement vraie ou fausse
    • Une proposition peut être non démontrable non parce qu’elle est fausse, mais parce qu’elle se situe hors du champ du système logique donné
    • La conjecture des nombres premiers jumeaux est souvent présentée comme un tel exemple
  • Dans l’interprétation de Brouwer–Heyting–Kolmogorov (BHK), l’accent est mis sur les preuves plutôt que sur les propositions
    • Une proposition est quelque chose qui possède une preuve
    • Les opérateurs logiques sont des constructions qui fabriquent des preuves à partir d’autres preuves
  • Une preuve de A ∧ B est une paire constituée d’une preuve de A et d’une preuve de B, c’est-à-dire un product
  • A → B signifie qu’il existe une fonction transformant une preuve de A en preuve de B
    • L’ensemble des preuves de A → B s’exprime comme l’ensemble des fonctions de A vers B, c’est-à-dire un hom-set
    • Si cet ensemble est vide, il n’existe aucun moyen de transformer une preuve de A en preuve de B
  • L’interprétation BHK n’a pas d’opérateur iff distinct, mais elle a des flèches
    • Lorsque des fonctions existent de A vers B et de B vers A, les deux propositions sont traitées comme équivalentes
    • Du point de vue des ensembles, c’est le cas où les ensembles de preuves des deux propositions sont isomorphes
  • La négation ne signifie pas simplement l’absence de preuve ; il faut montrer que l’hypothèse de la vérité de A mène à une contradiction
    • ⊥ joue le rôle d’une preuve d’une formule sans preuve, c’est-à-dire de False ou de bottom value
    • En BHK, ¬A se lit A → ⊥
    • En théorie des ensembles, ⊥ est représenté par l’ensemble vide

Voir la logique comme une catégorie

  • L’interprétation BHK fournit une perspective de haut niveau pour interpréter la logique via la théorie des catégories
  • Certaines catégories peuvent être vues comme des systèmes logiques
    • Les objets sont des propositions
    • Les morphismes sont des preuves
  • Toutes les catégories ne deviennent pas des systèmes logiques ; il faut des conditions garantissant qu’il existe des objets correspondant aux propositions logiquement valides, et pas d’objets correspondant aux propositions invalides
  • Les catégories satisfaisant ces conditions sont appelées catégories bicartésiennes fermées
  • Comme cas simple, si l’on considère d’abord un ordre, un système logique et un ensemble de propositions atomiques forment une catégorie
    • S’il n’existe qu’une seule façon d’aller de A à B, ou si l’on ignore leurs différences, on obtient un preorder
    • Si l’on identifie comme équivalentes les propositions qui s’impliquent mutuellement, on obtient un ordre partiel
    • A ≤ B signifie A → B
  • Dans un diagramme de Hasse, lorsque A est sous B, alors A → B est vrai

Correspondances en théorie de l’ordre pour les opérateurs logiques

  • Les opérateurs logiques and et or apparaissent comme product et sum dans l’interprétation BHK, et correspondent, en théorie de l’ordre, à meet et join
  • Pour former un système logique, il faut pouvoir combiner n’importe quelles deux propositions avec and ou or, donc l’ordre doit posséder un meet et un join pour tous ses éléments
    • Un tel ordre s’appelle un lattice
  • Une loi importante entre and et or est la distributivité
    • Si, pour tous A, B, C, on a A ∧ (B ∨ C) ≅ (A ∧ B) ∨ (A ∧ C), alors on a un distributive lattice
  • Pour représenter la logique intuitionniste, le lattice doit aussi contenir des éléments correspondant à True et False
    • False s’écrit ⊥ et est lié au principe d’explosion, selon lequel, à partir d’une preuve de False, on peut démontrer n’importe quelle proposition
    • True s’écrit ⊤ ; toute proposition l’implique, mais il ne permet pas à lui seul d’en tirer un contenu significatif
  • Dans un ordre, True et False sont respectivement le plus grand et le plus petit objet
    • En termes catégoriques, ils correspondent à l’objet terminal et à l’objet initial
    • Un lattice possédant un plus petit et un plus grand élément est un bounded lattice

Objet d’implication et objet exponentiel

  • Un lattice représentant un système logique doit disposer, pour chaque paire A, B, d’un objet d’implication représentant la proposition selon laquelle A implique B
  • Cet objet est défini à partir de la structure du modus ponens
    • Il faut que A ∧ (A ⇒ B) → B soit vrai
  • Cette seule condition ne suffit pas
    • D’autres objets, comme A ⇒ B ∧ C ou A ⇒ B ∧ C ∧ D, pourraient aussi prendre cette place
    • Le véritable A ⇒ B est le plus grand des objets X satisfaisant A ∧ X → B
  • En théorie de l’ordre, A ⇒ B est appelé exponential element ou relative pseudo-complement
    • C’est le plus grand X tel que A ∧ X ≤ B
  • Logiquement, le proposition d’implication A ⇒ B est la proposition X la plus triviale satisfaisant A ∧ X → B
  • Catégoriquement, il se définit comme un objet exponentiel ou un objet d’homomorphismes internes
    • Il doit exister un morphisme A × X → B
    • Et pour tout autre objet candidat ayant la même propriété, il doit exister un morphisme unique vers le véritable objet exponentiel
  • Cette définition de l’objet d’implication correspond à la logique intuitionniste
    • En logique classique, à cause du tiers exclu, A ⇒ B se simplifie en ¬A ∨ B
  • Comme meet, join et l’objet d’implication, A ⇒ B est défini de manière unique à isomorphisme près

Algèbre de Heyting et catégorie bicartésienne fermée

  • La logique intuitionniste se compose de True, False, and, or et implies
  • Exprimée sous forme d’ordre, elle devient une algèbre de Heyting
    • Elle possède join et meet
    • Elle possède un plus grand et un plus petit objet
    • Elle possède un objet d’implication
  • Un système de logique intuitionniste peut être vu comme une algèbre de Heyting
    • and et or correspondent à meet et join
    • True et False correspondent au plus grand et au plus petit objet
    • implies correspond à l’objet exponentiel
  • Si l’on adapte la même définition à une catégorie générale, on obtient une catégorie bicartésienne fermée
    • Elle possède product et coproduct
    • Elle possède un objet initial et un objet terminal
    • Elle possède un objet exponentiel
  • Un système de logique intuitionniste peut aussi être vu comme une catégorie bicartésienne fermée
    • and et or correspondent à product et coproduct
    • True et False correspondent à l’objet terminal et à l’objet initial
    • implies correspond à l’objet exponentiel
  • Un lattice suivant la logique classique doit, en plus d’être borné et distributif, être complémenté
    • Pour chaque proposition A, il existe un ¬A unique satisfaisant A ∨ ¬A = 1 et A ∧ ¬A = 0
    • Un tel lattice s’appelle une algèbre booléenne

Une preuve simple en logique catégorique

  • A ∨ ⊤ ≅ ⊤ découle immédiatement de la définition de join
    • Le join est la plus petite borne supérieure supérieure ou égale aux deux objets
    • Comme le seul objet supérieur ou égal à ⊤ est ⊤ lui-même, le join de n’importe quel A avec ⊤ est ⊤
    • Logiquement, c’est la tautologie « n’importe quel A ou True, c’est True »
  • Si A → B, alors A ∨ B = B
    • Si l’un des deux objets est au-dessus de l’autre, le join est l’objet situé plus haut
    • On peut voir cela comme une généralisation de A ∨ ⊤ = ⊤
    • Car pour tout objet A, on a toujours A → ⊤
  • Le principe d’identité se démontre aussi à l’aide de l’objet d’implication
    • A ⇒ A est le plus grand X satisfaisant A ∧ X → A
    • Cette condition vaut pour tout X, donc l’objet maximal est ⊤
    • Ainsi, A → A est toujours vrai
  • Si A implique sémantiquement B dans tous les modèles, c’est-à-dire A ⊨ B, alors A ⇒ B correspond aussi à ⊤
    • Puisque A implique déjà B, on a A ∧ X → B pour tout X
    • On appelle aussi cela le théorème de déduction

Construire la logique avec une algèbre de Heyting libre

  • Pour raisonner logiquement, on commence par choisir les propositions atomiques à utiliser selon le domaine du problème
  • Si le type de logique choisi est la logique intuitionniste, il faut dessiner, pour tous A et B, un graphe contenant des propositions composées comme A ∧ B et A ∨ B
  • Comme il faut aussi inclure les compositions de propositions composées, la liste complète devient infinie
  • Pour savoir si une proposition en implique une autre, on suit les chemins des flèches partant de la proposition de départ
  • Faire de la logique consiste à trouver un chemin entre ce que l’on sait déjà et ce que l’on veut prouver, ou à construire une preuve en manipulant celles dont on dispose déjà
  • En logique intuitionniste, il est généralement difficile de prouver qu’un fait est inaccessible à partir des axiomes, autrement dit qu’il n’est pas démontrable

À lire aussi

1 commentaires

 
GN⁺ 2024-10-27
Commentaires sur Hacker News

  • Cette page est vraiment excellente, et je suis tombé dessus plusieurs fois en étudiant le sujet
    Cela dit, je donnerais quand même ma préférence à l’apprentissage avec Milewski. Apprendre cela est un voyage, et l’auteur de ct-illustrated semble encore être au milieu du chemin
    Milewski, lui, a déjà parcouru cette route plusieurs fois, donc son livre et son blog sont de bons points de départ
    https://github.com/hmemcpy/milewski-ctfp-pdf Book
    https://bartoszmilewski.com/2014/10/28/category-theory-for-p... Blog

    • J’ai lu une douzaine de chapitres du début de Milewski, et si les premiers chapitres étaient vraiment bons, son style qui ne donne pas de définitions et notations précises devient de plus en plus agaçant
      Il semble penser qu’écrire dans une prose légère et imprécise rend forcément les choses plus faciles à comprendre, mais à cause de cela c’est presque inutilisable comme ouvrage de référence
      Ce n’est absolument pas le cas¹
      ¹) https://news.ycombinator.com/item?id=41756286
    • Je n’arrive pas à comprendre ce que bartoszmilewski raconte, donc ce livre ne me semble d’aucune utilité
      En revanche, au travail, j’utilise la théorie des catégories sur l’ensemble de mon modèle de domaine

  • Cela avait déjà été discuté auparavant sous une autre URL
    https://news.ycombinator.com/item?id=28660131 (2 commentaires)
    https://news.ycombinator.com/item?id=28660157 (112 commentaires)

  • Au début du livre, en comparant les mathématiques à la science ou à l’ingénierie, je suis tombé sur cette belle phrase
    « Pour cette raison, les mathématiciens se retrouvent dans la position étrange, voire singulière, de devoir toujours défendre ce qu’ils font du point de vue de sa valeur pour d’autres disciplines. Encore une fois, dans n’importe quel autre domaine académique, cela serait jugé absurde. »
    C’est une idée à laquelle toute personne ayant étudié un domaine qui ne mène pas directement à des résultats rentables peut s’identifier, et il est réconfortant d’entendre que même les gens doués avec les nombres doivent lutter contre le rasoir de Milton Friedman

    • Dans ce cas, il est heureux qu’une grande partie des projets en « études culturelles » soient en réalité directement financés par le département de la Défense et le département d’État américains
      Aujourd’hui, l’ensemble des recherches en « postcolonialisme » n’est rien d’autre que le back-end du soft power américain, et en cas de guerre ce sera probablement aussi le back-end du hard power

  • Si les cercles intérieurs sont toujours centrés verticalement, les schémas de type cercle dans le cercle ne tiennent pas très bien à l’échelle

  • Existe-t-il des retours d’expérience où la théorie des catégories a permis de résoudre utilement un problème de CS/SWE qu’on n’aurait pas pu résoudre sans elle ? Les monades ne comptent pas, parce qu’on les inventerait naturellement si la situation l’exigeait
    J’ai étudié cela pendant un an en master, puis j’ai fini par abandonner

    • Il n’existe aucun problème qui ne puisse pas être modélisé sans théorie des catégories
      L’un des théorèmes les plus fondamentaux de la théorie des catégories, le lemme de Yoneda, dit directement que tout problème exprimé dans le langage des catégories peut être traduit dans le langage des ensembles et des fonctions. Il en va de même pour tous les objets mathématiques définis à partir d’ensembles, donc on peut toujours remplacer un nom par sa définition
      Ce que le langage catégorique apporte au cadre implicite d’une théorie ne peut pas dépasser la définition de « catégorie », et cette définition est très réduite. C’est un peu comme demander pourquoi on utilise les groupes plutôt que « une opération sur un ensemble munie de l’associativité, de la fermeture, d’un élément neutre et d’inverses », formulation pourtant plus accessible
      L’algèbre abstraite repose sur une bibliothèque de définitions qui désignent des types d’opérations sur des ensembles assez simples pour être suffisamment fréquents. Les outils ou techniques ne sont pas le genre de choses qu’on trouve dans une définition
      Les anneaux, espaces vectoriels et modules sont généralement acceptés immédiatement, alors que les catégories divisent entre croyants et non-croyants. Je me demande pourquoi
    • L’exemple le plus proche que je connaisse est le travail sur UMAP
      Quand j’ai interviewé Leland McInnes, il m’a expliqué en détail que la théorie des catégories avait joué un grand rôle pour relier de nombreux points, même si elle n’était pas strictement nécessaire dans le code réel du résultat final
      Vu l’ampleur de l’amélioration relative par rapport à l’état de l’art précédent, t-SNE, c’est le seul exemple qui m’ait fait reconsidérer mes critiques sur la manière dont on parle de théorie des catégories en logiciel
      https://arxiv.org/abs/1802.03426
    • C’est un peu comme demander : « Y a-t-il des retours d’expérience de réussite où l’on est allé en voiture à un endroit où l’on ne pouvait pas aller à pied ? »
      La théorie des catégories est à la fois un langage et un outil, donc tout ce qu’on peut dire dans le langage de la théorie des catégories peut aussi être dit dans d’autres langages
      Comme avec une voiture, une fois qu’on a appris à conduire — et la courbe d’apprentissage est ici très raide — on peut aller plus vite. En principe, il n’y a rien qu’on ne puisse atteindre à pied sans mentionner explicitement les concepts de théorie des catégories
    • Quand on reformule ce qu’on a déjà compris dans un cadre plus général, on voit mieux ce que cela signifie réellement et on sépare l’essentiel des détails sales
      D’après ma compréhension très limitée, une partie importante de la théorie des catégories consiste à caractériser les objets par des propriétés universelles
      Une autre utilité pratique de la théorie des catégories est qu’elle fournit un langage commun pour les informaticiens, mathématiciens et physiciens. Si tout le monde parle des mêmes motifs avec des noms différents et des définitions légèrement incompatibles, collaborer n’est pas simple
    • Au Topos Institute, nous développons un nouveau logiciel qui, je l’espère, sera bien plus transparent pour les personnes qui n’ont pas encore bu le Kool-Aid de la théorie des catégories
      La pré-alpha actuelle est surtout destinée à la modélisation de systèmes dynamiques, mais je pense que la portée du travail visé exige des fondations catégoriques. Je serais heureux d’entendre l’avis de quiconque
      https://topos.site/blog/2024-10-02-introducing-catcolab/

  • Je pense que la théorie des catégories est utile, mais pas encore vraiment en informatique
    Sans besoin réel, cela ne peut que sembler difficile. Faut-il vraiment comprendre les propriétés universelles, les foncteurs adjoints et le lemme de Yoneda ? Si ce n’est pas nécessaire, on peine forcément à apprendre ce que c’est
    Fait intéressant, l’expérience en programmation fonctionnelle aide à comprendre la théorie des catégories, mais l’inverse beaucoup moins. Par exemple, le polymorphisme paramétrique donne une intuition des transformations naturelles, et les transformations naturelles sont au cœur de toutes les applications de la théorie des catégories
    Les applications convaincantes de la théorie des catégories sont très mathématiques. On les trouve en topologie algébrique, en théorie des représentations, en géométrie algébrique et en logique non classique

  • Il y a une erreur
    « Le modus ponens est une proposition composée de deux autres propositions, ici notées A et B ; si la proposition A est vraie et que la proposition A --> B est également vraie, c’est-à-dire si A implique B, alors B est aussi vraie. Par exemple, si l’on sait que “Socrate est un homme” et que “les hommes sont mortels”, alors on sait aussi que “Socrate est mortel”. »
    Cet exemple n’est pas un cas de modus ponens, qui est une règle de la logique propositionnelle, mais un syllogisme catégorique qui nécessite la logique des prédicats

  • Ici, on dit que « la logique est la science du possible », mais ne devrait-elle pas être la science du déterminé ?
    Le point essentiel, à mon avis, est de pouvoir dire de manière déterminée ce qui est valide ou non

  • La notation diagrammatique est intéressante
    L’auteur présente-t-il aussi des règles d’inférence pour des transformations préservant la vérité des diagrammes ?