À 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 relationune théorie très faible montre que si un énoncé Σ₁ (c'est-à-dire du type
, voire<telle> machine de Turing termine sur telle entrée
) est démontré par T alors il l'est par T′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 estconstructif
ou pas. (Comme je le mentionne ci-dessous, je crois comprendre de façon détournée quel'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'axiomel'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.]