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éesXML (RSS 1.0) • Recent comments / Commentaires récents

Entry #2209 [older|newer] / Entrée #2209 [précédente|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 :

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.]

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

Recent entries / Entrées récentesIndex of all entries / Index de toutes les entrées