David Madore's WebLog: (Nouvelle tentative d')introduction aux mathématiques constructives : histoire, motivations et principes

La controverse Hilbert-Brouwer

L'histoire commence au début du XXe siècle à un moment où les fondements des mathématiques commencent à se mettre en place : le monde mathématique a vu se mettre en place des approches rendant l'Analyse plus rigoureuse (Cauchy, Weierstraß, Dedekind…), l'axiomatisation de l'Arithmétique (Peano), la naissance de la théorie des ensembles (Cantor) et de l'idée que celle-ci peut servir à soutenir l'ensemble des mathématiques (Frege). Deux courants apparentés émergent en philosophie des mathématiques, le logicisme et le formalisme (voir ici pour une explication de la différence — qui ne m'intéresse pas tellement ici), qui proposent de ramener, autant que possible, la pratique mathématique à l'application de règles de déduction logique à partir d'un jeu d'axiomes (voire de pure logique dans le cas du logicisme).

Chef de file du courant formaliste, David Hilbert propose, en 1904, un programme visant à fonder les mathématiques sur une base axiomatique : au moins pour une branche donnée des mathématiques, on devrait (selon le programme de Hilbert), trouver des axiomes, formaliser ces axiomes (c'est-à-dire leur donner une forme extrêmement précise ramenant, en principe, la démonstration, à un simple jeu de manipulation de symboles), et idéalement, prouver mathématiquement que les axiomes en question permettent de démontrer ou réfuter tout énoncé syntaxiquement licite, et qu'ils ne comportent pas de contradiction. (La dernière partie de ce programme sera sérieusement mise à mal à cause des limitations posées par le théorème d'incomplétude de Gödel — voir notamment ici —, mais ce n'est pas ce qui me préoccupe ici. On dit parfois que Gödel a porté le coup de grâce au programme de Hilbert, mais il me semble, au contraire que, une fois acceptées ces limitations, le programme de Hilbert a été un grand succès et qu'il est largement admis que les mathématiques ont besoin d'axiomes et de règles de déductions claires même si, dans la pratique, les démonstrations se font généralement en langage informel.)

Hilbert accueille aussi avec enthousiasme la théorie des ensembles, qu'il qualifie de paradis créé par Cantor, parce qu'il permet de rendre précises les constructions admises en la matière, et il accepte, au passage, ses infinis de différentes tailles. (Qui font maintenant partie des mathématiques « standard », un nouveau signe de succès du programme de Hilbert.) Il s'oppose en cela au courant finitiste, dans lequel s'inscrit notamment Kronecker (selon lequel les entiers naturels ont été créés par le bon Dieu, tout le reste est l'œuvre de l'homme) et dans une moindre mesure Poincaré, qui rejettent ou regardent au moins avec soupçon les constructions infinies.

Les règles de logique admises par le programme formaliste, les règles de la logique « classique », permettent souvent de montrer qu'un certain objet mathématique existe sans pour autant exhiber cet objet. Ces raisonnements prennent typiquement une forme du style : je veux montrer qu'il existe un <machin> ; supposons au contraire que <machin> n'existe pas : dans ce cas <…diverses conséquences sont tirées…>, ce qui est une contradiction : ce n'est donc pas possible, et ceci prouve que <machin> existe. À aucun moment le <machin> n'est construit : il est simplement montré qu'il ne peut pas ne pas exister : classiquement, cela revient exactement au même qu'exister, mais cela ne permet pas d'expliciter <machin> ; on peut donc dire que la preuve n'est pas constructive.

Deux exemples significatifs de telles preuves non constructives (ou considérées à l'époque comme non constructives, parce qu'en fait, tout dépend de la manière précise dont on les formalise et/ou démontre) sont donnés par deux théorèmes mathématiques très importants et dus, justement, aux deux protagonistes de notre histoire. Il s'agit d'une part du théorème de la base de Hilbert (1888), avec comme conséquence le fait que les anneaux d'invariants polynomiaux (peu importe de quoi il s'agit) sont finiment engendrés, sans que la démonstration (au moins dans sa forme initiale) exhibe explicitement un système générateur ni ne permette de le calculer, ce qui aurait fait dire à Paul Gordan, le grand spécialiste des invariants, ce n'est pas des mathématiques, c'est de la théologie (en fait, cette phrase, comme toutes les meilleures citations, est probablement apocryphe). Et d'autre part, le théorème du point fixe de Brouwer (c. 1910), dû au topologiste Luitzen Egbertus Jan Brouwer, lequel théorème affirme que toute fonction continue d'une boule dans elle-même a un point fixe, sans que la démonstration (au moins dans sa forme initiale) exhibe un tel point fixe ni ne permette de le calculer.

Ces preuves non-constructives heurtent la conception philosophique de Brouwer, selon lequel prouver l'existence d'un objet ne doit pouvoir se faire qu'en construisant l'objet en question. Il est également en désaccord, plus généralement, avec l'idée formaliste de ramener les mathématiques — au moins en principe — à une application mécanique de règles logiques à partir d'axiomes : pour Brouwer, la créativité de la démarche du mathématicien ne peut pas se ramener à une application formelle de règles. Par ailleurs, Brouwer se rapproche de l'école finitiste par son scepticisme au sujet des constructions infinies arbitraires autorisées par la théorie des ensembles de Cantor (même si on ne peut pas vraiment dire que Brouwer soit un finitiste). Enfin, son intuition du continu, c'est-à-dire de la droite réelle, ne s'accorde pas vraiment avec la formalisation des nombres réels par Dedekind, mais je dois dire que je ne prétends pas vraiment comprendre ce que Brouwer pensait exactement des nombres réels (par opposition aux réinterprétations ultérieures de l'intuitionnisme). Bref, pour ces différentes raisons, Brouwer s'oppose à la philosophie formaliste défendue par Hilbert (ainsi qu'à sa cousine, le logicisme) et, une fois qu'il a obtenu un poste permanent en 1912, il développe ses propres idées auxquelles il donne le nom d'intuitionnisme.

Il est toujours un peu compliqué, quand comme moi on n'est pas historien des mathématiques, de se faire une idée claire des positions philosophiques de telle ou telle école : le formalisme tel qu'il était conçu par Hilbert (surtout avant la publication des théorèmes de Gödel) n'est pas le formalisme tel qu'on le comprend maintenant, et l'intuitionnisme l'est encore beaucoup moins. Donc je ne suis pas sûr de bien comprendre précisément ce que Brouwer pensait (et à la limite, ça ne m'intéresse pas tant que ça) : notamment, l'importance qu'il accordait au sujet créateur, ou même la signification de ce terme, m'échappe complètement.

Mais il est quand même clair que Brouwer a identifié sans ambiguïté la loi du tiers exclu (s'il est impossible que quelque chose n'existe pas, alors ce quelque chose existe) comme une cause importante de non-constructivisme, devant donc être rejetée. Et Hilbert, de son côté, a considéré comme incompréhensible ce refus d'utiliser le tiers exclu en mathématiques, qu'il a comparé au refus par un astronome d'utiliser un télescope ou au refus par un boxeur d'utiliser ses poings. La controverse intellectuelle entre les deux hommes s'est mêlée de considérations plus politiques (dans le contexte international tendu de l'entre-deux-guerres), et finalement personnelles, et a culminé lorsque Hilbert en 1928 a voulu forcer Brouwer à démissionner du comité éditorial du prestigieux journal Mathematische Annalen dont il était éditeur en chef (les deux autres éditeurs en chef, Einstein et Carathéodory, n'ont pas approuvé la décision et ont eux-même démissionné, laissant Hilbert seul en charge du journal).

Mathématiquement, on peut dire que c'est Hilbert qui a gagné la polémique, au moins en ce sens les mathématiques actuelles se font de nos jours, dans leur écrasante majorité, en logique classique. De plus, il est généralement admis — même si c'est un peu une déclaration de foi, rarement importante dans la pratique — qu'elles doivent se comprendre comme fonctionnant dans un système formel bien précis appelé ZFC (la théorie des ensembles de Zermelo-Fraenkel avec axiome du choix), qui est une axiomatisation de la théorie des ensembles de Cantor (le paradis dont nous ne devions pas être chassés). En tout cas il est clair que, sauf si l'auteur d'un article mathématique a préfacé celui-ci de promesses contraires, le fait d'utiliser librement la loi du tiers exclu, ou d'invoquer des ensembles infinis à la façon de Cantor, ne suscitera aucun commentaire d'un rapporteur.

Mais ce n'est pas pour autant que l'intuitionnisme ait disparu. Une quantité plus faible, mais absolument pas négligeable, de mathématiques se font de nos jours dans ou bien en étudiant des systèmes qui m'admettent pas la loi du tiers exclu comme axiome.

Cependant l'intuitionnisme lui-même n'est plus vraiment tel qu'il était imaginé par Brouwer : la question de savoir ce que devient la logique en l'absence de la loi du tiers exclu et de ce qu'elle permet de prouver a été étudiée principalement par des logiciens (comme Gödel, Kripke), et notamment par Arend Heyting, élève de Brouwer, à qui on doit d'avoir mis sur un plan clair et rigoureux les règles de l'intuitionnisme (ou du moins les règles de ce qu'on appelle maintenant l'intuitionnisme), ainsi qu'à ses propres élèves, Anne Troelstra et Dirk van Dalen. C'est ironique : l'intuitionnisme est né comme une réaction au logicisme et au formalisme, et il est largement devenu lui-même une branche de la logique formelle (sans pour autant que les idées fondatrices de Brouwer se soient perdues dans cette transformation). En tout état de cause, ce qu'on appelle maintenant logique intuitionniste est simplement celle qui s'obtient en retirant la loi du tiers exclu (d'une certaine formulation) de la logique classique.

Bishop et ses successeurs

Cependant, l'intuitionnisme tel que compris originellement par Brouwer ne se contentait pas de retirer aux mathématiques la loi du tiers exclu, produisant une logique simplement plus faible que la logique classique : il postulait aussi pour vrais des résultats de continuité qui sont contradictoires avec les mathématiques classiques (mais qui cessent de conduire à une absurdité dans le cadre de la logique intuitionniste). Le plus emblématique de ces résultats (il découle lui-même d'autres principes plus généraux) est l'affirmation que toute fonction réelle est continue, un résultat manifestement faux en mathématiques classiques (la fonction valant 0 sur les réels ≤0 et 1 sur les réels >0, par exemple, est discontinue en 0), mais qui devient logiquement possible si on affaiblit la logique (on ne peut plus affirmer que tout réel soit est >0 soit n'est pas >0), ce qui permet à Brouwer de décider de l'accepter comme vrai.

Le développement ultérieur du constructivisme est venu avec Errett Bishop, qui, en 1967, écrit un traité d'analyse constructive : il travaille sans la loi du tiers exclu (i.e., en « logique intuitionniste »), mais contrairement à Brouwer, il ne postule rien qui soit contradictoire avec les mathématiques classiques. Par conséquent, tous les énoncés contenus dans le traité de Bishop sont valables (et en général, bien connus) dans le contexte de l'analyse classique. Le point de vue est maintenant quelque chose comme le suivant : il ne s'agit pas de faire des mathématiques différentes, mais de faire des mathématiques plus fines, plus précises, en ce sens que disposer d'une preuve constructive d'un résultat apporte (souvent) plus d'informations que disposer d'une preuve classique. Par exemple, et je vais y revenir, si on dispose d'une preuve constructive du fait que pour tout x il existe y tel que <quelque chose>, la preuve devrait permettre de construire, i.e., de calculer effectivement (algorithmiquement) ce y en fonction de x (c'est du moins l'idée : le fait que ce soit bien le cas dépend crucialement de ce qu'on prend exactement comme fondations). D'autres, notamment Douglas Bridges et Fred Richman, ont étudié des versions constructives d'autres branches des mathématiques, comme l'algèbre commutative.

⚠ Dès lors, on voit que les mots mathématiques constructives ou intuitionnisme ne font pas référence à quelque chose de très précis : autant il est largement accepté que logique intuitionniste fait référence à la logique dépourvue de la loi du tiers exclu (mais déjà cela permet un certain nombre de variations comme la logique classique elle-même en permet — je ne m'étends pas à ce sujet), le mot intuitionnisme peut faire référence à différentes interprétations de l'intuitionnisme de Brouwer (donc, a priori, incompatible avec les mathématiques classiques), et le terme de mathématiques constructives peut faire référence à n'importe quelle sorte de mathématiques travaillant en logique intuitionniste (donc pas forcément incompatible avec les mathématiques classiques), mais parfois ces termes sont utilisés de façon interchangeable, et parfois constructif indique qu'on a vraiment un résultat métamathématique selon lequel une preuve de l'existence de x permet de construire un tel x. Il faut voir précisément ce que chaque auteur prend comme cadre et comme axiomes !

Un livre de Bridges et Richman propose la terminologie suivante : ils définissent quatre systèmes de mathématiques qu'ils appellent : BISH, INT, RUSS et CLASS :

• Le premier, BISH, est celui des mathématiques constructives de Bishop. Il forme le socle commun des trois autres qui s'obtiennent en ajoutant des règles ou axiomes et sont mutuellement incompatibles. C'est donc le plus faible des quatre (au sens où tout théorème de BISH est aussi un théorème dans INT, RUSS et CLASS).
• Le système CLASS est (plus ou moins) le système des mathématiques classiques. (J'écris plus ou moins parce que ce système ne doit pas admettre toutes les constructions ensemblistes de ZFC, mais ce n'est pas important ici.) Il s'obtient en ajoutant à BISH la loi du tiers exclu.
• Le système INT est l'intuitionnisme de Brouwer, ou du moins une interprétation moderne, et formelle, de celui-ci : il est obtenu en ajoutant à BISH des postulats qui sont incompatibles avec les mathématiques classiques, comme le principe du choix continu, et aussi d'autres qui ne le sont pas comme le théorème de l'éventail. (Le principe du choix continu affirme que que si P ⊆ ℕ^ℕ × ℕ vérifie la propriété que pour tout a∈ℕ^ℕ il existe n∈ℕ tel que (a,n)∈P, alors il existe f:ℕ^ℕ→ℕ continue [au sens où pour tout a∈ℕ^ℕ il existe k∈ℕ tel que f(a) ne change pas quand on remplace a par une suite ayant les mêmes k premiers termes] telle que pour tout a∈ℕ^ℕ on ait (a,f(a))∈P. C'était quelque chose que Brouwer considérait comme fondamental dans sa conception même du « continu ».) Bref, on peut penser que INT correspond à une bonne approximation de ce que Brouwer considérait comme mathématiques valables.
• Quant au système RUSS, il formalise le constructivisme de l'école russe, notamment d'Andrej Markov fils, qui vise à fournir un cadre d'étude de la calculabilité (au sens algorithmique). Ce système s'obtient en ajoutant à BISH des principes qui rendent le système incompatible avec les mathématiques classiques de CLASS mais également incompatible avec INT. (Les deux principaux axiomes de RUSS sont : le principe d'énumérabilité, selon lequel l'ensemble des fonctions partielles de ℕ vers ℕ dont le domaine de définition est dénombrable est lui-même dénombrable ; et le principe de Markov selon lequel toute suite binaire qui n'est pas constamment égale à 0 contient un 1 ; le principe d'énumérabilité contredit à la fois CLASS et INT, tandis que le principe de Markov est une trivialité dans CLASS et est suspect dans INT au sens où il n'est pas contradictoire mais il n'est pas non plus postulé ni démontrable.)

Pour séduisante que soit cette classification en quatre grands systèmes, elle est loin d'être la fin de l'histoire. Notamment, le système BISH des mathématiques à la Bishop (censé selon les auteurs de la classification être le socle commun minimal des mathématiques constructives, donc) accepte certains axiomes, comme l'axiome du choix dénombrable ou dépendant (en fait, elle les postule de façon détournée en les cachant assez insidieusement dans la logique), dont on peut pourtant vouloir se dispenser : d'autres chercheurs (tels que Fred Richman qui est pourtant un des auteurs de la classification, mais aussi Peter Schuster ou Hajime Ishihara) ont étudié les mathématiques dans des systèmes plus faibles que BISH, qui ne postulent pas d'axiome du choix, même de façon détournée ; l'intérêt est par exemple qu'on obtient ainsi des résultats valables dans tous les topoï (cf. plus bas). Et il y a d'autres façons de varier les constructions autorisées dans le cadre d'un système qui se prétend constructif (je reviendrai là-dessus à la fin de cette entrée), que ce soit en affaiblissant ou en renforçant. Néanmoins, ces quatre systèmes BISH, INT, RUSS et CLASS ont le mérite de servir de points de référence pour en comparer d'autres.

Topos, types, et tout et tout

Un autre développement qui a eu un impact sur les mathématiques constructives est l'émergence de la notion de topos, développé au début des années 1960 par Grothendieck (et ses élèves) dans le cadre de la géométrie algébrique, où il apparaît comme une forme très générale de topologie, et ultérieurement étudié aussi sous l'angle de la théorie des catégories et, ce qui m'intéresse ici, de la logique, notamment à travers les travaux d'André Joyal. Les topos (ou topoï) sont un contexte naturel pour étudier les mathématiques constructives et/ou la logique intuitionniste, parce que même si « de l'extérieur » ce sont des objets mathématiques classiques, « de l'intérieur » ils apparaissent comme des univers régis par la logique intuitionniste (c'est ce que j'essayais d'expliquer ici, tout en promettant de ne pas définir ce qu'est un topos) : donc on peut fabriquer des topoï qui modélisent tel ou tel système de mathématiques constructives (et justifier, par exemple, que Brouwer avait raison de croire que tel ou tel principe, ou conséquence comme toute fonction réelle est continue, est cohérent, i.e., possible, dans le cadre de la logique intuitionniste). Un topos qui a reçu un intérêt particulier (et que j'ai le projet de présenter Un Jour™ dans ce blog, cf. ce billet) est le topos effectif de Martin Hyland, qui justifie le constructivisme à la Markov (essentiellement RUSS dans la typologie évoquée ci-dessus) : par exemple, dans le topos effectif, toute fonction ℕ→ℕ est calculable par une machine de Turing. [Ajout : le billet sur le topos effectif est ici.]

Enfin, un autre sujet qui a trouvé des connexions fortes avec l'intuitionnisme est la théorie des types en informatique (qui ont d'ailleurs un lien avec les topoï, ou avec certaines variations autour de la notion de topos). Un système de typage est, pour parler de façon extrêmement vague, un système qui attribue aux données manipulables dans un langage de programmation une propriété appelée « type » (qui pourra être attribuée à la compilation ou à l'exécution, mais du point de vue théorique le premier cas est souvent plus intéressant) qui distingue, par exemple, un entier ou une chaîne de caractères ; mais des types plus intéressants, si le langage le permet, pourraient être, par exemple, une fonction prenant en entrée une paire d'entiers et renvoyant un entier voire une fonction prenant en entrée une donnée de type A et renvoyant une autre fonction prenant une entrée de type B et renvoyant une donnée de type A (qu'on pourrait noter A→(B→A)). La correspondance de Curry-Howard est un principe général (dont il existe diverses formalisations précises), selon lequel il existe une analogie profonde entre certains systèmes de typage informatiques et certains systèmes logiques en mathématiques : grosso modo, cette correspondance associe les types côté informatique avec les énoncés côté mathématique (par exemple, le type A→(B→A), je prends un A et je renvoie une fonction prenant un B et renvoyant un A pourrait correspondre à l'affirmation logique A⇒(B⇒A), si A est vrai alors B implique A), et elle associe les données de ces types côté informatique avec les preuves de ces énoncés côté mathématique. La correspondance de Curry-Howard peut fonctionner en logique classique comme en logique intuitionniste : grosso modo, l'axiome ((P⇒Q)⇒P)⇒P, ou loi de Peirce, qui peut servir (aussi bien que le tiers exclu) à différencier la logique classique de la logique intuitionniste, correspond, via Curry-Howard, à une fonction très importante de certains langages de programmation, le call/cc (dont le type est ((P→Q)→P)→P), j'ai d'ailleurs écrit une très vieille page à son sujet ; mais comme la plupart des langages de programmation n'ont pas de call/cc (ou même s'ils en ont un, il est ajouté pour ainsi dire « après coup » et pas comme un élément essentiel du typage), la logique intuitionniste se présente comme plus naturelle ici.

La correspondance de Curry-Howard est tellement fortement ancrée dans certains systèmes de typage qu'il n'est plus vraiment possible de dire s'il s'agit de systèmes de typage informatiques ou de systèmes logiques, ni même si la distinction a un sens : on peut évoquer par exemple les systèmes du λ-cube de Henk Barendregt tels que le système F de Girard ou le calcul des constructions ; ou encore, les systèmes (dans un esprit assez différent) développés par Per Martin-Löf qui avait notamment en tête, je crois comprendre, de formaliser plus précisément les mathématiques à la Bishop. (Le fil Twitter qui passe par ici est d'ailleurs fort intéressant.)

Toujours est-il que ces systèmes de typage/preuve (qui fondent divers programmes, comme Coq, utilisés aussi bien pour la certification de programmes que la certification de preuves mathématiques) s'inscrivent naturellement en logique intuitionniste : s'ils sont capables de fonctionner en logique classique, c'est par addition parfois un peu ad hoc de la loi du tiers exclu.

De fait, je pense qu'une partie importante de la recherche en mathématiques constructives se fait maintenant soit dans l'idée de liens avec l'informatique, soit au moins avec un regard vers l'informatique. Bien sûr, ça ne concerne pas uniquement le système de typage : le fait qu'une preuve dans certains systèmes constructifs du fait que pour tout x il existe y tel que <blabla> permette d'extraire un algorithme renvoyant y en fonction de x, justifie aussi l'intérêt informatique porté aux mathématiques constructives (de toute façon, ces deux raisons sont très liées l'une à l'autre).

Un peu de logique

Commençons par la logique. Je ne veux pas la formaliser complètement, surtout que je prétends m'adresser à des gens qui ne sont pas logiciens (j'ai donné une description un peu plus formelle dans cette partie de cette entrée passée), mais voici les règles de base de manipulation des connecteurs et quantificateurs logiques, règles dont j'insiste qu'elles sont les mêmes que pour (une certaine présentation de) logique classique si ce n'est qu'on ne dispose pas de la loi du tiers exclu, mais fortement inspirées de l'interprétation de Brouwer-Heyting-Kolmogorov :

• pour conclure P∧Q, je peux prouver les deux ; pour utiliser P∧Q, je peux utiliser P ou utiliser Q (comme il me plaira) ;
• pour conclure P∨Q, je peux prouver l'un des deux ; pour utiliser P∨Q, je peux traiter deux cas, c'est-à-dire être prêt à utiliser l'un quelconque des deux (sans que je choisisse lequel) ;
• pour conclure P⇒Q, je peux temporairement supposer P, raisonner comme si je disposais de P, et prouver Q ce qui, une fois levée l'hypothèse, me permettra de conclure P⇒Q ; pour utiliser P⇒Q, je peux l'appliquer à P pour obtenir Q ;
• pour conclure ⊤, je n'ai rien à faire ; et utiliser ⊤ ne permet de rien faire d'utile ;
• je ne dispose pas de règle pour conclure ⊥ ; et utiliser ⊥ permet(trait) de faire n'importe quoi ;
• pour conclure ∀x.P(x), je peux temporairement supposer donné un x (sur lequel je ne suis pas en droit de faire d'hypothèse), et prouver P(x) ce qui, une fois abstraite la variable, me permettra de conclure ∀x.P(x) ; pour utiliser ∀x.P(x), je peux l'appliquer à un t quelconque pour obtenir P(t) ;
• pour conclure ∃x.P(x), je peux donner un t et prouver P(t) (pour ce t) ; pour utiliser ∃x.P(x), je peux utiliser P(y) où y est une nouvelle variable (sur laquelle je ne suis pas en droit de faire d'hypothèse) [là normalement je voudrais renvoyer vers un bout de cette discussion Twitter, mais peut-être que c'est un peu technique à ce stade] ;
• on traite ¬P (la négation de P) comme un simple raccourci de langage signifiant P⇒⊥.

(Le mot peut est utilisé à chaque fois parce que rien ne dit qu'il n'y a pas d'autres techniques pour arriver à ceci ou cela : par exemple, ils pourraient être des axiomes.)

Le dernier point énuméré signifie que prouver ¬P, je peux temporairement supposer P et arriver à une absurdité, ce qui, une fois levée l'hypothèse, permet de conclure ¬P : ce type de raisonnement « par l'absurde » est autorisé puisqu'il s'agit justement de prouver ¬P qui dit très exactement P est absurde (peut-être une meilleure lecture dans le contexte intuitionniste que P est faux). En revanche, le type de raisonnement « par l'absurde » qui n'est pas permis, c'est de supposer ¬P d'arriver à une absurdité, et d'espérer en conclure P : si ¬P conduit à une absurdité, c'est qu'on a montré ¬¬P (qu'on peut peut-être imaginer comme signifiant intuitivement P est plausible), pas P. On a P ⇒ ¬¬P (démonstration : pour démontrer P ⇒ ¬¬P, je suppose P et je cherche à démontrer ¬¬P sous cette hypothèse ; pour démontrer ¬¬P, c'est-à-dire (¬P)⇒⊥, je suppose ¬P et je cherche à démontrer ⊥ (c'est-à-dire une absurdité) sous cette hypothèse ; mais à ce stade, j'ai supposé à la fois P et ¬P, c'est-à-dire P⇒⊥, et j'ai donc ⊥, l'absurdité recherchée) ; en revanche, la réciproque n'est pas valable en général (il n'est pas difficile de voir que supposer ¬¬P ⇒ P pour tout P implique la loi du tiers exclu Q∨¬Q [indication : supposer ¬(Q∨¬Q) donne une absurdité] ; mais pour voir qu'elle n'est effectivement pas démontrable, il faudrait construire des modèles, ce que je ne veux pas faire ici).

Je ne veux pas trop m'étendre sur la logique, mais signalons quand même quelques points qu'on rencontre souvent, en commençant par la distributivité des connecteurs logiques. Il reste valable en logique intuitionniste que ∧ est distributif sur ∨, c'est-à-dire que P∧(Q∨R) équivaut à (P∧Q)∨(P∧R). (Voici la démonstration en détails : dans le sens P∧(Q∨R) ⇒ (P∧Q)∨(P∧R) : en supposant P∧(Q∨R), j'ai d'une part P et d'autre part Q∨R ; je traite deux cas : soit j'ai Q, soit j'ai R : dans le premier cas j'ai P et Q, c'est-à-dire P∧Q, et de même dans le second j'ai P∧R, donc dans les deux cas j'ai bien (P∧Q)∨(P∧R) ; pour le sens réciproque (P∧Q)∨(P∧R) ⇒ P∧(Q∨R), supposons (P∧Q)∨(P∧R) et traitons deux cas : si j'ai P∧Q, j'ai d'une part P et d'autre part Q donc Q∨R, et dans l'autre cas de même j'ai P et Q∨R.) Dans l'autre sens, si on tente de distribuer ∨ sur ∧ (ce qui est légitime en logique classique), on peut encore affirmer en logique intuitionniste que P∨(Q∧R) implique (P∨Q)∧(P∨R) (démonstration : en supposant P∨(Q∧R), je traite deux cas, soit j'ai P soit j'ai Q∧R, dans le premier cas j'ai bien P∨Q puisque j'ai P et j'ai aussi P∨R pour la même raison, et dans le second cas, j'ai à la fois Q et R, donc j'ai bien P∨Q puisque j'ai Q et j'ai aussi P∨R puisque j'ai R) ; mais cette fois, la réciproque n'est plus valable en général : en logique intuitionniste, P∨(Q∧R) peut être strictement plus fort que (P∨Q)∧(P∨R) la réciproque est également valable (chacun de ‘∧’ et ‘∨’ est distributif sur l'autre) [correction (2022-11-24) : voir l'ajout ci-dessous pour des précisions].

(Ceci suggère, d'ailleurs, que la distributivité de ∧ sur ∨ est un phénomène plus naturel, ou plus fondamental, que celle de ∨ sur ∧, même si la logique classique les présente comme rigoureusement symétriques. Et peut-être même qu'il est plus intuitif de voir que je vais sortir et manger soit un sandwich soit une glace est complètement identique à je vais soit sortir et manger un sandwich soit sortir et manger une glace que de se dire que je vais soit sortir soit manger une glace et un sandwich l'est à d'une part je vais soit sortir soit manger une glace, et d'autre part je vais soit sortir soit manger un sandwich. Quoi qu'il en soit, ceci peut être un argument pour considérer que, comme on le fait habituellement, le connecteur ∧ a une priorité plus forte que le connecteur ∨ quand on omet les parenthèses.)

Ajout / correction / digression (2022-11-24) : J'avais initialement écrit ci-dessus que si ‘∧’ est distributif sur ‘∨’ comme en logique classique, on a que P∨(Q∧R) implique (P∨Q)∧(P∨R) mais pas forcément la réciproque. En fait, la distributivité de ‘∨’ sur ‘∧’ marche bien dans les deux sens : le plus simple pour le voir est d'utiliser la distributivité de ‘∧’ sur ‘∨’ pour réécrire (P∨Q)∧(P∨R) comme P ∨ (P∧R) ∨ (Q∧P) ∨ (Q∧R), et les deux termes du milieu sont de toute façon plus grands que P (i.e., ils l'impliquent) donc ceci est équivalent à P∨(Q∧R). Pourquoi ai-je fait cette erreur, alors ? Je peux donner deux raisons (et ainsi justifier pourquoi je pense quand même que la distributivité de ‘∨’ sur ‘∧’ est une sorte d'accident alors que celle de ‘∧’ sur ‘∨’ est fondamentale). La première c'est qu'avec les quantificateurs on a bien équivalence dans un cas, celle de P∧∃x.(Q(x)) avec ∃x.(P∧Q(x)) alors que, dans l'autre sens P∨∀x.(Q(x)) implique mais peut être strictement plus fort que ∀x.(P∨Q(x)) (classiquement les deux sont équivalents). La deuxième est que, dans un sens que je ne veux pas définir, P∨(Q∧R) et (P∨Q)∧(P∨R) doivent sans doute être considérés comme logiquement équivalents mais pas isomorphes, c'est-à-dire en gros qu'on a des implications dans les deux sens, mais si on commençait à regarder l'identité des preuves, la composée des deux preuves (P∨Q)∧(P∨R) ⊢ P∨(Q∧R) et P∨(Q∧R) ⊢ (P∨Q)∧(P∨R) ne va pas donner la « preuve identité » ; ceci n'a aucune importance dans le cadre où je me suis placé (l'identité des preuves n'est ni définie ni retenue), mais cela peut en avoir dans d'autres contextes, par exemple si on imagine que P,Q,R sont des ensembles ou des types informatiques, manifestement P⊎(Q×R) et (P⊎Q)×(P⊎R) ne sont pas identifiables alors que P×(Q⊎R) et (P×Q)⊎(P×R) le sont. Donc je maintiens quand même le paragraphe précédent que la distributivité de ‘∧’ sur ‘∨’ est plus naturelle que celle de ‘∨’ sur ‘∧’, mais mon explication était erronée — en logique intuitionniste comme en logique classique les deux distributivité (finies !) valent. (Merci à Florent Pompigne d'avoir attiré mon attention sur ce problème.)

Signalons de même que (P∨Q)⇒R équivaut à (P⇒R)∧(Q⇒R), et que P⇒(Q∧R) équivaut à (P⇒Q)∧(P⇒R), mais qu'en revanche (P∧Q)⇒R est potentiellement plus faible que (P⇒R)∨(Q⇒R) et que P⇒(Q∨R) est aussi potentiellement plus faible que (P⇒Q)∨(P⇒R). (Les démonstrations des implications valables devraient être un bon exercice, ainsi que la vérification du fait que les règles proposées ne permettent au moins pas de façon évidente d'obtenir celles qui ne sont pas valables. Là aussi, je pense que les implications qui sont les plus intuitivement claires sont celles qui sont valables en logique intuitionniste, donc elle n'a pas complètement usurpé son nom !) Comme cas particulier de ce que je viens de dire, ¬(P∨Q) est la même chose que (¬P)∧(¬Q), mais ¬(P∧Q) est potentiellement plus faible que (¬P)∨(¬Q). Il peut aussi être bon de noter que ¬¬(P∧Q) équivaut à (¬¬P)∧(¬¬Q) et ¬¬(P⇒Q) équivaut à (¬¬P)⇒(¬¬Q) (je laisse ça en exercice).

On a quelque chose d'analogue pour les quantificateurs : (∃x.P(x))⇒R équivaut (à condition que R ne fasse pas intervenir x du tout) à ∀x.(P(x)⇒R), et P⇒(∀x.R(x)) à ∀x.(P⇒R(x)) ; en revanche, (∀x.P(x))⇒R est potentiellement plus faible que ∃x.(P(x)⇒R), et P⇒(∃x.R(x)) que ∃x.(P⇒R(x)). Le cas le plus important à retenir est que ¬∃x.P(x) équivaut à ∀x.¬P(x) mais que ¬∀x.P(x) est potentiellement plus faible que ∃x.¬P(x). On peut noter que ¬¬∀x.P(x) implique ∀x.¬¬P(x) (mais la réciproque ne vaut pas en général).

Ajout (2022-11-24) : J'avais oublié de mentionner le fait que P∧∃x.(Q(x)) est équivalent à ∃x.(P∧Q(x)) alors que, dans l'autre sens P∨∀x.(Q(x)) implique mais peut être strictement plus fort que ∀x.(P∨Q(x)) (classiquement les deux sont équivalents)

Le fait que ¬∃x.P(x) équivaille à ∀x.¬P(x) même en logique intuitionniste permet d'utiliser une tournure de phrase telle que aucun x ne vérifie P(x) (ou P(x) n'est jamais vérifié) sans qu'on ait à s'inquiéter de savoir laquelle des deux elle désigne.

Une chose qui mérite d'être signalée, c'est que même si on s'en tient au pur calcul propositionnel (i.e., sans quantificateurs), la logique intuitionniste est déjà subtile et substantiellement différente de la logique classique. En logique classique, une formule propositionnelle de r variables (c'est-à-dire obtenue en connectant comme on veut des variables propositionnelles X₁,…,X_r par les connecteurs ∧,∨,⇒,⊤,⊥,¬) est complètement classifiée, à équivalence démontrable près, par son tableau de vérité, c'est-à-dire la valeur de vérité de la formule pour chacune des 2^r combinaisons de valeurs de vérité des variables, et il y a donc 2^2r formules différentes à équivalence près, et décider si une formule est démontrable peut se faire en testant chacune des 2^r possibilités. En logique intuitionniste, les choses sont bien différentes : rien qu'avec une variable, il y a une infinité de formules inéquivalentes, et les analogues avec plusieurs variables (algèbre de Heyting complètes libres sur r variables) sont essentiellement impossibles à décrire. On peut certes décider algorithmiquement si une pure formule propositionnelle est démontrable, mais c'est algorithmiquement plus délicat que pour le cas classique (on peut, par exemple, énumérer tous les arbres de dérivation en calcul des séquents sans coupure, ou tous les modèles de Kripke de taille assez petite ; voir ici pour des détails).

Toujours en pur calcul propositionnel, une différence avec la logique classique est l'existence de logiques intermédiaires obtenues en ajoutant des schémas d'axiomes à la logique propositionnelle, c'est-à-dire tous les axiomes de la forme ψ(X₁,…,X_r) où ψ est une certaine formule propositionnelle dans les variables X₁,…,X_r. En logique classique on ne peut rien ajouter de la sorte, car soit ψ est vraie pour toute valeur de vérité de X₁,…,X_r, et elle est démontrable (donc l'axiome n'ajoute rien), soit il existe une combinaison de valeurs de vérité de X₁,…,X_r telle que ψ(X₁,…,X_r) n'est pas vraie, et alors l'axiome conduira à une incohérence. Mais en logique intuitionniste on peut ajouter de tels schémas d'axiomes. Si on ajoute le schéma d'axiomes X∨¬X (loi du tiers exclu) ou (¬¬X)⇒X (élimination des doubles négations), on obtient la logique classique (noter que (¬¬X)⇒X, pour un X précis, est en général plus faible que X∨¬X, mais supposer que (¬¬X)⇒X vaut pour tout X permet de conclure X∨¬X pour tout X), ou de même ((X⇒Y)⇒X)⇒X (loi de Peirce). En revanche, il existe toutes sortes de schémas d'axiomes conduisant à une logique strictement intermédiaire entre la logique classique et la logique intuitionniste, par exemple : ¬X∨¬¬X (loi faible du tiers exclu) ou bien (X⇒Y) ∨ (Y⇒X) (axiome de Dummett), ou encore (((¬¬X)⇒X) ⇒ (X∨¬X)) ⇒ ((¬¬X)∨¬X) (axiome de Scott), ou encore (¬X⇒(Y₁∨Y₂)) ⇒ ((¬X⇒Y₁) ∨ (¬X⇒Y₂)) (axiome de Kreisel-Putnam) : ces formules ne sont pas démontrables en logique intuitionniste pure (elles le sont en logique classique), mais les postuler ne conduit pas non plus à la logique classique. (Les logiques propositionnelles intermédiaires axiomatisées par le schéma de Scott ou celui de Kreisel-Putnam, comme le calcul propositionnel intuitionniste pur, ont la propriété de la disjonction, c'est-à-dire que si U∨V y est démontrable, alors l'un de U ou de V est démontrable. Ceci est très loin d'être évident, et on ne connaît pas de technique générale pour prouver ce genre de choses.)

Un (tout petit) peu d'arithmétique

Bon, assez de pure logique, on voudrait faire des mathématiques un peu plus substantielles.

La première chose qu'on peut tenter de faire en maths constructives, c'est de l'arithmétique. Prenons par exemple les axiomes de Peano : ils décrivent un type d'objet appelés entiers naturels avec une instance particulière, 0 (zéro), une fonction S (successeur) prenant un entier naturel et renvoyant un entier naturel, et deux fonctions + et × (voire ↑) prenant deux entiers naturels et renvoyant des entiers naturels ; avec les axiomes suivants :

• ∀n.¬(Sn=0) (Sn n'est jamais égal à 0)
• ∀p.∀q.((Sp=Sq)⇒(p=q)) (deux entiers naturels ayant le même successeur sont égaux)
• (P(0) ∧ ∀n.(P(n)⇒P(Sn))) ⇒ ∀n.P(n) (principe de récurrence : si une propriété est vraie en 0 et vraie du successeur de tout entier naturel où elle est vraie, alors cette propriété est vraie en tout entier naturel) — cette affirmation étant soit quantifiée universellement sur P, si la logique le permet, soit énoncée comme un schéma d'axiomes pour toute formule logique P ayant une variable libre n.
• ∀m.(m+0=m)
• ∀m.∀n.(m+Sn=S(m+n))
• ∀m.(m×0=0)
• ∀m.∀n.(m×Sn=(m×n)+m)
• ∀m.(m↑0=1) (où 1 := S0)
• ∀m.∀n.(m↑Sn=(m↑n)×m)

Il faut aussi mettre quelque part les axiomes de l'égalité (qui sont tantôt classés dans la logique tantôt à part) :

• ∀m.(m=m) (réflexivité)
• ∀m.∀n.((m=n)⇒(n=m)) (symétrie — on doit pouvoir s'en passer)
• ∀m.∀n.((m=n)⇒(P(m)⇒P(n))) (extensionnalité des prédicats : si m et n sont égaux alors toute propriété de l'un vaut pour l'autre ; la transitivité en découle facilement) — avec la même remarque sur P que dans le principe de récurrence ci-dessus.

Énoncés en logique classique, ces axiomes donnent l'arithmétique de Peano ; énoncés en logique intuitionniste, ils donnent l'arithmétique de Heyting.

(Il y a aussi des subtilités sur ce que la logique permet d'exprimer : en logique du premier ordre on ne peut véritablement manipuler que les entiers naturels, et en tout cas on ne peut quantifier que sur eux, si bien que les affirmations faites sur toute propriété P ci-dessus, c'est-à-dire la récurrence et l'extensionnalité des prédicats, doivent être approchées en les énonçant pour toute formule qu'on peut écrire : on définit ainsi l'arithmétique de Peano du premier ordre et l'arithmétique de Heyting du premier ordre ; en logique du second ordre on peut aussi quantifier sur les propriétés, mais il faut alors ajouter un schéma de compréhension du type ∃P.∀n.(P(n)⇔φ(n)) où φ(n) parcourt toutes les formules du second ordre, ou bien un autre mécanisme pour fabriquer des propriétés, et on obtient l'arithmétique de Peano ou de Heyting du second ordre : je ne m'étends pas plus, parce qu'il n'y a rien ici de spécifique à l'intuitionnisme, ce sont des subtilités logiques certes importantes mais orthogonales à dont je veux parler.)

Mais l'arithmétique de Heyting (intuitionniste, donc) ne déroutera guère la personne habituée à l'arithmétique de Peano classique : les résultats classiques comme la commutativité de l'addition ou de la multiplication, la distributivité de la multiplication sur l'addition, la division euclidienne, le fait que 2+2=4 ou 6×7=42, ce genre de choses, ou même l'existence et l'unicité de la décomposition en facteurs premiers (qu'il faut prendre le soin de coder dans le langage de l'arithmétique du premier ordre si on veut ça, ce n'est pas évident mais ça n'a aucun rapport avec ce dont je parle ici), marchent exactement pareil en arithmétique de Heyting qu'en arithmétique de Peano.

En fait, pour aller trouver un énoncé qui soit démontrable dans l'arithmétique de Peano et pas dans l'arithmétique de Heyting, il faut se gratter un peu la tête. Un tel exemple est toute machine de Turing soit termine en temps fini soit ne termine pas en temps fini (ce qui est une tautologie en logique classique mais n'est pas démontrable dans l'arithmétique de Heyting, je l'avais démontré ici [chercher problème de l'arrêt]), une fois qu'on a encodé la notion de machine de Turing dans l'arithmétique (ce qui ne pose pas plus de difficulté intuitionniste que classique tant qu'on reste à niveau fini) ; ou encore l'arithmétique de Peano est cohérente ou bien elle ne l'est pas (idem, il faut faire appel à un codage de Gödel ; on peut noter que la cohérence de l'arithmétique de Peano est équivalente à celle de Heyting, cela découle d'une traduction de type Gödel-Gentzen, cf. ici, cette équivalence étant elle-même démontrable dans l'arithmétique de Heyting).

En particulier, je prends la peine de souligner, parce que ce n'est pas forcément évident quand on débute la logique intuitionniste et qu'on ne sait pas ce qu'on a le droit de dire ou pas, que :

Tout entier naturel est ou bien nul ou bien non nul (∀m.((m=0)∨¬(m=0))).

Plus généralement, deux entiers naturels ou bien sont égaux ou bien ne sont pas égaux (∀m.∀n.((m=n)∨¬(m=n))).

(La démonstration, disons de la première affirmation, ∀m.((m=0)∨¬(m=0)), est simplement par récurrence sur m : pour m=0 on a (m=0)∨¬(m=0) car le premier est vrai, et si (m=0)∨¬(m=0) alors on a (Sm=0)∨¬(Sm=0) car le second est vrai en vertu des axiomes (l'hypothèse de récurrence ne sert même pas).)

On dit que l'égalité sur les entiers naturels est décidable (notamment, elle est stable, c'est-à-dire que ¬¬(m=n) implique m=n). On peut donc sans hésitation écrire m≠n pour ¬(m=n) (enfin, on pourra prendre ça comme définition dans d'autres contextes aussi, mais il y a toujours un certain doute en logique intuitionniste sur ce que ‘≠’ signifie, mais ce doute ne s'étend pas aux entiers), et la négation de m≠n est m=n comme on s'y attend.

Il en va de même de l'ordre : si m,n sont deux entiers naturels, on a m<n ou bien m=n ou bien m>n (et ces trois cas sont exclusifs, c'est-à-dire que la conjonction de deux différents entraîne une absurdité).

(Je passe en petits caractères pour donner quelques résultats métamathématiques sur l'arithmétique de Heyting et son rapport avec l'arithmétique de Peano.)

Bon, malgré tout ça, les entiers naturels se comportent intuitionnistement très largement comme classiquement : on n'a pas besoin des poings pour boxer avec eux ! Cette constatation s'étend, plus largement, à ce qu'on pourrait appeler les structures discrètes et finies, essentiellement parce qu'on peut les formaliser en arithmétique du premier ordre : j'ai parlé ci-dessus d'entiers naturels, mais cela vaut aussi bien si on considère d'autres structures discrètes finies : graphes finis, groupes finis, ce genre de choses. (Par exemple, si on croit que la classification des groupes simples finis est démontrable dans l'arithmétique de Peano, elle l'est aussi dans l'arithmétique de Heyting.)

Les entiers relatifs et les rationnels se comportent bien entendu, comme les entiers naturels du point de vue de l'intuitionnisme : peu importe les détails de la manière dont ils sont construits, il n'y aura pas plus de surprise à leur sujet que pour les entiers naturels. Par exemple, on peut affirmer que deux rationnels sont égaux ou ne sont pas égaux, ou que si r,s sont deux entiers naturels, on a r<s ou bien r=s ou bien r>s.

Cette grande similarité entre théorie classique et théorie intuitionniste va cesser dès qu'on commence à regarder des ensembles, ou des objets construits à partir d'ensembles (par exemple, les nombres réels intuitionnistes se comportent assez différemment des nombres réels classiques). Mais pour en parler un peu plus, il faudrait quand même en dire un peu plus sur la logique qui sert de cadre.

Et cette entrée se termine en queue de poisson

Comme je l'ai dit plus haut, en mathématiques classiques, on travaille de façon « standard » (i.e., disons, sauf précision expresse du contraire) dans ZFC (mais il existe des myriades d'autres systèmes plus forts — comme ZFC enrichi d'axiomes de grands cardinaux — ou plus faibles — comme l'arithmétique du second ordre ou du premier ordre, voire des sous-systèmes de l'une ou de l'autre — qui ont aussi été étudiés et sont parfois utilisés pour travailler). Pour faire des maths constructives il n'y a pas de système standard aussi clair.

Il existe bien des systèmes analogues à ZFC, notamment IZF (ZF intuitionniste, une sorte de transposition évidente des axiomes de ZF en logique intuitionniste, en remplaçant juste l'axiome de de Fondation par le schéma de ∈-récursion, et le schéma de Remplacement par le schéma de Collection), mais il n'est pas franchement très « constructif », et CZF (ZF constructif, dont les axiomes sont un peu plus compliqués à décrire) qui fait en sorte de ne pas permettre la construction d'ensembles de parties tout en permettant la construction de produits cartésiens (et notamment d'ensembles de fonctions), mais aucun ne peut être considéré comme aussi standard que ZFC.

Il est notamment assez peu plaisant, en mathématiques constructives, d'essayer de faire que « tout soit un ensemble » comme on le fait dans ZFC (ou plutôt, comme on fait semblant de le croire en mathématiques classiques pour se forcer à entrer dans le cadre de ZFC). Les entiers naturels, notamment, ont plutôt intérêt à être considérés comme des « atomes », et il n'est pas non plus très heureux de se forcer à encoder une paire d'objets (x,y) comme un ensemble {{x}, {x,y}} : même si je ne crois pas qu'il y ait d'obstacle majeur à ces sujets, ce n'est, disons, pas très agréable. Tout ça n'a pas vraiment de rapport avec l'intuitionnisme, mais l'attention portée aux questions logiques, à la constructivité, à l'économie, au lien avec les systèmes de typage, etc., rendent ces problématiques plus prégnantes dans le cadre de l'intuitionnisme.

Voici quelques unes des choses à regarder quand on a affaire à un système de mathématiques constructives (i.e., quelques unes des choses qui diffèrent d'un système à un autre et qui peuvent être significatives) :

• Le système admet-il des formes de l'axiome du choix ? (Il faudrait revenir sur ce sujet et expliquer ce dont il s'agit, bien sûr, mais au moins approximativement il s'agit de dire qu'affirmer que pour tout x∈X il existe un y∈Y vérifiant une certaine condition P(x,y) équivaut à affirmer qu'il existe une fonction f:X→Y telle que pour tout x∈X on ait P(x,f(x)) ; ce n'est pas tenable en général, mais on pourra vouloir postuler ceci sous certaines conditions, par exemple si X=ℕ.)
• Le système permet-il de former des ensembles de parties 𝒫(X) ou seulement des ensembles Z^X de fonctions ? (L'enjeu, ici, c'est qu'en mathématiques constructives comme en mathématiques classiques on peut identifier 𝒫(X) avec l'ensemble Ω^X des « fonctions caractéristiques » où Ω := 𝒫(1) est l'ensemble des valeurs de vérité, i.e., l'ensemble des parties d'un singleton 1 := {★}. Mais en mathématiques classiques, Ω s'identifie à l'ensemble {0,1} et est indiscutablement un ensemble, alors qu'en mathématiques constructives, Ω est potentiellement quelque chose de gigantesque, on peut penser qu'il est trop gros pour former un ensemble, et c'est notamment le point de vue adopté dans la théorie des ensembles constructives CZF.)
• L'égalité des fonctions est-elle extensionnelle ? Autrement dit, f=g signifie-t-il exactement ∀x.(f(x) = g(x)) ? On peut aussi se poser la même question sur les ensembles : E=F signifie-t-il exactement ∀x.(x∈E ⇔ x∈F) ? (La question est notamment significative pour les valeurs de vérité : est-ce que le fait que deux valeurs de vérité soient égales signifie la même chose que le fait que chacune implique l'autre ?) La réponse à cette question n'est vraiment significative que combinée à la suivante :
• L'égalité est-elle la relation d'équivalence la plus fine permise sur un ensemble ? Notamment, x=y implique-t-il f(x) = f(y) pour toute fonction f et x∈E ⇔ y∈E pour tout ensemble E ? (L'enjeu, ici, est que certaines théories de mathématiques constructives, notamment celles de Bishop, ou des systèmes à la Martin-Löf, ne permettent pas vraiment de former des ensembles quotients, donc on les simule avec des setoïdes qui sont la donnée d'un porteur muni d'une relation d'équivalence qu'on adoube égalité sur l'ensemble ; mais du coup, une « fonction » sur l'ensemble est une fonction sur le porteur qui vérifie les propriétés qu'on vient de dire, et qui, pour embrouiller les choses, portent aussi parfois le nom d'extensionnalité bien qu'il s'agisse en quelque sorte du dual du point précédent ; on pourrait croire que tout ça est complètement neutre, au final, mais cela a des conséquences mathématiques tangibles, puisque l'axiome du choix est valable pour les « porteurs » — et notamment le fait que ℕ soit un porteur est significatif — mais pas forcément pour les setoïdes qui sont leurs quotients. Je ne m'étends pas plus à ce sujet parce que je n'aime pas cette approche qui me semble à la fois compliquée et philosophiquement douteuse, mais comme on croise des mathématiques à la Bishop je ne peux pas ne rien en dire.)

Je suis certainement ignorant d'autres subtilités qui peuvent se présenter, notamment en lien avec la théorie des types (par exemple, je n'ai jamais compris ce que le mot prédicativité signifiait, cf. cette discussion Twitter et notamment les questions que j'y ai posées, mais c'est certainement un mot important pour distinguer un système de maths constructives d'un autre).

❦

Mon but pour la suite serait (aurait été ? est ?) de me placer dans un cadre informel choisi pour ne pas être trop compliqué ni trop déroutant, disons, assez proche de IZF (où on peut former librement des ensembles de parties, l'égalité est la relation d'équivalence la plus fine et elle est extensionnelle ; mais on n'a pas d'axiome du choix sauf l'« axiome du choix unique » ou axiome du non-choix) quoique sans forcer à penser que « tout est un ensemble », et, dans un tel cadre, exposer un peu de théorie des ensembles élémentaire et d'analyse élémentaire (sur les réels de Dedekind), en insistant à la fois sur ce qui reste comme on en a l'habitude en maths classiques (du style si x<y sont deux nombres réels, il existe un rationnel r tel que x<r<y) mais aussi ce qu'on ne peut pas dire (on ne peut pas dire qu'une partie d'un ensemble fini est finie, on ne peut pas dire que pour deux réels x,y on a ou bien x≤y ou bien x≥y, par exemple). J'ai donné l'exemple plus haut de liens Twitter vers quelques démonstrations constructives (ici, là et là), et c'est un peu le type du genre de choses que je voudrais expliquer.

Mais bon, comme je l'ai dit en tête de cette entrée, l'écriture de cette suite s'est embourbée, et de toute façon cette entrée est déjà bien trop longue comme telle, donc je la publie en l'état, malgré cette fin un peu en queue de poisson.

Ajout : il y a une sorte de suite de ce billet par ici.