David Madore's WebLog: De la force de Coq et d'autres systèmes, et de l'utilité de mettre les résultats mathématiques en contexte

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]

↓Entry #2209 [older| permalink|newer] / ↓Entrée #2209 [précédente| permalien|suivante] ↓

(mardi)

De la force de Coq et d'autres systèmes, et de l'utilité de mettre les résultats mathématiques en contexte

À cause de la combinaison entre l'écriture de l'entrée précédente et de mon interaction avec des (enfin, surtout un) mathématicien constructiviste à la Bishop/Richman, j'ai tenté de me faire une idée sur la force logique des systèmes admis par les constructivistes. (L'idée est que — pour une raison qu'on ne comprend pas vraiment, mais que je suis tenté de prendre pour un indice empirique de l'existence platonique des entiers — toutes les théories logiques introduites « naturellement » en mathématiques semblent s'arranger selon une échelle totalement ordonnée de « force » convenablement définie. Je voulais savoir où, sur cette échelle, se situent les différents cadres des mathématiques constructives. On m'a recommandé de lire le texte introductif de Martin-Löf The Hilbert-Brouwer controversy resolved? — mais au final il me suggère plus de questions qu'il n'en clôt.) Mauvaise idée : je me suis retrouvé dans un labyrinthe de petits énoncés tordus, tous semblables — et surtout, de gens qui ne communiquent pas assez entre eux, et qui ne présentent pas leurs résultats dans le contexte des autres résultats du même genre.

Certes, le problème n'est pas évident, pour plusieurs raisons :

  • D'abord, ce n'est pas évident de définir ce qu'on appelle la force logique d'un système (j'agite pas mal les mains en parlant de ça). Il n'est pas du tout vrai que deux théories logiques naturelles T et T′ soient toujours comparables si on considère toutes leurs conséquences (i.e., il n'est pas vrai que soit toute conséquence de T découle aussi de T′ soit le contraire ; par exemple, la théorie des ensembles de Zermelo avec l'axiome du choix, ZC, est incomparable avec la théorie des ensembles de Zermelo-Fraenkel sans l'axiome du choix, ZF). Il faut pour cela se limiter au moins aux énoncés arithmétiques, sans doute même aux énoncés arithmétiques Π₂ (c'est-à-dire du type <telle> machine de Turing termine pour toute entrée) ou Π₁ (c'est-à-dire du type <telle> machine de Turing ne termine jamais), ou peut-être utiliser la relation une théorie très faible montre que si un énoncé Σ₁ (c'est-à-dire du type <telle> machine de Turing termine sur telle entrée) est démontré par T alors il l'est par T, voire une théorie très faible montre que si T est inconsistante alors T′ l'est, et si possible en explicitant un lien algorithmique entre une preuve effectuée dans T et une preuve dans T′. Je n'ai pas les idées totalement claires sur les rapports entre tous ces concepts (premier labyrinthe !), et même si je crois qu'au moins dans les cas qui m'intéressent cela ne fait aucune différence, je n'en suis pas totalement sûr. Premier reproche : les gens qui énoncent des comparaisons entre théories ne sont pas toujours très clairs sur ce qu'ils veulent dire, et en tout cas ne font pas du tout l'effort de remettre en contexte ce qu'on peut dire sur ces différentes relations. (À toutes fins utiles, je note quand même que le texte le plus clair que j'aie trouvé qui explique un peu comment les choses s'articulent est l'article introductif The Realm of Ordinal Analysis de Michael Rathjen — cf. notamment les définitions 2.4, 2.14, 2.15 et la remarque 2.16.)
  • De même, système admis par les constructivistes n'est pas bien défini, à part le fait qu'il doit s'agir de logique intuitionniste. En tout cas, moi, je ne comprends pas bien ce qui fait qu'on considère que tel ou tel postulat est constructif ou pas. (Comme je le mentionne ci-dessous, je crois comprendre de façon détournée que l'ensemble des parties d'un singleton existe ne peut pas être constructif, mais j'ai un peu du mal à voir ce qu'il y a de non constructif à l'ensemble des parties d'un singleton, ou en tout cas au simple postulat de son existence !) Ce qui est sûr, c'est qu'il y a un autre labyrinthe ici, de théories logiques, de systèmes de typage et de systèmes de preuves, etc., et que je suis loin d'avoir une idée clair du rapport entre toutes ces choses. L'article de Barendregt Introduction to generalized type systems (où il introduit le fameux λ-cube, et un cube analogue de théories logiques), par exemple, est très bon pour se faire une idée rapide de ce qu'est un système de typage, mais on reste ignorant du rapport précis entre ces systèmes de typage et les théories des types introduites par Martin-Löf. Un des problèmes est probablement que les informaticiens théoriciens et les matheux ne se parlent pas suffisamment, et disent des choses semblables dans des langages différents, ce qui fait qu'il est difficile de relier ce que disent les uns et ce que disent les autres.
  • L'ajout d'un axiome en apparence innocent peut changer complètement la force d'un système. (Parfois il peut même le rendre inconsistant : voir le paradoxe de Girard, expliqué par exemple ici, qui est une sorte de version du paradoxe de Burali-Forti en théorie des types. Pour le résoudre, on a tendance à introduire des notions d'univers, typiquement une suite infinie d'univers emboîtés, un peu comme Grothendieck l'a fait pour se débarrasser de difficultés en théorie des catégories, et ce genre de postulat n'est évidemment pas innocent du point de vue de la force logique.) Ainsi, l'axiome du tiers exclu (qui change la logique intuitionniste en logique classique) ne se contente pas de briser le constructivisme, il peut aussi augmenter considérablement la force logique d'une théorie — j'ai mis longtemps à le comprendre, surtout que superficiellement ceci semble contradictoire avec la traduction de Dragalin-Friedman. C'est le cas notamment de la théorie CZF, ou ZF constructif (décrite en détails dans ces notes sur CZF par Aczel et Rathjen), une des théories standard pour les maths constructives : toute seule, elle a la même force arithmétique Π₂ qu'une théorie classique assez faible, KP (je n'ai d'ailleurs pas de bonne référence pour ce fait, mais voir page 24 du texte de Rathjen que j'ai déjà cité), alors que quand on ajoute l'axiome du tiers exclu elle devient équivalente à ZF, qui est très forte (voir la proposition 7.5 des notes d'Aczel et Rathjen citées ci-dessus). De façon encore plus surprenante, l'axiome l'ensemble des parties d'un singleton existe (i.e., la classe des sous-ensembles de {∅} est un ensemble) change considérablement la force arithmétique de CZF (voir la preuve de 7.3(ii) dans le texte d'Aczel et Rathjen et le paragraphe ci-dessous). Et je crois comprendre que pour des théories des types (comme le calcul des constructions) c'est le cas de l'axiome d'irrelevance des preuves, ou de l'axiome du choix (alors que par rapport à ZF classique, l'axiome du choix apporte une force logique nulle : par un argument de Gödel, tout énoncé aritmétique prouvable dans ZFC l'est en fait dans ZF).

Une des choses que j'aimerais comprendre, par exemple, c'est quelle est la force logique du calcul des constructions inductives (une extension du calcul des constructions qui se situe au coin le plus complexe du cube de Barendregt mentionné ci-dessus) et du système Coq qui se base dessus. Et aussi de savoir si on doit le considérer comme « constructif ». (La réponse à ces deux questions dépendra sans doute, et de façon subtile, de ce qu'on met dedans : il est certain que l'ajout du tiers exclu augmente énormément la force logique, par exemple, mais j'ai les idées beaucoup moins claires sur l'introduction du type Prop « imprédicatif » ou de l'irrelevance des preuves.) J'ai toutes sortes de réponses partielles à ces questions, mais surtout un grand mal à les relier les unes aux autres, de nouveau, parce que les gens qui ont écrit ces réponses ne se citent pas les uns les autres pour expliquer le lien entre ce qu'ils disent. Pour commencer, j'apprends dans un vieil article de B. Werner intitulé Sets in Types, Types in Sets que Coq avec ω univers est (co-interprétable, donc) équiconsistant avec ZFC avec ω univers (de Grothendieck, i.e., cardinaux inaccessibles) — sauf qu'en fait, en lisant bien, on voit que c'est après ajout de l'axiome du tiers exclu (et peut-être un autre axiome bizarre), donc ça ne m'apprend qu'une borne supérieure (très faible) sur la force de Coq sans le tiers exclu. Un article de Rathjen intitulé Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions (publié dans un volume en l'honneur de Martin-Löf) m'apprend, si je lis bien !, qu'une certaine théorie basée sur le calcul des constructions (et/ou la théorie des types de Martin-Löf — comme je l'ai dit, je ne comprends pas bien le rapport entre elles), comportant une règle d'« irrelevance des preuves », a une force logique équivalente à la fois (1) à CZF + l'axiome d'existence de l'ensemble des parties [d'un singleton, cela suffit], (2) à la théorie classique Power-KP (essentiellement, Kripke-Platek si on ajoute la fonction « ensemble des parties » au langage), ou encore (3) à la théorie des ensembles classique de Zermelo à laquelle on ajoute un nombre d'univers égal à l'ordinal de Bachmann-Howard. La thèse d'Alexandre Miquel émet (conjecture 9.7.6) une supposition qui pourrait sembler contradictoire avec ça, mais peut-être pas parce qu'il y a toutes sortes de subtilités techniques qui diffèrent entre les théories comparées (en tout cas, les deux sont d'accord sur le fait que la force logique dépasse celle de la théorie des ensembles de Zermelo) — en revanche, je ne comprends pas si l'axiome d'irrelevance des preuves a dû être postulé pour obtenir la borne inférieure. En tout cas, il s'agit de théories assez « fortes » car elles dépassent l'arithmétique du second ordre (qualifiée de fossé infranchissable dans le texte de Martin-Löf cité tout au début). A contrario, j'ai trouvé un texte d'Aczel, On Relating Type Theories and Set Theories ainsi qu'un plus vieux texte de Rathjen, The strength of Some Martin-Löf Type Theories, qui arrivent à la conclusion que diverses théories des types entre lesquelles je m'embrouille complètement sont, pour leur part, d'une force logique très modeste (en-deçà du fossé infranchissable évoqué par Martin-Löf). La différence doit donc bien être dans l'existence de l'ensemble des parties [d'un singleton], dans le type Prop de Coq que différents auteurs qualifient d'« imprédicatif » même si j'avoue ne jamais avoir compris ce que ce mot veut dire, et/ou dans l'irrelevance des preuves.

Mais bon, trève de détails techniques (que j'avoue avoir écrits surtout pour m'en souvenir plus tard) : ce dont je veux surtout me plaindre et de la façon dont les gens ne communiquent pas assez. Par exemple, j'ai trouvé extrêmement peu d'arêtes pour la relation être cité par entre les équipes d'informaticiens qui gravitent autour de Coq (du genre, B. Werner) et les équipes de matheux qui font de la théorie ordinale de la démonstration (comme le M. Rathjen que j'ai cité plusieurs fois ci-dessus, et dont les articles répondent très souvent aux questions que je me pose en théorie de la démonstration) : pourtant, ces deux groupes de gens font de la logique parfois intuitionniste et notamment de la théorie de la démonstration ; et pourtant, il est essentiel pour bien faire comprendre ses résultats de les mettre en perspective par rapport à d'autres résultats du même genre. Ceci me rappelle cette citation de Giancarlo Rota :

A leader in the theory of pseudo-parabolic partial differential equations in quasi-convex domains will not stoop to being understood by specialists in quasi-parabolic partial differential equations in pseudo-convex domains.

— Indiscrete Thoughts (XXI. Book reviews: Professor Neanderthal's World)

Résultat, moi qui ne suis spécialiste ni des équations différentielles pseudo-paraboliques dans les domaines quasi-convexes ni des équations différentielles quasi-paraboliques dans les domaines pseudo-convexes, je dois m'arracher les cheveux à me demander quel est le rapport entre tel résultat de la première théorie et tel résultat apparemment très semblable de la seconde, sachant qu'aucun ne mentionne l'autre pour m'éclairer sur le sujet.

[Ajout : il y a différents compléments dans les commentaires, grâce aux explications gentiment fournies par Arnaud Spiwack ; la moralité est qu'en tant que mathématicien classique non habitué aux maths constructives et/ou précatives, je m'embrouille complètement sur les nuances entre ce que ces différentes théories intuitionnistes prouvent ou interprètent (quelle est la force supplémentaire apportée par l'axiome du tiers exclu, par celle de l'axiome 0≠1, auquel je n'avais pas du tout pensé, la force de leur fragment de double négation, la difficulté à montrer leur cohérence versus leur normalisation : tout ça est très confus pour moi). Mais je retiens quand même que la comparaison entre Coq et ZFC n'est pas claire en l'état actuel des choses.]

Nouvel ajout () : cette réponse par Loïc Pujet sur le site StackExchange sur les assistants de preuve fournit un excellent résumé de l'état de l'art de la force logique de différents systèmes de preuve/typage aussi bien de la famille de Martin-Löf que de celle du cube de Barendregt.

↑Entry #2209 [older| permalink|newer] / ↑Entrée #2209 [précédente| permalien|suivante] ↑

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]