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

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

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

(vendredi)

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

Méta : J'ai déjà fait plusieurs tentatives pour expliquer sur ce blog ce que sont les mathématiques constructives et comment elles fonctionnent (notamment ici — où j'ai tenté d'expliquer les règles de la logique intuitionniste mais en même temps je me suis embourbé dans des explications sur ce que je devrais ou voudrais écrire —, et ici — où j'ai publié l'introduction / motivation d'une entrée que j'avais commencé à écrire et qui, à cause de ça, s'est complètement embourbée). Je considère ces tentatives comme des échecs. Une raison de cet échec est que je n'ai pas correctement expliqué, pour commencer, de quoi il s'agit et pourquoi on s'y intéresse. Plus tard, j'ai participé à un podcast avec mes collègues Sylvie Benzoni-Gavage et David Monniaux sur le thème mathématiques honnêtes (l'expression vient d'une citation de Poincaré, qui a ensuite donné lieu à un échange sur Twitter), où il a été question au passage d'essayer d'expliquer ce que sont les maths constructives ; mais là aussi, j'ai peur de m'être très mal débrouillé quand j'ai évoqué le sujet. Je voudrais donc faire une nouvelle tentative, en reprenant à zéro. Comme cette tentative-ci est de nouveau en train de s'embourber (ça fait maintenant quelque chose comme six mois que j'ai commencé à l'écrire), je me force à en publier le début comme une entrée autonome, où je parle un petit peu de l'histoire et des motivations, puis je commence à développer quelques principes, quitte à ce que la fin soit un peu abrupte.

Au moins le début de cette entrée (où je parle plus d'histoire des mathématiques que de mathématiques) devrait être très largement compréhensible, quitte à sauter quelques passages un peu plus techniques.

De façon extrêmement schématique (et juste pour lancer le sujet : ceci ne se prétend pas être une explication), les mathématiques constructives sont des mathématiques faites dans une logique particulière appelée logique intuitionniste. (Les termes constructif et intuitionniste sont un peu — mais pas complètement — interchangeables.) Cette logique intuitionniste diffère de la logique usuelle dans laquelle on fait des mathématiques (logique classique) en ce qu'elle abandonne une règle de raisonnement, à savoir la loi du tiers exclu, laquelle affirme — schématiquement — que ❝si quelque chose n'est pas faux alors ce quelque chose est vrai❞. (Ou, ce qui revient au même, la logique intuitionniste abandonne le principe du raisonnement par l'absurde où, pour montrer que P est vrai, on suppose « par l'absurde » que P est faux, on aboutit à une contradiction, et on en conclut que P devait être vrai.) La logique intuitionniste est donc plus faible que la logique classique : du coup, prouver quelque chose en logique intuitionniste est plus difficile ou, si on veut, il y a moins de théorèmes (un théorème en logique intuitionniste est encore un théorème en logique classique, mais un théorème en logique classique n'est pas forcément un théorème en logique intuitionniste) ; donc obtenir un résultat « constructivement » est plus fort que l'obtenir « classiquement », et l'étude des maths constructives consiste en bonne partie à se demander quels résultats classiques sont encore valables constructivement, ou, à défaut, comment on peut les démontrer autrement, ou sinon, les reformuler, pour obtenir quelque chose de constructif.

☞ Oui mais pourquoi donc faire ça ? Pourquoi affaiblir la logique ? Pourquoi précisément comme ça ? Pourquoi remettre en cause la loi du tiers exclu ? Quel est l'intérêt de la démarche ? Quelles sont les règles du jeu ? Et pourquoi ces mots constructif et intuitionniste ? C'est ce que je veux essayer d'expliquer ici.

Plan :

Un (tout petit) peu d'histoire du constructivisme en mathématiques

Commençons par essayer d'expliquer comment cette notion est apparue. Qu'on me permette de faire de l'histoire des maths très schématique et simplifiée, juste pour situer un peu les choses et sans prétendre décrire complètement des positions philosophiques forcément assez complexes :

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→(BA)). 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→(BA), je prends un A et je renvoie une fonction prenant un B et renvoyant un A pourrait correspondre à l'affirmation logique A⇒(BA), 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 ((PQ)⇒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 ((PQ)→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).

Motivations et principes

J'arrête là ce petit aperçu de l'histoire du développement de l'intuitionnisme. Maintenant une autre question qu'on est naturellement en droit de se poser c'est à quoi bon ? : quel est l'intérêt de faire des mathématiques sans la loi du tiers exclu si c'est comme, pour reprendre l'expression de Hilbert, faire de la boxe sans ses poings ? Je vois un certain nombre de justifications possibles, pas du tout exclusives et certainement pas exhaustives :

‣ La première justification est purement intellectuelle : la loi du tiers exclu est un peu à part dans les règles de la logique en ce que la retirer se fait assez naturellement et ne conduit pas à une théorie tellement ridiculement faible qu'on ne peut rien faire avec. Et même si la logique qui en résulte (la logique intuitionniste) n'avait pas d'autre intérêts par ailleurs ou des connexions avec d'autres constructions (comme les topoï ou les théories des types), on pourrait observer qu'elle a une certaine élégance interne qui peut à elle seule expliquer qu'on s'y intéresse. Savoir si tel ou tel énoncé mathématique est démontrable sans recourir à la loi du tiers exclu (ou seulement à une forme limitée de celle-ci) est une question intellectuellement intéressante, comme savoir ce qu'on peut faire sans l'Axiome du Choix : c'est, après tout, le but de la logique d'examiner les modes de raisonnement et de comprendre ce qu'on peut faire avec.

De ce point de vue, il est d'ailleurs normal que les mathématiques constructives aient donné lieu à toutes sortes études façon mathématiques à rebours (voir par exemple ceci ou cela) : autrement dit, on cherche à classifier toutes sortes de principes qu'on peut postuler qui sont plus faibles que la loi du tiers exclu, mais qui ne sont néanmoins pas automatiquement vrais en mathématiques constructives, et à trouver ce qui implique quoi entre ces principes. On peut d'ailleurs dire que cette étude a été démarrée par Brouwer lui-même, qui a introduit certains principes de ce genre, comme le principe limité d'omniscience, qui n'est pas démontrable en logique intuitionniste, est démontrable en logique classique, mais reste strictement plus faible que la loi du tiers exclu. (En l'occurrence, le principe limité d'omniscience affirme que toute suite binaire est soit constamment égale à 0, soit prend la valeur 1.) La situation est assez semblable à l'étude très développée des formes faibles de l'axiome du choix en théorie des ensembles classique, où on cherche, de même, à dégager des principes qui sont des théorèmes de ZFC, ne sont pas démontrables dans ZF, mais restent strictement plus faibles que l'axiome du choix ; et ensuite, à étudier ce qui implique quoi entre ces principes. Bref, il s'agit d'une démarche normale de la logique.

‣ Je pense aussi que faire des mathématiques constructives, quand on est un mathématicien « classique », peut avoir un intérêt pédagogique (ou métapédagogique : relatif à l'enseignement de la pédagogie) : cela peut être une façon de se rappeler « ce que ça fait » de ne pas bien savoir comment approcher un problème, de ne pas savoir dans quelle direction partir, de manquer d'intuition, dans un domaine qui n'est pourtant pas techniquement compliqué comme l'analyse réelle. (À titre d'exemple, j'ai pas mal séché pour produire les démonstrations constructives que j'ai écrites ici, et sur Twitter, et j'ai même tenté ici d'analyser pourquoi j'avais trouvé ça difficile.) Le simple aspect déroutant des choses (attends, je n'ai pas le droit de dire qu'une partie d'un ensemble fini est finie ? je n'ai pas le droit de dire que tout nombre réel est positif ou négatif ?) est instructif de toutes sortes de manières, et notamment le fait qu'on arrive quand même à dire des choses, malgré une difficulté qui semble, a priori, insurmontable. Peut-être, finalement, qu'il est utile pour les boxeurs de s'exercer un peu à boxer sans leurs poings, de manière à développer leur jeu de jambes.

Savoir si un énoncé mathématique est démontrable constructivement, et si oui, comment, ou si on peut le reformuler pour qu'il le devienne, nous permet de mieux comprendre ce qu'on démontre. De mon point de vue, c'est surtout là l'intérêt des mathématiques constructives (et sur l'angle des mathématiques à rebours) : elles permettent d'avoir un regard neuf sur des résultats, phénomènes ou objets qu'on croit bien connaître. Ou de mieux choisir les définitions et les formulations des énoncés : celles qui permettent de mieux faire fonctionner la théorie dans un contexte constructif ont des chances d'être préférables pour d'autres raisons aussi. (De la même façon que je pense qu'il est préférable d'essayer de se passer de l'axiome du choix quand il n'est pas nécessaire, je pense qu'il est opportun d'avoir conscience de quand la loi du tiers exclu est utilisée.)

‣ Disposer d'une preuve constructive d'un théorème est plus difficile mais apporte plus qu'une preuve classique. On peut tenir différents points de vue philosophiques sur ce que ce que ce « plus » signifie exactement (voir par exemple la discussion Twitter — intéressante mais difficile à suivre parce qu'elle a plusieurs branches — qui passe par ici ou ou encore ). Mais il y a au moins des contextes dans lesquels ce « plus » se traduit par une retombée pratique. Notamment, je l'ai dit plus haut, dans un certain nombre de systèmes de mathématiques constructives, avoir une preuve de l'existence d'un objet (pour tout x il existe y tel que <blabla>) permet d'extraire un algorithme construisant l'objet en question (renvoyant y en fonction de x). Mais aussi, un raisonnement en logique intuitionniste va être valable dans un cadre plus large, par exemple dans n'importe quel topos, et il se peut que ce soit la façon la plus efficace de démontrer certains théorèmes même si on ne s'intéresse in fine qu'à un résultat classique (par exemple : montrer un résultat sur les modules en logique intuitionniste donne automatiquement ce même résultat sur les faisceaux de modules ce qui, même si on n'est intéressé qu'à la logique classique, est peut-être la façon la plus simple d'y arriver).

Il est d'ailleurs vraisemblable, que même si nous sommes habitués à faire des mathématiques classiques, nous ayons au moins en partie à l'esprit un certain regard constructif sur les preuves : quand une preuve annonce l'existence d'un objet, nous espérons souvent, même si nous ne l'attendons pas forcément, que cet objet soit rendu explicite, et je pense qu'il est largement admis que la preuve a plus de valeur quand c'est le cas. Parfois le côté explicite de la construction est sous-entendu par l'énoncé (beaucoup d'énoncés de type il existe un isomorphisme entre l'espace vectoriel <machin> et l'espace vectoriel <truc> signifient implicitement plus que oui, ils ont la même dimension) ; parfois nous sommes plus ou moins mal à l'aise quand on triche avec ces règles tacites : j'avais donné ici l'exemple de l'affirmation il existe un programme qui, donné un entier k en entrée, termine toujours en temps fini et renvoie soit l'emplacement de la première occurrence de k fois consécutivement le chiffre 7 dans l'écriture décimale de π, soit faux (ou si on préfère) si une telle occurrence n'existe pas, qui est classiquement démontrable mais qui serait un énoncé un peu malhonnête à écrire sans qualification ni avertissement parce qu'on ne sait pas donner explicitement un tel programme.

Quel que soit le sens philosophique qu'on donne à l'idée d'avoir une preuve intuitionniste d'un énoncé mathématique (et son rapport avec le fait d'avoir une preuve classique), il est bon d'avoir informellement à l'esprit l'interprétation de Brouwer-Heyting-Kolmogorov qui est quelque chose comme ceci :

  • une preuve de PQ (conjonction : P et Q) est un couple formé d'une preuve de P et d'une de Q, c'est-à-dire la donnée d'une preuve de chacun des deux ;
  • une preuve de PQ (disjonction : P ou Q) est la donnée d'une preuve de P ou d'une preuve de Q ;
  • une preuve de PQ (implication : si P alors Q) est une manière de transformer une preuve de P en une preuve de Q ;
  • une preuve de ⊤ (le vrai) est triviale ;
  • une preuve de ⊥ (le faux) n'est pas ;
  • une preuve de ∀x.P(x) (quantification universelle : pour tout x on a P(x)) est une manière de transformer un x en une preuve de P(x) ;
  • une preuve de ∃x.P(x) (quantification existentielle : il existe x tel que P(x)) est la donnée d'un t particulier et d'une preuve de P(t) ;
  • enfin, on traite ¬P (la négation de P) comme un simple raccourci de langage signifiant P⇒⊥ (i.e., P conduit à une absurdité).

Telles que je les ai écrits, ces items ne définissent pas correctement la logique et doivent rester informels, parce qu'on ne sait pas ce que une manière de transformer signifie (voir cependant ce billet pour une formalisation possible de ces règles, dans laquelle une manière de transformer est interprétée comme un algorithme prenant une chose et en renvoyant une autre). Mais cela permet au moins de se faire une idée intuitive des règles de la logique (cf. ci-dessous pour une présentation un peu plus précise).

Il faut cependant que je sois clair sur le point suivant : même si on parle de logique constructive, il n'y a pas forcément de principe métamathématique affirmant que pour si ∃x.P(x) est prouvable alors il y a un t tel que P(t) soit prouvable (ni que si PQ est prouvable alors l'un de P ou de Q est prouvable). Certains systèmes de mathématiques constructives ont en effet cette propriété (notamment l'arithmétique de Heyting, j'en parle un peu ci-dessous), mais le simple fait qu'une théorie soit exprimée en logique intuitionniste ne le garantit pas en soi (ne serait-ce que parce que les axiomes peuvent casser la propriété en question, par exemple s'ils affirment l'existence d'objets auxquels ils ne donnent pas de nom ou s'ils impliquent la loi du tiers exclu). Et le terme constructif est suffisamment vague et informel pour ne pas signifier grand-chose d'autre que travaillant en logique intuitionniste. Disons juste que cette propriété a tendance à être considérée comme désirable.

Il n'est pas non plus correct que les règles de logique permettent en interne d'extraire de ∀x.∃y.P(x,y) une fonction f associant y à x, ou un énoncé du type ∃f.∀x.P(x,f(x)) : il y aurait beaucoup à dire au sujet de l'axiome du choix (qui est justement ce qui passe de l'un à l'autre), mais en tout état de cause, il ne faut pas lire les règles de la logique (même si l'interprétation de Brouwer-Heyting-Kolmogorov peut sembler le suggérer) comme autorisant forcément cette possibilité.

Parlons un peu des règles du jeu

Bon, venons-en au fait : comment peut-on présenter les mathématiques constructives ? Que sont les mathématiques constructives ? Et comment les enseigner ?

Il faut être clair sur un point (que j'ai déjà suggéré à plusieurs reprises ci-dessus) : il n'y a pas un seul et unique système de mathématiques constructives. Déjà ce n'est pas le cas pour les mathématiques classiques, mais au moins les mathématiques classiques ont un « cadre standard », à savoir ZFC, la théorie des ensembles de Zermelo-Fraenkel avec axiome du choix, dans lequel il est généralement admis qu'on se place si on ne dit pas expressément quelque chose d'autre. Il n'en va pas de même pour les mathématiques constructives (et si on prend bêtement ZFC en retirant la loi du tiers exclu, on obtient… ZFC, parce que les axiomes dans leur formulation usuelle impliquent quand même la loi du tiers exclu !). Il y a des systèmes, travaillant en logique intuitionniste, qu'on peut avoir envie de qualifier de constructifs (sachant que ce terme n'a pas une définition bien précise au-delà de travaillant en logique intuitionniste), selon ce qu'on veut faire avec. La logique elle-même mérite d'être précisée, d'ailleurs : si le calcul des prédicats du premier ordre intuitionniste est un cadre bien défini (et c'est ce qu'on imagine assez bien en prenant le calcul des prédicats du premier ordre classique et en pratiquant l'exérèse de la loi du tiers exclu), et donc, par exemple, l'arithmétique de Heyting du premier ordre, qui s'obtient en prenant les mêmes axiomes que l'arithmétique de Peano mais en calcul des prédicats du premier ordre intuitionniste, on peut aussi définir toutes sortes de logique d'ordre supérieur plus ou moins sophistiquées, en logique intuitionniste comme en logique classique, si ce n'est qu'en logique intuitionniste elles sont peut-être plus utiles parce qu'on peut vouloir limiter le recours à la théorie des ensembles.

Néanmoins, pour beaucoup de choses qu'on veut dire, la fixation exacte de la logique, du système d'axiomes, de la formalisation, n'a pas tant d'importance que ça. Dans n'importe quel système éducatif, on commence à faire des maths avant de savoir ce qu'est ZFC, et c'est aussi ce qui s'est passé historiquement : on peut donc légitimement avoir l'audace de faire des maths constructives sans formaliser un cadre dans lequel faire des maths constructives (surtout que, comme je l'ai dit plus haut, Brouwer avait la plus grande méfiance pour la logique formelle). Mais je n'aime pas non plus l'idée de faire comme si les difficultés n'existaient pas, et l'approche de Bishop et compagnie de rejeter la logique et d'agiter les mains pour faire comme si le lecteur comprenait bien sûr quelles sont les règles de raisonnement autorisées sans vraiment les donner, me déplaît pas mal (surtout que, dans le cas de Bishop et ses élèves, leur système de base est bizarre et exotique, avec, à la place des ensembles, des setoïdes qu'ils cachent sous le tapis et que ces décisions font que magiquement certaines versions de l'axiome du choix valent et d'autres pas : c'est assez incompréhensible, et, il faut le dire, la présentation de Bishop est pédagogiquement épouvantable). À tout le moins, si on veut s'adresser à un lecteur déjà un minimum formé aux mathématiques classiques, je pense qu'il faut insister lourdement sur les différences avec les mathématiques classiques, sur les choses qu'on n'a pas le droit d'affirmer et sur les surprises qu'on peut avoir, au lieu d'essayer de gommer ces différences.

Je vais donc finir cette entrée en essayant d'entrer enfin un tout petit peu dans le sujet lui-même, c'est-à-dire, en parlant enfin de mathématiques constructives elles-mêmes et pas juste de leur histoire, de leur intérêt et des points de vue qu'on peut avoir à leur sujet.

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 PQ, je peux prouver les deux ; pour utiliser PQ, je peux utiliser P ou utiliser Q (comme il me plaira) ;
  • pour conclure PQ, je peux prouver l'un des deux ; pour utiliser PQ, je peux traiter deux cas, c'est-à-dire être prêt à utiliser l'un quelconque des deux (sans que je choisisse lequel) ;
  • pour conclure PQ, 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 PQ ; pour utiliser PQ, 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∧(QR) équivaut à (PQ)∨(PR). (Voici la démonstration en détails : dans le sens P∧(QR) ⇒ (PQ)∨(PR) : en supposant P∧(QR), j'ai d'une part P et d'autre part QR ; je traite deux cas : soit j'ai Q, soit j'ai R : dans le premier cas j'ai P et Q, c'est-à-dire PQ, et de même dans le second j'ai PR, donc dans les deux cas j'ai bien (PQ)∨(PR) ; pour le sens réciproque (PQ)∨(PR) ⇒ P∧(QR), supposons (PQ)∨(PR) et traitons deux cas : si j'ai PQ, j'ai d'une part P et d'autre part Q donc QR, et dans l'autre cas de même j'ai P et QR.) 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∨(QR) implique (PQ)∧(PR) (démonstration : en supposant P∨(QR), je traite deux cas, soit j'ai P soit j'ai QR, dans le premier cas j'ai bien PQ puisque j'ai P et j'ai aussi PR pour la même raison, et dans le second cas, j'ai à la fois Q et R, donc j'ai bien PQ puisque j'ai Q et j'ai aussi PR puisque j'ai R) ; mais cette fois, la réciproque n'est plus valable en général : en logique intuitionniste, P∨(QR) peut être strictement plus fort que (PQ)∧(PR) la réciproque est également valable (chacun de ‘∧’ et ‘∨’ est distributif sur l'autre) [correction () : 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 () : J'avais initialement écrit ci-dessus que si ‘∧’ est distributif sur ‘∨’ comme en logique classique, on a que P∨(QR) implique (PQ)∧(PR) 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 (PQ)∧(PR) comme P ∨ (PR) ∨ (QP) ∨ (QR), 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∨(QR). 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.(PQ(x)) alors que, dans l'autre sens P∨∀x.(Q(x)) implique mais peut être strictement plus fort que ∀x.(PQ(x)) (classiquement les deux sont équivalents). La deuxième est que, dans un sens que je ne veux pas définir, P∨(QR) et (PQ)∧(PR) 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 (PQ)∧(PR) ⊢ P∨(QR) et P∨(QR) ⊢ (PQ)∧(PR) 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 (PQ)×(PR) ne sont pas identifiables alors que P×(QR) 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 (PQ)⇒R équivaut à (PR)∧(QR), et que P⇒(QR) équivaut à (PQ)∧(PR), mais qu'en revanche (PQ)⇒R est potentiellement plus faible que (PR)∨(QR) et que P⇒(QR) est aussi potentiellement plus faible que (PQ)∨(PR). (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, ¬(PQ) est la même chose que (¬P)∧(¬Q), mais ¬(PQ) est potentiellement plus faible que (¬P)∨(¬Q). Il peut aussi être bon de noter que ¬¬(PQ) équivaut à (¬¬P)∧(¬¬Q) et ¬¬(PQ) é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.(PR(x)) ; en revanche, (∀x.P(x))⇒R est potentiellement plus faible que ∃x.(P(x)⇒R), et P⇒(∃x.R(x)) que ∃x.(PR(x)). Le cas le plus important à retenir est que ¬∃x.P(x) équivaut à ∀xP(x) mais que ¬∀x.P(x) est potentiellement plus faible que ∃xP(x). On peut noter que ¬¬∀x.P(x) implique ∀x.¬¬P(x) (mais la réciproque ne vaut pas en général).

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

Le fait que ¬∃x.P(x) équivaille à ∀xP(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 X1,…,Xr 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 2r combinaisons de valeurs de vérité des variables, et il y a donc 22r formules différentes à équivalence près, et décider si une formule est démontrable peut se faire en testant chacune des 2r 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 ψ(X1,…,Xr) où ψ est une certaine formule propositionnelle dans les variables X1,…,Xr. En logique classique on ne peut rien ajouter de la sorte, car soit ψ est vraie pour toute valeur de vérité de X1,…,Xr, et elle est démontrable (donc l'axiome n'ajoute rien), soit il existe une combinaison de valeurs de vérité de X1,…,Xr telle que ψ(X1,…,Xr) 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 ((XY)⇒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 (XY) ∨ (YX) (axiome de Dummett), ou encore (((¬¬X)⇒X) ⇒ (X∨¬X)) ⇒ ((¬¬X)∨¬X) (axiome de Scott), ou encore (¬X⇒(Y₁∨Y₂)) ⇒ ((¬XY₁) ∨ (¬XY₂)) (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 UV 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=(mnm)

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))φ(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 mn 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 mn 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.)

Pour être un peu plus précis qu'un vague les théorèmes de l'arithmétique de Peano ont tendance à être également valables en arithmétique de Heyting, voici un résultat métamathématique important et assez précis à ce sujet. Supposons que P est une formule du type la machine de Turing suivante s'arrête (i.e., termine en temps fini) quelle que soit l'entrée m qu'on lui fournit en entrée ; ou, pour être plus précis, supposons que P est une formule arithmétique Π₂, c'est-à-dire de la forme ∀m.∃n.Q(m,n) (cela ne change rien si on autorise plusieurs quantificateurs universels et plusieurs quantificateurs existentiels tant qu'ils sont de la forme ∀⋯∀∃⋯∃, c'est-à-dire que tous les universels précèdent tous les existentiels) où Q est une formule arithmétique Δ₀, c'est-à-dire une formule dont tous les quantificateurs (portent sur les entiers naturels) et sont bornés, autrement dit de la forme ∀kt (qu'il faut bien sûr comprendre comme signifiant ∀k.((kt)⇒⋯)) ou bien ∃kt (qu'il faut bien sûr comprendre comme signifiant ∃k.((kt)∧⋯)) où t est un terme (une formule arithmétique Δ₀ est algorithmiquement testable, puisque chaque quantificateur, étant borné, ne porte que sur un nombre fini de possibilités, et la formule la machine de Turing e, si on lui fournit l'entrée m, s'arrête en au plus n étapes est exprimable sous arithmétique Δ₀). • Alors : si P est démontrable dans l'arithmétique de Peano, elle l'est aussi dans l'arithmétique de Heyting ; et on peut même être un peu plus précis en divisant ce résultat en deux étapes : premièrement, si ∀m.∃n.Q(m,n) est démontrable dans l'arithmétique de Peano, alors ∀m.¬¬∃n.Q(m,n) est démontrable dans l'arithmétique de Heyting, et deuxièmement, si c'est le cas, alors en fait ∀m.∃n.Q(m,n) est démontrable dans l'arithmétique de Heyting. (Dans tout ça, il faut comprendre arithmétique de Peano/Heyting du premier ordre, même si la technique fonctionne pour beaucoup de théories et il me semble que ça doit encore marcher pour l'arithmétique de Peano/Heyting du second ordre, mais je n'ai pas vérifié soigneusement.) De plus, ce résultat métamathématique (et les deux étapes que je viens de dire) est lui-même constructif, c'est-à-dire qu'on a un procédé algorithmique tout à fait explicite qui prend une démonstration dans Peano de P et qui renvoie une démonstration dans Heyting de P, et le fait que ce procédé soit correct est lui-même démontrable dans l'arithmétique de Heyting du premier ordre (ou dans des théories encore plus faibles).

À titre d'exemple de ce que je viens de dire, si la conjecture de Goldbach (tout entier pair est la somme de deux nombres premiers) est démontrable dans l'arithmétique de Peano, elle l'est dans l'arithmétique de Heyting : il suffit de considérer la machine de Turing qui prend un m en entier et cherche une écriture de 2m comme somme de deux nombres premiers et termine quand elle l'a trouvée (Goldbach affirme que cette machine termine pour chaque entrée : si ce fait est démontrable dans Peano il l'est aussi dans Heyting) ; a contrario, d'ailleurs, si la conjecture de Goldbach est réfutable dans l'arithmétique de Peano, elle l'est aussi dans l'arithmétique de Heyting au sens où celle-ci démontre l'existence d'un entier pair qui n'est pas somme de deux nombres premiers (considérer la machine de Turing qui ignore son entrée et cherche un contre-exemple à la conjecture de Goldbach).

L'arithmétique de Heyting (du premier ordre disons, même si c'est aussi vrai au second ordre) possède deux propriétés métamathématique désirables pour une théorie qualifiée de constructive : la propriété de la disjonction, et la propriété de l'existence numérique. La propriété de la disjonction affirme que si elle démontre PQP,Q sont des énoncés (i.e., des formules closes, i.e., sans variable libre), alors elle démontre forcément soit P soit Q ; et la propriété de l'existence numérique affirme que si elle démontre ∃n.P(n) (là aussi un énoncé, i.e., n est la seule variable libre de P(n)), alors il y a un n entier naturel explicite tel que P(n) soit prouvable (ou plus exactement, P(SSS⋯S0) où le symbole ‘S’ est répété n fois). (L'arithmétique de Peano classique, elle, ne possède pas les deux propriétés que je viens de dire : on s'en rend compte en prenant un énoncé comme soit l'arithmétique de Peano est cohérente soit elle n'est pas cohérente, ou bien soit n=0 et l'arithmétique de Peano est cohérente, soit n=1 et l'arithmétique de Peano n'est pas cohérente, qui sont des tautologies en logique classique, mais aucune branche de l'alternative n'est prouvable dans l'arithmétique de Peano ; les énoncés en question ne sont donc pas prouvables dans l'arithmétique de Heyting.) La propriété de la disjonction et de l'existence numérique pour l'arithmétique de Heyting ne sont pas elles-mêmes prouvables dans l'arithmétique de Heyting pour des raisons Gödeliennes, mais elles sont néanmoins constructives, et il existe un algorithme qui prend une preuve de PQ, respectivement ∃n.P(n), dans l'arithmétique de Heyting et renvoie soit une preuve de P soit une preuve de Q, respectivement un n et une preuve de P(n) (bon, dit comme ça ce n'est pas très impressionnant parce que, classiquement, l'algorithme pourrait juste énumérer toutes les preuves possibles jusqu'à en trouver une qui convienne, mais justement, sa terminaison est prouvable sans faire appel au principe de Markov). Une variante de la propriété de l'existence numérique fonctionne encore pour une formule ayant des variables libres, et permet de conclure que si l'arithmétique de Heyting démontre l'énoncé ∀m.∃n.P(m,n), alors il existe machine de Turing e telle que l'arithmétique de Heyting démontre ∀m.(em↓∧P(m,em)) (lire : quel que soit m, la machine de Turing e termine quand on lui fournit m en entrée, et le résultat n vérifie P(m,n)).

Un autre fait métamathématique méritant d'être signalé concernant l'arithmétique de Heyting est que son fragment propositionnel est le même que le pur calcul propositionnel intuitionniste. Plus exactement, si une formule propositionnelle ψ(X1,…,Xr) de r variables est telle que ψ(P1,…,Pr) est démontrable en arithmétique de Heyting (du premier ordre, je ne sais pas pour le second ordre) pour tous énoncés arithmétiques P1,…,Pr, alors en fait ψ(X1,…,Xr) est démontrable en pur calcul propositionnel intuitionniste (i.e., c'est une tautologie). Ou, si on préfère (les résultats métamathématiques que dont je parle sont des théorèmes classiques, je ne sais pas si on peut les rendre constructifs), si ψ(X1,…,Xr) est une formule propositionnelle qui est une tautologie classique mais n'est pas une tautologie intuitionniste, il existe des énoncés arithmétiques P1,…,Pr tels que ψ(P1,…,Pr) ne soit pas un théorème de l'arithmétique de Heyting (alors que c'en est un de l'arithmétique de Peano classique puisque ψ est une tautologie classique) : ceci généralise le fait que l'arithmétique de Peano est cohérente ou bien elle ne l'est pas (cas où ψ := X∨¬X et P := “l'arithmétique de Peano est cohérente”) n'est pas démontrable dans l'arithmétique de Heyting. Il serait intéressant de chercher à fabriquer de tels énoncés en prenant pour ψ l'axiome de Scott ou celui de Kreisel-Putnam (cf. ci-dessus).

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 xX il existe un yY vérifiant une certaine condition P(x,y) équivaut à affirmer qu'il existe une fonction f:XY telle que pour tout xX 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 ZX 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.(xExF) ? (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 xEyE 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 xy ou bien xy, par exemple). J'ai donné l'exemple plus haut de liens Twitter vers quelques démonstrations constructives (ici, et ), 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.

↑Entry #2721 [older| permalink|newer] / ↑Entrée #2721 [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]