David Madore's WebLog: Introduction aux mathématiques constructives : 1. un peu de théorie des ensembles

Rappel du contexte et quelques notations

Redisons rapidement ici quelques unes des choses que j'ai évoquées dans ma précédente introduction aux maths constructives.

Très sommairement, donc, les maths constructives sont des maths faites en logique intuitionniste, c'est-à-dire dans laquelle on abandonne le principe de tiers exclu selon lequel toute affirmation P est soit vraie soit fausse (P∨¬P), ou, ce qui revient au même, que si une affirmation P n'est pas fausse alors elle est vraie (¬¬P⇒P ; en revanche, P n'est pas vrai est la même chose que P est faux, c'est la définition). (Les termes de maths constructives et de logique intuitionniste ne sont pas tout à fait interchangeables, mais je vais les traiter un peu comme tels : voir la partie historique de l'entrée précédente pour plus de précisions sur l'histoire des termes.) La logique intuitionniste étant plus faible que la logique classique, tout résultat obtenu dans ce cadre restera valable dans le cadre de la logique classique : on aura moins de théorèmes (et ceux qui restent peuvent devenir plus durs à démontrer), mais du coup, on peut considérer qu'une preuve constructive est plus forte (plus rare, donc plus difficile) qu'une preuve classique. Parmi les raisons de vouloir s'imposer la discipline de chercher à faire des preuves constructives, on peut notamment mentionner :

• certains pensent (mais ce n'est pas mon cas) que les mathématiques constructives sont plus correctes, parce qu'elles sont plus en accord avec leur conception philosophique de l'univers mathématique (cf. ce que je racontais sur Brouwer) ; on peut aussi simplement penser que la logique intuitionniste, à défaut d'être plus correcte, est plus économique que la logique classique, et qu'on doit donc essayer de travailler avec ;
• les preuves constructives (donc les théorèmes qu'elles produisent) sont valables plus largement que les preuves classiques (notamment, un énoncé constructivement valable est valable dans n'importe quel topos muni d'un objet d'entiers naturels) ;
• les preuves constructives apportent plus d'information que les preuves classiques (notamment, dans certaines conditions, on peut extraire un algorithme d'une preuve constructive qui calcule l'objet dont le théorème affirme l'existence — d'où le terme de constructif) ;
• la question de savoir ce qui est prouvable constructivement apporte un nouveau regard sur des théorèmes connus, qui peut être intéressant du point de vue logique, ou du point de vue pédagogique, en permettant de mieux comprendre les liens logiques entre les théorèmes et les difficultés à passer de l'un à un autre ;
• le fait de s'assurer que les définitions ou les lemmes utilisées fonctionnent bien dans un contexte constructif peut être un critère pour choisir la « bonne » définition ou la « bonne » preuve entre des possibilités classiquement indifférentes (et on peut espérer que la « bonne » se généralisera mieux) : par exemple, classiquement, en topologie, on peut définir les fermés à partir des ouverts ou les ouverts à partir des fermés, mais constructivement, seule la première approche fonctionne, ce qui suggère qu'il vaut mieux définir une topologie par ses ouverts ;
• certains outils informatiques assistants de preuve, provenant de systèmes de typage, fonctionnent naturellement en logique intuitionniste : même si on peut les faire travailler en logique classique en postulant le principe du tiers exclu, on peut penser qu'une preuve valable constructivement sera plus facile à produire, à analyser ou à utiliser dans de tels outils ;
• et enfin, bien sûr, la question de savoir si un résultat est valable constructivement est une question mathématique (classique !) tout à fait légitime, qu'on peut considérer pour son intérét intellectuel intrinsèque.

Mais avant de commencer vraiment, il faut que je dise un mot sur les règles du jeu. J'ai (plus ou moins) décrit les règles de la logique dans une partie de mon entrée précédente, et mon but est de les illustrer par l'exemple, donc je ne vais pas les réexpliquer ici, mais il faut que je parle un peu du cadre dans lequel je me place (parce qu'il n'y a pas un cadre unique pour faire des maths constructives) :

Dans ce qui suit, je vais me placer dans un cadre informel utilisant des conventions fondationnelles choisies pour dérouter le moins possible le mathématicien classique. Techniquement, les choses que je vais dire (correctement formalisées) seront vraies dans n'importe quel topos muni d'un objet d'entiers naturels, ou seront des théorèmes de la théorie IZF (un analogue assez standard de ZF en logique intuitionniste), mais je n'ai pas envie de définir ni ce qu'est un topos ni ce que sont les axiomes d'IZF parce que ce serait contraire à mon objectif pédagogique. Je vais essayer de rester agnostique ou vague quant à la question de savoir si je considère que « tout est un ensemble » (comme c'est le cas si on se place dans IZF) ou si les objets ont des types (ça n'a pas vraiment de rapport avec l'intuitionnisme, disons qu'il est peut-être plus tentant en maths constructives de travailler dans des théories des types que dans des fondements ensemblistes, mais comme mon but est de faire des choses élémentaires je n'ai pas envie de faire de choix ni même d'expliquer la différence). Pour ceux qui ont besoin de détails (les autres, sautez la fin de ce paragraphe), je précise cependant certaines des choses que je prends dans mes fondations, ou qui en résulte. D'abord, l'égalité fonctionne comme on l'attend classiquement, c'est-à-dire que c'est la plus fine relation d'équivalence et elle est extensionnelle (c'est-à-dire que d'une part si x=y alors f(x)=f(y) pour n'importe quelle fonction f, prédicat ou expression faisant intervenir une variable libre ; et d'autre part si deux ensembles X,Y ont les mêmes éléments, ∀t.(t∈X⇔t∈Y), alors ils sont égaux, et si deux fonctions f,g ayant mêmes source et but prennent les mêmes valeurs ∀t.(f(t)=g(t)), alors elles sont égales). Je suppose aussi que les ensembles de parties peuvent être formés librement, et je noterai 𝒫(X) l'ensemble des parties de X (par ailleurs l'ensemble des parties d'un singleton jouera notamment un rôle crucial comme l'ensemble des « valeurs de vérité », je vais y venir). En revanche, je ne peux pas supposer l'axiome du choix (on va voir qu'il implique le tiers exclu), et je ne veux pas le faire, même pas l'axiome du choix dénombrable, parce que même classiquement il y a un intérêt à étudier ce qui se passe sans lui, mais je vais revenir sur ce sujet ; je vais quand même postuler l'« axiome du choix unique » (ou axiome du non-choix) que j'expliquerai plus loin.

☞ Je rappelle à toutes fins utiles que dire P (où P est une formule logique) signifie exactement la même chose que de dire P est vraie (cf. le début de cette entrée, qui concerne les maths classiques mais ce n'est pas pertinent ici) ; et dire P est fausse ou P n'est pas vraie signifie exactement la même chose que ¬P (la négation de P, qui est un raccourci de langage pour P⇒⊥, c'est-à-dire si P est vraie, alors les poules ont des dents). Là où la logique intuitionniste diffère de la logique classique c'est qu'elle ne permet pas de passer de P n'est pas fausse (i.e., ¬¬P) à P est vraie. (En revanche, trois négations équivalent à une seule, quatre à deux, etc. : il est faux que P n'est pas fausse est pareil que P est fausse, et il n'est pas faux que P n'est pas fausse est pareil que P n'est pas fausse.)

Ça n'a rien à voir avec la logique intuitionniste, mais je signale aussi, s'il y avait un doute, que P⇒Q⇒R doit se lire comme P⇒(Q⇒R), et qu'il est équivalent à P∧Q⇒R (lequel doit se lire, lui, comme (P∧Q)⇒R). Sauf dans le contexte où je signale informellement un tas d'implications en série : on a les implications successives P ⇒ Q ⇒ R ⇒ S doit bien sûr se comprendre comme on a P⇒Q et aussi Q⇒R et aussi R⇒S. J'espère que cela ne causera pas de confusion.

Pour attirer l'attention sur les principales surprises des maths constructives par rapport aux maths classiques, j'utiliserai le souligné comme ceci (pour dire quelque chose comme on ne peut pas affirmer que pati-pata) ou le rouge comme ceci (pour un bout de raisonnement qui n'est pas valable constructivement ; mais de toute façon je le dirai toujours explicitement).

Ensembles vides et habités, singletons, sous-terminaux, valeurs de vérité

Commençons par la notion la plus simple qui soit, celle d'ensembles vide et habités.

On dit que E (un ensemble « dans l'univers » ou bien une partie d'un autre ensemble X, j'ai dit que je ne voulais pas rentrer dans ce genre de questions) est vide lorsqu'il n'a pas d'élément, c'est-à-dire, en symboles, ¬∃x.(x∈E) (il n'existe pas de x qui appartienne à E) ou, ce qui revient logiquement au même ∀x.¬(x∈E) (quel que soit x, il est faux que x appartienne à E), ou si on préfère l'écrire comme ça, ∀x∈E.(⊥) (tout x appartenant à E conduit à une absurdité, le symbole ‘⊥’ désigne l'énoncé tautologiquement faux, et l'ensemble vide est donc l'ensemble des x qui vérifient ⊥), avec la convention habituelle que ∀x∈E.(P(x)) signifie ∀x.(x∈E⇒P(x)) (de même que ∃x∈E.P(x) signifie ∃x.(x∈E∧P(x)) ; et je rappelle par ailleurs que ¬P signifie P⇒⊥).

Tout ce que je viens de dire est exactement pareil qu'en mathématiques classiques, et on note ∅ l'ensemble vide (unique par extensionnalité, au moins en tant que partie d'un X fixé).

Mais la notion d'ensemble non-vide, i.e., d'ensemble vérifiant ¬(E=∅), elle, n'a que très peu d'intérêt constructif : un ensemble E est non-vide s'il vérifie ¬¬∃x.(x∈E) ou, ce qui revient au même ¬∀x.¬(x∈E), mais on ne peut pas faire grand-chose avec un ensemble non-vide : notamment, on ne peut pas affirmer qu'un ensemble non-vide a un élément (je vais revenir là-dessus ci-dessous).

Ce qui est beaucoup plus utile, donc, est la notion d'ensemble habité, c'est-à-dire d'ensemble vérifiant ∃x.(x∈E), ou, si on préfère l'écrire comme ça, ∃x∈E.(⊤) (le symbole ‘⊤’ désigne l'énoncé tautologiquement vrai) : un ensemble habité est un ensemble ayant un élément. Du coup, un ensemble vide est simplement un ensemble non-habité (ou inhabité, mais attention à la confusion entre français et anglais ici !).

Il s'agit là d'un exemple extrêmement simple d'un phénomène assez courant en mathématiques constructives : quand on a deux notions qui classiquement sont simplement la négation l'une de l'autre (parfois les deux ont un nom, parfois seulement l'une des deux), constructivement on va généralement attacher plus d'importance à celle qui permet de définir l'autre comme sa négation (ici, habité permet de définir vide comme non-habité, mais vide ne permet pas de définir habité, qui est plus fort que non-vide) : généralement parlant, en mathématiques constructives, les négations ont d'assez mauvaises propriétés, donc on s'attache autant que possible à définir des notions positives. (Bien sûr, la situation n'est pas toujours aussi simple que ce que je viens de décrire : parfois une même notion classique donne naissance à plusieurs notions constructives entre lesquelles il n'est pas évident de choisir, voir par exemple ici/là sur Twitter concernant la notion de « corps ».)

À part l'ensemble vide, un autre ensemble très important est la notion de singleton (ou terminal si on a la théorie des types/catégories à l'esprit) : un singleton est un ensemble habité dont tous les éléments sont égaux. Le singleton est donc le pendant ensembliste de la notion d'existence unique : comme en maths classiques, on notera ∃!x∈E.(P(x)), lire il existe un unique x∈E tel que P(x) pour dire ∃x∈E.(P(x)) ∧ ∀u∈E.∀v∈E.(P(u)⇒P(v)⇒(u=v)), c'est-à-dire que d'une part il existe x∈E tel que P(x) et d'autre part si u,v∈E vérifient tous les deux P alors ils sont égaux. Avec cette notation, on peut dire que E est un singleton lorsque ∃!x.∈E.(⊤), c'est-à-dire ∃x.∈E.(⊤) ∧ ∀u∈E.∀v∈E.(u=v), ou, ce qui revient au même (exercice !) ∃x.∈E.∀y∈E.(y=x).

On peut également définir la notion d'ensemble sous-terminal, qui est un ensemble dont tous les éléments sont égaux, ∀u∈E.∀v∈E.(u=v) : classiquement ce n'est pas intéressant (classiquement, un ensemble sous-terminal est soit vide soit un singleton), mais constructivement elle est suffisamment intéressante pour mériter un nom, et, à vrai dire, pas évidente à visualiser. Un singleton est donc un ensemble habité et sous-terminal.

☞ On pourrait entrer dans des arguties pour savoir si on doit différencier les singletons les uns des autres ou si on a même le droit de se poser la question : dans la théorie des ensembles intuitionniste IZF, comme dans ZFC (classique), il y a « autant de singletons que d'ensembles » (on a {x}={y} si et seulement si x=y par extensionnalité) ; dans un point de vue plus proche de la théorie des types, la question de l'égalité entre singletons n'a pas de sens, on peut juste dire qu'ils sont isomorphes (c'est-à-dire en bijection, cf. ci-dessous), sauf si on parle de parties singletonnes d'un ensemble plus gros. Ces questions ne m'intéressent pas ici, j'ai écrit ci-dessus que je préférais rester agnostique à leur sujet puisque je travaille dans un cadre informel. Donc si j'écris, disons {●} pour un singleton, il faut comprendre n'importe quel singleton, peu importe, ils sont isomorphes et c'est tout ce qui importe ici, sans préjuger de savoir s'il y en a un seul ou si la question a un sens (dans le cadre d'IZF comme de ZFC), on peut supposer que je parle de {∅}. Et même si j'écris occasionnellement le singleton, je veux de même juste dire n'importe quel singleton à isomorphisme près.

Je n'ai pas grand-chose de particulier à dire sur les parties d'un ensemble : une partie E d'un ensemble X, notée E⊆X, est un ensemble dont tous les éléments appartiennent à X, on peut la considérer elle-même comme un ensemble, et si on a F⊆E⊆X alors F⊆X (tandis que, a contrario, lorsque E,F sont deux parties de X, l'inclusion F⊆X peut s'écrire ∀x∈X.(x∈F⇒x∈E)). Par ailleurs, si p(x) est une formule logique faisant intervenir une variable libre x, on peut former la partie, notée {x∈X : p(x)} des éléments x de X qui vérifient p(x), tout ceci comme en maths classiques, et inversement, toute partie E⊆X peut être considérée comme définie par la formule x∈E. Le principe d'extensionnalité affirme que deux parties E,F de X sont égales lorsque ∀x∈X.(x∈E⇔x∈F), autrement dit F⊆E et E⊆F impliquent F=E. L'intersection de deux parties E,F de X, notée E∩F peut se définir comme {x∈X : x∈E ∧ x∈F}, et leur réunion, notée E∪F comme {x∈X : x∈E ∨ x∈F}. Aucune différence ici avec les maths classiques, mais évidemment des différences apparaissent rapidement si on commence à définir la notion de complémentaire {x∈X : ¬(x∈E)} d'une partie E (comme on s'en doute facilement, on ne peut pas affirmer, par exemple, que le complémentaire du complémentaire redonne la partie de départ).

Je noterai 𝒫(X) l'ensemble des parties de X, c'est-à-dire que E⊆X équivaut à E∈𝒫(X) (en écrivant ceci je prends un point de vue « ensembliste » ; pour avoir une vision plus catégorique, il y aurait une relation binaire d'appartenance entre X et 𝒫(X) qui classifie les parties de X ; mais je ne veux pas entrer dans ces questions de fondement qui n'ont rien à voir avec la question des maths constructives, et je souhaite rester informel).

Considérons un instant les parties d'un singleton. Disons qu'on ait fixé 1 := {●} un singleton de référence (dont on note ‘●’ l'unique élément : sa valeur n'a aucune importance, la seule chose qui importe est qu'il soit fixé). Si p est une affirmation (c'est-à-dire un énoncé logique sans variable libre), on peut considérer la partie {● : p}, c'est-à-dire l'ensemble {t∈{●} : p} des t de 1 qui vérifient p ; ici, comme la variable t n'apparaît pas dans p, dire que t (qui est forcément égal à ●) vérifie p, ça veut juste dire que p est vraie… c'est-à-dire juste p. À titre d'exemple, {● : 2+2=4} vaut {●}, tandis que {● : 2+2=5} vaut ∅ (et classiquement, ce sont les deux seules possibilités). Inversement, l'affirmation p (i.e., p est vraie) est logiquement équivalente à l'affirmation que ● appartient à {● : p}, ou, pour éviter d'avoir à parler de ●, au fait que {● : p} est habitée (si cette partie a un élément, c'est forcément ●).

Classiquement, cette construction {● : p} (mais qui, je répète, est juste un cas particulier de la construction {t∈X : P(t)} désignant le sous-ensemble de X constitué des éléments t vérifiant P(t), par exemple {t∈ℝ : 0≤t≤1} = [0;1]) n'a pas grand intérêt : car classiquement, soit p est vraie et on obtient {●}, soit elle est fausse et on obtient ∅. Mais constructivement, elle a une grande importance : la valeur de vérité d'une affirmation p est (ou peut s'identifier, selon le point de vue qu'on adopte) à la partie {● : p} (c'est-à-dire l'ensemble {t∈{●} : p} des éléments de 1={●} qui vérifient p) ; et inversement, comme je l'ai dit, une partie U de 1={●} peut s'identifier à la valeur de vérité de l'affirmation ●∈U, soit ∃t∈1.(t∈U), du fait que U est habitée. Deux valeurs de vérité sont particulièrement importantes, le vrai, noté ⊤, identifié à la partie pleine (c'est-à-dire ici, habitée) {● : ⊤} = {●} de 1, et le faux, noté ⊥, identifié à la partie vide {● : ⊥} = ∅ de 1.

Ceci est l'occasion d'introduire le concept de contre-exemple brouwérien. Considérons l'affirmation (†) tout ensemble est soit habité soit vide (qui, classiquement, est évidente). On se doute bien qu'elle est constructivement suspecte. Je ne peux pas donner de contre-exemple à (†), car il faudrait pour cela construire un modèle non-classique de la logique intuitionniste, et je n'ai pas introduit les outils pour. Mais je peux faire tenir le raisonnement suivant :

Supposons l'affirmation (†) tout ensemble est soit habité soit vide.

Soit p une affirmation quelconque (i.e., une valeur de vérité). Considérons l'ensemble {● : p} qui lui est associée. D'après (†), soit {● : p} est habité, soit {● : p} est vide.

Si {● : p} est habité, alors p est vraie. En effet, un élément de {● : p} est, en particulier, un élément de {●}, donc c'est ●, et ● appartient à {● : p} si et seulement si p vaut.

Si {● : p} est vide, alors p est fausse. En effet, dans ce cas, ● n'appartient pas à {● : p}, c'est-à-dire que ¬p vaut.

On a donc prouvé, en utilisant (†), que p est vraie ou fausse, i.e., p∨¬p, pour quelque affirmation p que ce soit. C'est-à-dire qu'on a prouvé la loi du tiers exclu.

Bref, l'affirmation (†) implique la loi du tiers exclu. Comme manifestement on ne veut pas admettre la loi du tiers exclu, on ne peut non plus pas affirmer que tout ensemble est soit habité soit vide. Ceci n'est pas une réfutation de (†) (qui est vraie en maths classiques, donc elle ne saurait pas être fausse en maths constructives), mais c'est un rejet, c'est-à-dire, on ne peut pas espérer la démontrer et on ne veut certainement pas la prendre pour axiome. De façon générale, un contre-exemple brouwérien à une affirmation consiste à montrer que cette affirmation implique soit la loi du tiers exclu, soit un autre principe qui, quoique plus faible que la loi du tiers exclu, est néanmoins considéré comme un tabou constructif (par exemple la loi faible du tiers exclu ¬p∨¬¬p ou des « principes d'omniscience » dont je dois parler ultérieurement).

(À titre d'exercice, on pourra utiliser un contre-exemple brouwérien pour justifier qu'on ne peut pas affirmer que tout ensemble est vide ou non-vide, car cela implique la loi faible du tiers exclu ¬p∨¬¬p ; et qu'on ne peut pas affirmer que tout ensemble non vide est habité, car cela implique la loi d'élimination des doubles négations ¬¬p ⇒ p, qui implique à son tour la loi du tiers exclu pour des raisons de pure logique.)

Bien sûr, pour considérer qu'un contre-exemple brouwérien oblige à rejeter une affirmation parce que celle-ci implique un tabou constructif, encore faut-il savoir que le tabou constructif n'est pas lui-même démontrable (après tout, il est logiquement concevable que la loi du tiers exclu soit démontrable même si ce n'est pas évident). Pour ça, il faut utiliser de vrais modèles : mais ceci sort du cadre de ce billet (mais on pourra par exemple consulter celui sur le topos effectif, qui est un monde dans lequel la loi du tiers exclu, ou même la loi faible du tiers exclu, ne sont pas valables), donc je me contenterai ici de contre-exemples brouwériens.

Produits, fonctions, injections, surjections, bijections

Je ne crois pas avoir quoi que ce soit d'intéressant à dire sur le produit cartésien X×Y de deux ensembles : comme en mathématiques classiques, c'est l'ensemble des paires (x,y) avec x dans X et y dans Y, sachant que (x,y)=(x′,y′) si et seulement si x=x′ et y=y′. Je ne cherche pas à savoir ce qu'est une paire exactement (est-ce un concept atomique, ou est-ce qu'elle est codée comme {{x}, {x,y}} ?), parce que ce n'est pas intéressant et ça n'a rien à voir avec mon propos ici. On peut définir de même des produits cartésiens finis X₁×⋯×X_n, avec la convention qu'on retrouve « le » singleton si n=0 : je parlerai de produits cartésiens plus généraux plus bas. Une relation entre ensembles X et Y est simplement une partie du produit cartésien X×Y.

On a aussi (exactement comme en maths classiques) une notion de réunion disjointe de deux ensembles, qu'on peut noter quelque chose comme X+Y ou X⊎Y ou X⊔Y ou je ne sais quoi : c'est là qu'il est un peu agaçant d'avoir le point de vue ensembliste où les éléments de tout ensemble appartiennent à quelque chose de fixe alors qu'on se fout, bien sûr, de ce que sont exactement les éléments de X+Y tant qu'il est réunion de deux parties en bijection (cf. ci-dessous) avec X et Y respectivement, et qui ne s'intersectent pas. (Si on tient à avoir le point de vue ensembliste, on définira X+Y comme (X×{0})∪(Y×{1}), mais voilà justement le genre de détails qui n'a aucun intérêt.)

Comme en mathématiques classiques, on peut identifier la notion de fonction X→Y avec celle de relation fonctionnelle, c'est-à-dire de partie f⊆X×Y du produit cartésien qui vérifie ∀x∈X.∃!y∈Y.((x,y)∈f). Cette identification n'est pas totalement anecdotique (elle dépend de choses que j'ai supposées ci-dessus, essentiellement l'axiome du « choix unique » sur lequel je dois revenir), mais comme je l'ai dit, je veux plutôt me mettre dans un cadre où la différence avec les mathématiques classiques n'est pas exagérée, et je veux certainement admettre le principe du choix unique. On peut alors noter f(x) l'unique y tel que (x,y)∈f, s'en servir dans les formules, etc. On note Y^X (ou éventuellement Hom(X,Y)) l'ensemble des fonctions X→Y, c'est-à-dire qu'on exige ici implicitement que les fondements sur lesquels on travaille permettent librement de former de tels ensembles de fonctions. Noter qu'on a f=f′ (pour deux fonctions f,f′:X→Y) si et seulement si f(x)=f′(x) pour tout x∈X (extensionnalité pour les fonctions), cela dépend aussi d'un certain nombre de choix fondationnels que j'ai faits ci-dessus. La notion de composition de fonctions ne pose pas de problème.

On dit que f est injective lorsque deux éléments ayant la même image par f sont égaux, ∀x∈X.∀x′∈X.((f(x)=f(x′))⇒(x=x′)) (c'est la même notion qu'en mathématiques classiques, mais je l'écris explicitement pour qu'il n'y ait pas de doute sur la façon dont on la tourne), et surjective lorsque tout élément de Y est l'image par f d'un élément de X, soit ∀y∈Y.∃x∈X.(f(x)=y) (dans tous les cas, l'image de f, notée f(X)⊆Y, ou im(f), sera {y∈Y : ∃x∈X.(f(x)=y)}) ; et on dit que f est bijective lorsqu'elle est à la fois injective et surjective.

Si on préfère : f est injective, resp. surjective, resp. bijective, lorsque pour tout y∈Y l'image réciproque f⁻¹({y}) := {x∈X : f(x)=y} est sous-terminale, resp. habitée, resp. un singleton. Comme en mathématiques classiques, une fonction bijective f:X→Y a une (unique) réciproque g:Y→X au sens où la composée dans les deux sens est l'identité sur l'ensemble correspondant (et l'existence de g implique que f est bijective, et g elle-même est bijective). On peut dire que deux ensembles sont isomorphes ou simplement en bijection lorsqu'il existe une bijection entre eux.

Une relation d'équivalence sur un ensemble X est une partie R⊆X² qui est ①réflexive (∀x∈X.(xRx)), ②symétrique (∀x,y∈X.(xRy ⇒ yRx)) et ③transitive (∀x,y,z∈X.(xRy ⇒ yRz ⇒ xRz)), où j'ai écrit uRv pour dire (u,v)∈R. Lorsque c'est le cas, on peut définir l'ensemble X/R comme l'ensemble des classes d'équivalence, c'est-à-dire l'image de l'application X→𝒫(X) définie par x↦{y∈X : xRy} (la classe d'équivalence de x pour R ; si on préfère, une classe d'équivalence est une partie C⊆X qui est habitée et telle que la restriction de R à C soit une clique, autrement dit C²⊆R ; et X/R est l'ensemble de ces parties). On a alors par définition une surjection X → X/R (dite surjection canonique), et toute surjection f:X→Y peut s'écrire (à bijection près) sous cette forme en appelant R la relation {(u,v)∈X² : f(u)=f(v)} (plus exactement, il y a une unique bijection X/R → Y envoyant la classe de x sur f(x)). Plus généralement, toute fonction f:X→Y peut se factoriser comme la composée de la surjection canonique X → X/R où R est la relation qui vient d'être dite, suivie d'une bijection X/R → im(f), et de l'injection canonique im(f) → Y (c'est-à-dire l'inclusion de la partie en question).

Comme en mathématiques classiques, une fonction f:X→Y est injective si et seulement si elle est simplifiable à gauche, ce qui signifie par définition que si g,g′:T→X sont deux fonctions (depuis T un ensemble quelconque) vérifiant f∘g = f∘g′, alors g=g′. La démonstration est facile et exactement la même qu'en mathématiques classiques, mais donnons-la complètement parce que c'est quand même instructif :

Démonstration du fait qu'une fonction est injective si et seulement si elle est simplifiable à gauche :

Le sens « seulement si » est très facile : si f est injective et si f∘g = f∘g′, alors on a f(g(t)) = f(g′(t)) pour tout t dans T, donc g(t)=g′(t) en appliquant la définition de l'injectivité de f, et comme ceci est vrai pour tout t cela signifie bien (par extensionnalité) que g=g′.

Pour ce qui est du « si », il suffit de prendre pour T un singleton, notons-le 1={●}, et si x,x′∈X de considérer les fonctions g,g′:1→X envoyant ● sur x et x′ respectivement : si f(x)=f(x′) alors f∘g = f∘g′ puisqu'elles coïncident sur l'unique élément ● de 1, donc g=g′ par l'hypothèse de simplifiabilité à gauche, donc g(●)=g′(●), c'est-à-dire x=x′, ce qui montre l'injectivité. ∎

On peut aussi affirmer, comme en mathématiques classiques, que f:X→Y est surjective si et seulement si elle est simplifiable à droite, c'est-à-dire que que si g,g′:Y→Z vérifient g∘f = g′∘f, alors g=g′. Le « seulement si » est de nouveau une vérification purement formelle (si f est surjective et si g∘f = g′∘f, alors donné un y dans Y on peut écrire y=f(x) par surjectivité, et on a g(f(x)) = g′(f(x)), c'est-à-dire g(y)=g′(y), et comme y était arbitraire dans Y ceci montre g=g′). Mais pour le « si », cette fois, la démonstration classique « évidente » ne fonctionnera pas :

Démonstration (classique) du fait que toute fonction simplifiable à droite est surjective : Supposons que lorsque g,g′:Y→Z vérifient g∘f = g′∘f, alors g=g′, et on veut montrer que f:X→Y est surjective. Soit y∈Y quelconque. Posons Z={0,1}. On définit g:Y→Z comme la fonction valant constamment 0, et g′ comme la fonction valant 1 sur y et 0 ailleurs. S'il n'existe pas x∈X tel que f(x)=y, alors g∘f = g′∘f (ces deux fonctions valent 0 partout), donc par l'hypothèse qu'on a faite, g=g′, et notamment en évaluant en y on a 0=1, ce qui est absurde. Donc il existe x∈X tel que f(x)=y, et on a montré la surjectivité de f. ∎

Cette démonstration est classiquement valable, mais il y a deux points qui posent problème constructivement : premièrement le fait de définir g′ par g′(u)=1 si u=y et g′(u)=0 sinon : ceci définit une fonction sur la réunion de {y} et de son complémentaire {u∈Y : ¬(u=y)}, mais constructivement on ne peut pas affirmer que tout élément u∈Y est soit égal à y soit non égal à y, donc on n'a pas défini une fonction (totale, seulement une fonction partielle) ; et deuxièmement, le fait de conclure qu'il existe un x tel que f(x)=y alors qu'on a (enfin, aurait, s'il n'y avait pas le premier problème) seulement démontré que son inexistence était contradictoire.

Pourtant, l'énoncé est valable constructivement : ici on a affaire à un cas où la démonstration classique ne fonctionne pas mais le résultat reste néanmoins valable, simplement il faut faire plus attention pour le prouver. C'est un exercice intéressant d'essayer d'y arriver, mais je pense qu'il est très difficile si on n'a pas l'habitude des maths constructives. Voici deux démonstrations différentes qui fonctionnent constructivement, que je m'attarde à rédiger en détails parce que ce sont de bons exemples de techniques de preuves.

Démonstration (constructive nº1) du fait que toute fonction simplifiable à droite est surjective : Supposons que lorsque g,g′:Y→Z vérifient g∘f = g′∘f, alors g=g′, et on veut montrer que f:X→Y est surjective.

Soit W := (Y×{0}) ∪ (Y×{1}) la réunion disjointe de deux copies de Y ; et soit R la relation d'équivalence sur W définie par (y,i)R(y′,j) lorsque y=y′ et que soit i=j soit il existe un x∈X tel que f(x)=y ; soit enfin Z := W/R le quotient de W par cette relation d'équivalence. (Autrement dit, on prend deux copies de Y et on identifie les éléments des deux copies quand ils sont dans l'image de f.)

Ce R est bien une relation d'équivalence, le seul point non trivial étant la transitivité, mais si (y,i)R(y′,j) et (y′,j)R(y″,k), alors d'une part y=y′=y″, et d'autre part soit i=j et j=k, soit il existe un x∈X tel que f(x)=y, donc en tout cas (y,i)R(y″,k).

On définit alors g:Y→Z comme la fonction envoyant y∈Y sur la classe d'équivalence de (y,0) et g′:Y→Z comme celle envoyant y∈Y sur la classe d'équivalence de (y,1). La définition de R fait que g(f(x)) = g′(f(x)) (puisque (f(x),i)R(f(x),j) quels que soient i,j), et par l'hypothèse qu'on a faite, on en déduit g=g′. Notamment, si y∈Y est quelconque, on a (y,0)R(y,1), c'est-à-dire (comme ¬(0=1)) qu'il existe un x∈X tel que f(x)=y. Comme le y était quelconque, on a montré la surjectivité de f. ∎

Démonstration (constructive nº2) du fait que toute fonction simplifiable à droite est surjective : Supposons que lorsque g,g′:Y→Z vérifient g∘f = g′∘f, alors g=g′, et on veut montrer que f:X→Y est surjective. Soit 1 := {●} un singleton, et Ω := 𝒫(1) son ensemble de parties. On définit alors g:Y→Ω comme la fonction envoyant n'importe quel y∈Y sur la partie habitée ⊤ := {●}, et g′:Y→Ω comme la fonction envoyant y∈Y sur la partie {● : ∃x∈X.(y=f(x))} (la valeur de vérité de ∃x∈X.(y=f(x))).

Montrons que g∘f = g′∘f : si x∈X et y=f(x), alors ∃t∈X.(y=f(t)) est vrai, donc {● : ∃t∈X.(y=f(t))} est habité et vaut donc {●}, c'est-à-dire que g(y)=g′(y), bref, g(f(x)) = g′(f(x)). Par l'hypothèse qu'on a faite, on en déduit g=g′. Notamment, si y∈Y est quelconque, g(y)=g′(y), c'est-à-dire que {●} = {● : ∃x∈X.(y=f(x))} est habité, et donc ∃x∈X.(y=f(x)). Comme le y était quelconque, on a montré la surjectivité de f. ∎

Voir ici ou là pour des reformulations de l'une ou l'autre de ces démonstrations. La première démonstration utilise la construction catégorique d'un conoyau : elle est peut-être plus générale que la seconde en ce sens que (correctement reformulée) elle doit fonctionner dans une catégorie ayant les limites et colimites finies ou quelque chose comme ça, ou, côté ensembliste, elle fonctionne dans la théorie CZF laquelle est plus limitée qu'IZF (on ne peut pas montrer que Ω := 𝒫(1) est un ensemble dans CZF), mais ce n'est pas vraiment ça qui me préoccupe ici parce que j'ai dit que je me plaçais dans un cadre (topos ou IZF) qui permet librement de prendre des ensembles de parties.

La seconde démonstration montre la manière dont on peut utiliser l'ensemble Ω des parties d'un singleton (je vais en reparler ci-dessous). Elle montre aussi l'intérêt d'une construction assez surprenante quand on vient des maths classiques, qui est de former un ensemble du genre {a∈A : p} où p ne fait pas intervenir a (ici A=1, mais ça peut servir pour d'autre ensembles) : en maths classiques, évidemment, un tel ensemble sera soit A soit ∅ donc ce n'est pas très intéressant de l'écrire comme ça, mais en maths constructives cela nous donne un ensemble B qui est une partie de A et dont les éléments garantissent que p est vérifiée (on peut donc tenir des raisonnements du style soit a∈B : alors p est vraie, donc <…> qui sont extrêmement perturbants quand on n'a pas l'habitude vu que p ne fait pas du tout intervenir a).

Bref, constructivement (comme classiquement), une fonction simplifiable à gauche est la même chose qu'une fonction injective, et une fonction simplifiable à droite est la même chose qu'une fonction surjective.

En revanche, on ne peut pas affirmer en mathématiques constructives qu'une fonction injective est inversible à gauche (ou « rétractable ») ni qu'une fonction surjective est inversible à droite (ou « sectionnable ») : ici, une fonction inversible à gauche (rétractable) est une fonction f:X→Y elle qu'il existe g:Y→X vérifiant g∘f=id_X, et une fonction inversible à droite (sectionnable) est une fonction f:X→Y elle qu'il existe g:Y→X vérifiant f∘g=id_Y. L'affirmation toute fonction surjective est inversible à droite (sectionnable) est essentiellement l'axiome du choix, dont je vais parler plus bas, et on peut la mettre en doute même en mathématiques classiques. Quant à l'affirmation toute fonction injective est inversible à gauche (rétractable), elle souffre déjà d'une exception en mathématiques classiques : l'unique injection ∅→Y n'a pas de rétraction si Y est non-vide car il n'y a pas d'application Y→∅ : en mathématiques classiques on a l'habitude de passer ce genre de cas sous le tapis, mais c'est une indication du fait que quelque chose va casser en mathématiques constructives où on ne peut pas dire qu'un ensemble est vide ou habité (ni même vide ou non-vide). Et de fait, on ne peut même pas affirmer que toute fonction injective dont la source est habitée soit inversible à gauche : un « contre-exemple brouwérien », en anticipant sur des choses que je vais expliquer plus loin, est fourni par l'application {0,1}→Ω (où Ω=𝒫({●})) envoyant 0 sur ⊥=∅ et 1 sur ⊤={●}, qui est injective car ⊥≠⊤, mais on peut vérifier qu'elle est rétractable si et seulement si la loi faible du tiers exclu ∀p∈Ω.(¬p∨¬¬p) vaut.

L'ensemble Ω des valeurs de vérité

Puisque je l'ai déjà mentionné plusieurs fois, il y a un ensemble — à bijection près — qui joue un rôle extrêmement important, c'est celui qu'on appelle indifféremment ensemble des valeurs de vérité ou ensemble des parties du singleton ou encore classificateur de sous-objet : c'est l'ensemble des parties de 1 := {●}, il découle des choix fondationnels (non automatiques) que j'ai faits qu'il s'agit bien là d'un ensemble, et on le note souvent Ω.

L'identification entre l'ensemble des parties d'un singleton et l'ensemble des valeurs de vérité est obtenue, comme je l'ai déjà expliqué plus haut, en identifiant la valeur de vérité de p (une affirmation quelconque) à la partie {● : p} (c'est-à-dire {t∈1 : p}), et inversement, une partie U⊆1 à la valeur de vérité de l'affirmation U est habitée (i.e., ∃t∈1.(t∈U)). Bien sûr, avec cette identification, la valeur de vérité de p∧q (le et logique) est l'intersection des valeurs de vérité de p et de q, et la valeur de vérité de p∨q (le ou logique) est la réunion des valeurs de vérité de p et de q. Il n'y a pas de notation standard pour la valeur de vérité de p⇒q, mais on peut noter qu'elle est vraie (i.e., habitée, en tant que partie de {●} !) si et seulement si la valeur de vérité de p est incluse dans celle de q (en tant que parties de {●}). Deux valeurs de vérité sont particulièrement importantes, le vrai, noté ⊤, identifié à la partie pleine (c'est-à-dire ici, habitée) {● : ⊤} = {●} de 1, et le faux, noté ⊥, identifié à la partie vide {● : ⊥} = ∅ de 1.

Cette identification entre valeurs de vérité (voire, entre les affirmations logiques dont on prend la valeur de vérité) et parties de {●} est bien commode, et ne pose pas de problème sur le fond, même si elle peut causer des doutes ou conflits de notation parfois possiblement source de confusion. Soulignons donc que si p∈Ω, l'affirmation p est vraie (soit p=⊤, où ⊤ désigne la partie pleine de 1) lorsque p est vue comme une valeur de vérité, signifie la même chose que p est habitée (soit ∃t∈1.(t∈p)) lorsque p est vue comme une partie de 1 ; et la valeur de vérité de ces affirmations est justement p ; si bien que p est essentiellement interchangeable avec p=⊤ (lorsque p est vue comme une valeur de vérité) ou avec ∃t∈1.(t∈p) (lorsque p est vue comme une partie de 1). Si p∈Ω (dépendant peut-être de a), on considérera qu'il est légitime d'écrire {a∈A : p} pour {a∈A : p=⊤}, ou ce qui revient au même {a∈A : ∃t∈1.(t∈p)}. Du coup, faut-il écrire p∧q ou bien p∩q, par exemple ? C'est assez arbitraire. Et si on écrit p⇒q, cela peut désigner l'affirmation que p est inclus dans q, ou bien la valeur de vérité de cette affirmation. Encore une fois, il n'y a là aucune difficulté mathématique, mais un certain chaos sur les notations.

J'enfonce notamment le clou sur le fait que l'égalité sur Ω est donnée par l'équivalence, autrement dit p=q est l'affirmation que p⇔q est vraie, ou simplement p⇔q (ici, p⇔q est un raccourci de notation pour p⇒q et q⇒p) : en effet, p⇒q a la valeur de vérité de p⊆q et q⇒p de de q⊆p, et l'extensionnalité nous dit que p=q signifie p⊆q et q⊆p, et p⇔q est un raccourci pour p⇒q et q⇒p.

Signalons aussi que de même que p=⊤ signifie la même chose que p, de même, p=⊥ signifie la même chose que ¬p (car p⇔⊥ équivaut à p⇒⊥ et ⊥⇒p, et le premier est noté ¬p tandis que le second est tautologiquement vrai).

Comme en mathématiques classiques, on peut librement identifier une partie d'un ensemble X et sa fonction indicatrice X→Ω, c'est-à-dire qu'on dispose d'une bijection entre 𝒫(X) et Ω^X envoyant U⊆X sur la fonction X→Ω dont la valeur en x∈X est la valeur de vérité {● : x∈U} de x∈U (c'est ça la fonction indicatrice de U), et inversement, envoyant une fonction χ:X→Ω sur la partie {x∈X : χ(x)=⊤} de X formé des x tels que χ(x) soit vraie (=habitée).

La réunion et l'intersection de deux parties U,V⊆X d'un même ensemble X s'obtiennent en prenant le ou logique, respectivement le et logique, de leurs fonctions indicatrices. Deux telles parties U,V⊆X sont égales si et seulement si leurs fonctions indicatrices sont égales (au sens de l'équivalence logique, cf. ci-dessus) : c'est l'axiome d'extensionnalité.

Du point de vue algébrique, Ω peut être décrit comme un cadre (frame), c'est-à-dire un ensemble partiellement ordonné dans lequel toute partie finie a une borne inférieure (je n'ai pas défini ce que fini veut dire en maths constructives, mais on peut reformuler ça en disant qu'il y a un plus grand élément et que deux éléments quelconques ont une borne inférieure), une partie quelconque une borne supérieure, et les bornes inf finies sont distributives sur les bornes sup quelconques. (Les bornes inf finies sont données par les intersections, les bornes sup quelconques par les réunions. En fait, dans tout cadre les bornes inf quelconques existent toujours et pas juste les bornes inf finies, mais la distributivité est pour les bornes inf finies sur les bornes sup quelconques ; il vaut mieux considérer que la structure algébrique est donnée par les bornes inf finies et sup quelconques, et les morphismes de cadres sont ceux qui préservent ces opérations-là ; par exemple, les ouverts d'un espace topologique quelconque forment un cadre, c'est d'ailleurs le point de départ de la topologie sans points.) En fait, l'ensemble des parties d'un ensemble quelconque est un cadre, mais Ω a des propriétés assez particulières : pour commencer, c'est l'objet initial de la catégorie des cadres, c'est-à-dire que pour tout cadre L il existe un unique morphisme de cadres (= application préservant les bornes inf finies et bornes sup quelconques) Ω→L (donnée en envoyant p∈Ω sur ⋁{⊤ : p} où ⋁ désigne ici l'opération de borne sup dans L et ⊤ le plus grand élément de L).

Pour montrer la manière dont Ω se comporte de façon assez surprenante, voici un résultat facile mais assez représentatif de la manière dont on peut raisonner dessus (et cette démonstration est, il faut le dire, très déroutante quand on n'a pas l'habitude des maths constructives, donc je prends le soin de l'écrire en détails) :

Proposition : si f:Ω→Ω vérifie f(⊤)=⊤, alors f(p)≥p pour tout p∈Ω (l'ordre ‘≤’ sur Ω est bien sûr l'inclusion des parties de 1, ou, ce qui revient au même, l'implication logique des valeurs de vérité).

Démonstration : En considérant p∈Ω comme une partie de 1={●}, on veut montrer p⊆f(p). Pour cela, il suffit de montrer que tout élément de p appartient à f(p). Soit t un élément de p. Alors p est habité, donc p=⊤ (c'est-à-dire {●}) et t=●. Mais par l'hypothèse f(⊤)=⊤, on a f(p)=⊤, donc t (qui vaut ●) appartient bien à f(p). On a donc bien montré que tout élément t de p appartient à f(p), c'est-à-dire p⊆f(p) comme affirmé. ∎

Cette proposition est mystifiante parce que que d'un côté on ne peut pas affirmer que le vrai (⊤={●}) et le faux (⊥=∅) soient les seuls éléments de Ω (ce serait exactement le tiers exclu), de l'autre, la connaissance de la seule valeur de f sur le vrai (alors qu'on n'a rien supposé sur f, pas de préserver de structure algébrique, par exemple) suffit à entraîner une conclusion sur une valeur quelconque dans Ω. Et la démonstration est mystifiante parce que pour montrer que p⊆f(p) on prend un élément de p, et, surprise, de la simple existence de cet élément, en fait on sait tout de cet élément, de p, et de la valeur de f en p.

On peut se demander si, du coup, on pourrait aussi obtenir f(p)=p pour tout p à partir de, disons, f(⊤)=⊤ et f(⊥)=⊥ ; mais ce n'est pas possible : notamment, f(p) := ¬¬p vérifie f(⊤)=⊤ et f(⊥)=⊥ mais si c'est l'identité alors le tiers exclu vaut.

Voici un résultat dans le même genre, mais plus sophistiqué, que je reproduis comme exemple des raisonnements assez subtils qu'on peut tenir à propos de Ω :

Théorème de l'involution de Higgs : si f:Ω→Ω est injective (rappelons que cela signifie que f(u)=f(v) implique u=v), alors en fait f∘f=id_Ω (c'est-à-dire f(f(p))=p pour tout p∈Ω).

Démonstration : Commençons par rappeler le point crucial suivant qui servira tout du long : si p,q∈Ω sont tels que p=⊤ implique q=⊤, alors en fait p≤q. (J'ai déjà expliqué que l'ordre partiel sur Ω était à la fois l'implication et l'inclusion, mais ce point est suffisamment important pour que j'enfonce le clou une fois de plus en le démontrant. En effet, il s'agit de montrer p⊆q ; pour cela, prenons t un élément de p : mais alors p est habité, donc p=⊤, et par ailleurs t=●, donc par l'hypothèse qu'on a faite, q=⊤, donc t est bien élément de q.)

Et bien sûr, du coup, p,q∈Ω sont tels que p=⊤ équivaille q=⊤, alors en fait p=q. C'est-à-dire qu'on peut montrer que deux éléments de Ω sont égaux montrant que l'égalité de l'un à ⊤ implique l'égalité de l'autre.

Passons maintenant à la démonstration proprement dite du théorème.

Montrons d'abord le lemme suivant : (toujours sous l'hypothèse que f:Ω→Ω est injective,) si f(p)=⊤ alors f(f(p))=p (ce qui est un cas particulier de ce qu'on veut démontrer). Démonstration du lemme : si on suppose p=⊤ alors l'hypothèse f(p)=⊤ devient f(⊤)=⊤, et réciproquement, si on suppose f(⊤)=⊤, alors f(p)=⊤=f(⊤), donc p=⊤ puisque f est injective ; on a ainsi montré que p=⊤ équivaut à f(⊤)=⊤, donc par le point crucial, c'est qu'on a f(⊤)=p, donc f(f(p))=f(⊤)=p, ce qui conclut la démonstration du lemme. ∎

Le lemme entraîne notamment (toujours sous l'hypothèse f injective) que si (†) f(p)=⊤, alors on a f(f(f(p))) = f(p) = ⊤.

Mais réciproquement, si on suppose (‡) f(f(f(p)))=⊤, alors on va montrer f(p)=⊤ ; pour cela posons q := f(f(p)) ; l'hypothèse (‡) est alors f(q)=⊤, donc le lemme donne f(f(q))=q, c'est-à-dire f(f(f(f(p)))) = f(f(p)), et par l'injectivité de f on en déduit f(f(f(p))) = f(p) puis f(f(p)) = p, et l'hypothèse (‡) devient alors f(p)=⊤, comme annoncé.

Bref, aux deux paragraphes précédents, on a montré que (†) f(p)=⊤ est équivalent à (‡) f(f(f(p)))=⊤. Par le point crucial, on en déduit f(f(f(p))) = f(p), et ce, sous la seule hypothèse que f est injective. Or puisque f est injective, justement (donc simplifiable à gauche), ceci donne f(f(p)) = p, la conclusion finale souhaitée. ∎

Honnêtement, je ne comprends rien à ce qui se passe dans cette démonstration (que j'avais déjà écrite ici sur Twitter et que j'ai rédigée en décodant une démonstration — dans l'Éléphant de Johnstone — écrite dans un style diagrammatique qui me semblait encore plus opaque). Je veux dire, je la comprends localement, je comprends que tout s'enchaîne logiquement et qu'elle est correcte, mais c'est de la magie noire : je n'ai aucune intuition de ce qui se passe, et je me demande bien si des gens arrivent à avoir une intuition sur quelque chose du genre. En tout cas, ça illustre bien le caractère magique (à mes yeux) de Ω.

Quelques notions constructives sans intérêt en maths classiques

J'insiste sur le fait que tout ce qui est démontrable en maths constructives (en tout cas dans le cadre dans lequel je me suis placé) l'est aussi en maths classiques. Il ne peut donc rien y avoir de nouveau. Mais il peut y avoir des notions sans intérêt en maths classiques (parce qu'elles sont triviales ou se ramènent trivialement à une autre notion) qui deviennent intéressantes en maths constructives.

L'axiome du choix (ne sera pas admis)

L'axiome du choix sous sa forme générale est l'affirmation que toute fonction surjective est inversible à droite, i.e., que si f:X→Y est surjective alors il existe g:Y→X vérifiant g∘f=id_X (intuitivement, g choisit un élément dans chaque f⁻¹(y) pour y∈Y, lequel est habité par définition de la surjectivité). Il revient au même de dire que ∏_i∈I Z_i est habité si chacun des Z_i est habités (c'est d'ailleurs si et seulement si, car manifestement si (x_i)_i∈I ∈ ∏_i∈I Z_i alors x_i ∈ Z_i pour chaque i) : ici, ∏_i∈I Z_i est justement défini comme l'ensemble des fonctions (notées (x_i)_i∈I pour i ↦ x_i) telles que x_i ∈ Z_i pour chaque i. (Du moins, ça c'est dans une vision ensembliste des choses ; dans une vision catégorique, ∏_i∈I Z_i est simplement le produit au sens de la théorie des catégories.) L'équivalence annoncée résulte dans un sens en prenant Y=I et pour X la réunion disjointe ⨄_i∈I Z_i des Z_i et f:X→Y prenant constamment la valeur i sur chaque Z_i, et dans l'autre sens, I=Y et pour Z_i la fibre f⁻¹(i) de f au-dessus de i. Je ne rentre pas dans les détails, mais il n'y a rien d'intelligent ici.

L'intérêt de l'axiome du choix est de permettre de réécrire des énoncés du type ∀y∈Y.∃x∈X.(P(x,y)) en un énoncé du type ∃g∈X^Y.∀y∈Y.(P(g(y),y)).

Doit-on admettre l'axiome du choix constructivement ? La première chose à dire est que sous sa forme générale, il est incompatible avec le constructivisme en raison du résultat (contre-exemple brouwérien) suivant :

Théorème de Diaconescu : l'axiome du choix général implique le tiers exclu.

Démonstration : Soit p∈Ω une valeur de vérité. On veut montrer que p∨¬p. Soit {0,1} un ensemble ayant deux éléments distincts (i.e., la réunion disjointe de deux singletons) nommés 0 et 1. Posons U := {x∈{0,1} : (x=0)∨p} et V := {x∈{0,1} : (x=1)∨p}.

Soit Y = {U, V} (noter que je n'affirme ni que U et V sont égaux ni qu'ils ne sont pas égaux). Et soit X la réunion disjointe des éléments de Y, c'est-à-dire, pour être plus clair, l'ensemble des couples (x,W) avec x∈{0,1} et W∈{U,V} qui vérifient x∈W.

(Attention, je dois dire la réunion disjointe des éléments de Y et pas la réunion disjointe de U et V car cette dernière formulation, notée U⊎V, prend deux une copie de chaque ensemble : même classiquement, ce n'est pas la même chose, puisque si p est vraie, on a U=V et X est la réunion disjointe de ce seul ensemble, c'est-à-dire qu'on peut l'identifier à U=V={0,1}. Mais constructivement, on ne peut pas distinguer les deux cas U et V sont égaux et U et V ne sont pas égaux.)

Soit f:X→Y envoyant (x,W) sur W. Manifestement, f est surjective puisque chacun de U et V est habité. (En plus détaillé : si W∈Y, on a soit W=U soit W=V ; dans le premier cas, W est dans l'image de f puisque c'est l'image de (0,U), dans le second aussi puisque c'est l'image de (1,V).)

L'axiome du choix prétend donc qu'il existe g:Y→X qui choisit un élément x de chaque W ∈ Y = {U,V}. Appelons u := g(U) et v := g(V). Comme u,v∈{0,1}, qui est un ensemble discret (en tant que réunion disjointe de deux singletons), on a soit u=v, soit ¬(u=v). Considérons ces deux cas.

Dans le cas u=v, on a soit u=v=0 soit u=v=1 (de nouveau parce que {0,1} est la réunion disjointe de deux singletons), et on va traiter ces deux sous-cas séparément. Dans le premier sous-cas, on a v=0, et comme v∈V par définition, c'est-à-dire que 0 ∈ {x∈{0,1} : (x=1)∨p}, et donc on a p. De même dans le sous-cas u=v=1 : on a u=0, et comme u∈U par définition, c'est-à-dire que 1 ∈ {x∈{0,1} : (x=0)∨p}, et donc on a p. Bref, on a montré que si u=v alors p.

Maintenant, dans le cas où ¬(u=v), on ne peut pas avoir p : car p vaut, on a U={0,1} et de même V={0,1}, donc U=V, donc forcément g(U)=g(V), c'est-à-dire u=v, et on vient de supposer le contraire. C'est donc que p est absurde, autrement dit ¬p dans ce cas. Bref, on a montré que si ¬(u=v) alors ¬p.

Finalement, on a montré p∨¬p. Comme le choix de p était arbitraire, on a la loi du tiers exclu. ∎

Bref, en maths constructives, on ne peut pas admettre l'axiome du choix sous sa forme la plus générale. On peut cependant trouver que cette démonstration triche un peu (l'axiome du choix a surtout été obligé de « choisir » si U et V étaient égaux ou pas) et se demander s'il ne faudrait pas chercher à admettre des formes de l'axiome du choix qui ne seront pas problématiques de la sorte.

(Une digression un peu philosophique.)

Il y a une sorte de justification philosophique constructive à l'axiome du choix : pour prouver ∀y∈Y.∃x∈X.(P(x,y)), on aimerait croire qu'il s'agit (puisque c'est justement tout le principe du constructivisme) de produire une façon de convertir y∈Y en un x∈X qui exhibe P(x,y), et à ce moment-là, pourquoi ne pas collecter ces x en une fonction y ↦ g(y) ? Ce qui fait que cette justification ne marche pas, cependant, c'est que même si on doit pouvoir trouver un x∈X à partir de y∈Y qui vérifie P(x,y), ce x pourrait dépendre pas juste de y mais de la manière dont il est fourni. (Et ça se voit bien dans la preuve ci-dessus : le choix évident de x consiste à choisir 0 pour U et 1 pour V, mais ceci fait abstraction du fait que U et V pourraient être égaux, qui est le nerf de la guerre.)

Néanmoins, en ce limitant à certains ensembles Y on peut considérer que cette justification est valable. Notamment, si Y est l'ensemble ℕ des entiers naturels (que je vais introduire dans une suite de ce billet, mais bon, on sait quand même que ce que c'est) on peut la trouver convaincante, car un entier naturel, il n'y a pas trente-six façons de le présenter : il est ce qu'il est. J'ignore ce qu'il faut penser de l'axiome du choix pour les ensembles (Y) discrets, mais au moins l'axiome du choix pour Y=ℕ, ou axiome du choix dénombrable, et même un axiome un peu plus fort appelé « axiome du choix dépendant » (qui affirme que si X est un ensemble habité muni d'une relation ρ telle que ∀x∈X.∃x′∈X.(xρx′). alors il y a une suite u:ℕ→X telle que ∀n∈ℕ.(u(n)ρu(n+1))), est admis par un certain nombre de constructivistes, comme Douglas Bridges et son école. Le logicien Per Martin-Löf, pour donner raison à Bridges, a développé des systèmes dans lesquels ce genre d'axiomes est automatique (essentiellement pour la justification que j'ai dite : pour prouver ∀y∈Y.∃x∈X.(P(x,y)) on crée une façon de fabriquer x à partir de y), qui échappent au résultat de Diaconescu cité ci-dessus en changeant le rôle de l'égalité, laquelle n'est alors plus la relation fondamentale sur un ensemble mais une donnée additionnelle (cf. le concept de setoïde). En tout cas, il est sûr que l'axiome du choix dénombrable n'entraîne pas le tiers exclu.

Je ne suis pas convaincu par ces arguments en faveur de l'axiome du choix dénombrable ou dépendant. Selon moi, l'intérêt du constructivisme est largement dans son minimalisme, et admettre l'axiome du choix, fût-il dénombrable, va à l'encontre de ce minimalisme. D'ailleurs, même en maths classiques, étudier la théorie des ensembles sans axiome du choix présente un certain intérêt : il serait bizarre de renoncer à cet intérêt en maths constructives. Je renvoie à l'article de Peter Schuster, Countable Choice as a Questionable Uniformity Principle pour une discussion plus détaillée (essentiellement d'ordre philosophique ou fondationnelle), avec laquelle je crois être d'accord, sur les raisons de ne pas admettre l'axiome du choix, même dénombrable, en maths constructives.

Mais il faut être conscient que ce refus de l'axiome du choix même dénombrable va entraîner un certain nombre de complications. Par exemple dans la construction des nombres réels : car si on admet soit le tiers exclu (comme le fait ZF classique) soit l'axiome du choix dénombrable (comme le fait Bridges), les réels de Cauchy (définis par des suites de Cauchy) et les réels de Dedekind (définis par des coupures de Dedekind) coïncident : mais dans le cadre plus général, le deux diffèrent (grosso modo, les réels de Dedekind se comportent plus comme on s'y attend, mais les réels de Cauchy sont plus manipulables informatiquement, par exemple).

On peut d'ailleurs éventuellement introduire des formes encore plus faibles de l'axiome du choix, qui sont automatiquement vraies dans ZF classique et qui sont plus faibles que le choix dénombrable mais suffisent à simplifier nettement l'analyse. Une possibilité de ce genre, proposée par Bridges, Richman & Schuster est l'affirmation que toute suite (Z_n)_n∈ℕ d'ensembles habités, dont au plus un élément n'est pas un singleton [au sens où si m≠n alors Z_m est un singleton ou Z_n en est un] a une fonction de choix.

(Fin de la digression.)

Il faut quand même que je remarque que certaines formes de l'axiome du choix sont bien valables en maths constructives, au moins dans le cadre où je me place. Spécifiquement, il y a deux cas majeurs où le choix est valable :

• Si Y est fini (un concept que je dois définir plus tard, mais disons si Y={1,…,n} avec n un entier naturel), l'axiome du choix vaut : c'est-à-dire que le produit cartésien X₁×⋯×X_n d'un nombre fini d'ensembles habités est habité (la démonstration est par récurrence sur n).

  (Pour dissiper une confusion possible, on ne peut pas affirmer que l'ensemble Y = {U,V} dans la démonstration du théorème de Diaconescu ci-dessus est fini : de façon générale, un ensemble {U,V} énuméré par deux éléments U et V est fini si et seulement si U=V ou bien ¬(U=V).)

• Si chaque Z_i est un singleton, ou, ce qui revient au même dans l'autre présentation, si f:X→Y est bijective (et pas juste surjective), alors l'axiome du choix vaut : le produit cartésien d'une famille quelconque de singletons est habité (et est d'ailleurs un singleton). Ceci s'appelle parfois le principe du choix unique (ou principe du non-choix), et je m'en suis déjà servi un certain nombre de fois (pour dire que la réciproque d'une bijection a un sens) : il est consubstantiel avec le fait d'avoir choisi de représenter les fonctions par des graphes fonctionnels.

  (Ce principe vaut dans n'importe quel topos, il vaut dans la théorie des ensembles IZF ou CZF, mais pas, par exemple, dans le système Coq où il doit être postulé. Le problème si on n'admet pas le principe du choix unique est qu'on ne sait plus très bien ce que devrait être une fonction ; voir cette question MathOverflow pour une discussion.) Toujours est-il que, dans ce billet, j'admets le principe du choix unique sans hésiter (mais parfois en le signalant quand ça me semble intéressant à noter).