David Madore's WebLog: Introduction aux mathématiques constructives : 2. entiers naturels et principes d'omniscience

Ensembles finis, finiment énumérés, etc.

Déjà en maths classiques sans l'axiome du choix (ZF), la notion d'ensemble fini admet un certain nombre de variations (cf. cette question que j'avais posée sur MathOverflow). On se doute bien qu'en maths constructives il va falloir faire encore plus attention !

La notion la plus standard d'ensemble fini est, il me semble, d'être en bijection avec {1,…,n} pour un certain entier naturel n (il vaut évidemment mieux utiliser {0,…,n−1} = {m∈ℕ : m<n} ; mais ça revient au même une fois faite la convention que {1,…,n} désigne l'ensemble vide pour n=0, et je vais préférer {1,…,n} pour ne pas avoir à écrire des −1 partout). C'est la définition que je vais prendre. Le n en question est alors unique (je ne vais pas le prouver mais c'est standard et pas différent des maths classiques) et on peut l'appeler le cardinal [fini] de l'ensemble en question. Les ensembles finis avec cette notion se comportent assez bien comme en maths classiques (mais déjà on va avoir des problèmes en voulant passer à une partie ou à un quotient, cf. ci-dessous). Néanmoins, chacune des quatre notions suivantes peut avoir un intérêt, donc je pense que je peux les donner toutes les quatre, en commençant par celle que je viens d'esquisser :

• Un ensemble fini est, comme je viens de le dire, un ensemble X pour lequel il existe une bijection {1,…,n}→X. (Et je répète que, si n=0, l'ensemble {1,…,n} est vide par convention, i.e., un ensemble vide est fini.)

  On peut alors montrer que n est forcément unique (s'il y a une bijection entre {1,…,n} et {1,…,n′} alors n=n′). On l'appellera le cardinal de l'ensemble fini en question.

  On peut cependant définir cette notion d'ensemble fini sans référence aux entiers naturels, de la manière suivante : une partie finie d'un ensemble X quelconque est un élément du plus petit ensemble de parties de X qui contient ∅ et est stable par réunion disjointe avec un singleton ; et on peut alors définir un ensemble fini comme un ensemble qui est une partie finie de lui-même.

  Pour être parfaitement précis sur ce que signifie le paragraphe précédent, on appelle (temporairement) inductif par réunion disjointe avec un singleton (iprds) un ensemble ℐ⊆𝒫(X) de parties de X tel que ∅∈ℐ, et tel que si A∈ℐ et b∈X vérifient ¬(b∈A) alors (A∪{b})∈ℐ. Une intersection quelconque d'ensembles iprds de parties de X a encore cette propriété (c'est clair). On définit alors l'ensemble des parties finies de X comme l'intersection ℱ := ⋂{ℐ : ℐ est iprds} de tous les ensembles iprds de parties de X, c'est-à-dire, par ce que je viens de dire, comme le plus petit ensemble iprds de parties de X. Et X lui-même est dit fini lorsque X est dans ce ℱ.

  (Esquissons la démonstration de l'équivalence entre l'existence d'une bijection {1,…,n}→X et l'appartenance au plus petit ensemble iprds comme je viens de le dire : dans un sens, il est évident que la réunion d'une partie finie au sens d'être en bijection avec {1,…,n} et d'un singleton est encore une partie finie, donc que les parties finies sont un ensemble iprds, donc elles sont contiennent le plus petit ensemble iprds ; et dans l'autre sens, on montre par récurrence sur n que toute partie en bijection avec {1,…,n} appartient au plus petit ensemble iprds. ∎)

• Un ensemble finiment énuméré ou Kuratowski-fini est un ensemble X pour lequel il existe une surjection {1,…,n}→X, ou, ce qui revient au même (en factorisant cette surjection), que X est en bijection avec un quotient de {1,…,n} (par une relation d'équivalence).

  Concrètement, c'est un ensemble qu'on peut exprimer sous la forme {x₁,…,x_n}, sans demander que les x_i soient distincts (contrairement au cas d'un ensemble fini). On peut aussi définir un ensemble finiment énuméré comme (à bijection près) un quotient d'un ensemble fini par une relation d'équivalence.

  De nouveau, on peut également définir cette notion sans référence aux entiers naturels : une partie finiment énumérée d'un ensemble X quelconque est un élément du plus petit ensemble de parties de X qui contient ∅ et est stable par réunion (pas forcément disjointe cette fois) avec un singleton. On peut aussi les définir comme le plus petit ensemble de parties de X qui contient ∅ et les singletons et est stable par réunion binaire. Et X lui-même est finiment énuméré lorsqu'il est une partie finiment énumérée de lui-même.

• Un ensemble sous-fini est un ensemble qui est (à bijection près) une partie d'un ensemble fini.

  Il revient au même dire que c'est un ensemble X pour lequel il existe une bijection D→X avec D⊆{1,…,n}. Bref, c'est un ensemble en bijection avec un sous-ensemble de {1,…,n}.

• Un ensemble sous-finiment énuméré est une partie d'un ensemble finiment énuméré, ou, ce qui revient au même, un ensemble X pour lequel il existe une surjection D→X avec D⊆{1,…,n}.

  Dans ce que je viens de dire, il n'est pas tout à fait évident que les deux propriétés d'être une partie d'un ensemble finiment énuméré et d'être surjecté par une partie D de {1,…,n} sont équivalentes. Montrons donc cette équivalence. Un sens est facile : si h:{1,…,n}→X′ est surjective et si X⊆X′, on peut appeler D l'image réciproque de X par h et on a alors h:D→X surjective avec D⊆{1,…,n} ; donc « partie d'un ensemble finiment énuméré » implique « surjecté par une partie de {1,…,n} ». Dans l'autre sens, si on suppose l'existence d'une surjection h:D→X avec D⊆{1,…,n}, on peut mettre sur {1,…,n} la relation d'équivalence définie par i∼j lorsque i=j ou i∈D ∧ j∈D ∧ h(i)=h(j), ce qui définit une surjection de {1,…,n} sur X′ := {1,…,n}/∼, donc X′ est finiment énuméré, et l'application de X vers X′ envoyant h(i) pour i∈D sur la classe d'équivalence de i modulo ∼ est bien définie et injective par définition de ∼. (Si on préfère, on doit aussi pouvoir utiliser la relation ≈ définie par i≈j lorsque h(D∩{i}) = h(D∩{j}), je ne sais pas ce qui est le plus simple.) ∎

  Bref, un ensemble sous-finiment énuméré est un ensemble en bijection avec un quotient d'un sous-ensemble de {1,…,n} ou (indifféremment) un sous-ensemble d'un quotient de {1,…,n}.

On peut résumer ces quatre définitions en disant que X est fini, resp. finiment énuméré, resp. sous-fini, resp. sous-finiment énuméré lorsqu'il existe une fonction partielle {1,…,n} ⇢ X qui soit totale bijective, resp. totale surjective, resp. une bijection depuis son domaine de définition, resp. une surjection depuis son domaine de définition.

Je pense que la terminologie que je viens de donner est raisonnablement standard, mais elle n'est nullement universelle. Il y a des gens qui appellent finis ceux que j'ai appelés finiment énumérés, quitte à appeler finis discrets (cf. ci-dessous) ceux que j'ai appelés finis. Il y a des gens qui utilisent le terme de sous-fini pour ceux que j'ai appelés finiment énumérés, parce qu'il faut reconnaître que le concept d'ensemble sous-fini tel que défini ci-dessus n'est pas terriblement intéressant.

On se doute bien que si j'ai pris la peine d'introduire ces quatre termes, c'est que la distinction est pertinente. Il y a donc de grosses surprises quand on vient des maths classiques. Avant de les énoncer, je fais deux remarques faciles (et classiquement triviales) :

Observation : un ensemble fini (ou même finiment énuméré) est soit vide soit habité.

Démonstration : l'hypothèse garantit l'existence d'une surjection h:{1,…,n}→X. Si n=0, rappelons que {1,…,n}=∅ par convention, alors X est vide car l'existence d'un élément dans X implique immédiatement une contradiction à la surjectivité de h. Si n≥1, alors l'image de 1 par h fournit un élément de X. ∎

Observation : un ensemble fini (ou même sous-fini) est discret (rappelons que X est dit discret lorsque ∀x∈X.∀y∈X.(x=y ∨ ¬(x=y))).

Démonstration : comme une bijection préserve la notion d'ensemble discret (puisque l'égalité et la négation de l'égalité sont préservées par bijection), il suffit de remarquer que {1,…,n} ou plus généralement une partie de {1,…,n}, sont discrets ; or ceci résulte du fait que ℕ est discret : on a vu que pour i,j∈ℕ on a (i=j ∨ ¬(i=j)). (Il est trivial qu'une partie d'un ensemble discret est encore discrète.) ∎

Quelques contre-exemples brouwériens

Je donne maintenant deux contre-exemples brouwériens qui sont importants non seulement pour comprendre pourquoi les notions de finitude que j'ai introduites diffèrent en général, mais aussi parce que ce sont des contre-exemples largement réutilisables (d'ailleurs le premier a déjà été évoqué) et qui aident à se faire une idée intuitive de comment peut se comporter un ensemble en maths constructives.

Première surprise : on ne peut pas affirmer qu'une partie d'un ensemble fini soit forcément finie, car :

Proposition : l'affirmation toute partie d'un ensemble fini est finie (i.e., tout ensemble sous-fini est fini) implique la loi du tiers exclu.

Démonstration : On considère le contre-exemple brouwérien donné par la partie {● : p} du singleton 1 = {●}, où p est une valeur de vérité.

Il s'agit bien d'une partie d'un ensemble fini 1 = {●}, donc l'affirmation toute partie d'un ensemble fini est finie implique que {● : p} est fini ; mais d'après une observation faite ci-dessus, ceci entraîne que {● : p} est habité ou bien vide, c'est-à-dire que p est vrai ou bien p est faux : p∨¬p. Comme p était arbitraire, on a prouvé la loi du tiers exclu. ∎

Deuxième surprise : on ne peut pas affirmer qu'un quotient d'un ensemble fini soit forcément fini :

Proposition : l'affirmation tout quotient d'un ensemble fini est fini (i.e., tout ensemble finiment énuméré est fini) implique la loi du tiers exclu.

Démonstration : On considère le contre-exemple brouwérien suivant. Soit p∈Ω une valeur de vérité. On définit une relation d'équivalence R sur {0,1} donnée par {(i,j)∈{0,1}² : (i=j) ∨ p} = {(0,0)} ∪ {(1,1)} ∪ {(0,1) : p} ∪ {(1,0) : p}. Il est facile de vérifier qu'il s'agit bien d'une relation d'équivalence (moralement, on prend deux éléments distincts, et on les identifie si p vaut). Le quotient de {0,1} par cette relation d'équivalence (qui, soit dit en passant, est en bijection avec l'ensemble {U,V} dans la preuve du théorème de Diaconescu donnée à la fin de la partie précédente) est finiment énuméré par définition.

Mais si cet ensemble {0,1}/R est fini, alors d'après une observation faite ci-dessus, il est discret, donc soit la R-classe de 0 et celle de 1 sont égales soit elles ne sont pas égales, ce qui, sur la relation R, implique que (0,1)∈R ou bien ¬((0,1)∈R), c'est-à-dire p∨¬p. Donc l'affirmation tout quotient d'un ensemble fini est fini entraîne le tiers exclu. ∎

Ces mêmes contre-exemples et ces mêmes preuves montrent d'ailleurs un peu plus généralement que si toute partie d'un ensemble fini est finiment énumérée alors le tiers exclu vaut, et que si tout quotient d'un ensemble fini est sous-fini alors le tiers exclu vaut. Donc si deux quelconques des quatre notions de finitude introduites plus haut coïncident, le tiers exclu vaut.

L'idée intuitive qu'il faut se faire, je pense, d'un ensemble fini est que c'est un ensemble dont on connaît tous les éléments et on sait décider si deux d'entre eux coïncident (on verra plus bas que fini équivaut à finiment énuméré et discret) ; un ensemble finiment énuméré est un ensemble dont on connaît tous les éléments, mais sans supposer qu'on sait décider s'ils coïncident ; pour les ensembles sous-finis et sous-finiment énumérés, il faut imaginer qu'on a plutôt des « éléments potentiels » (dont on ne sait pas décider s'ils sont vraiment dans l'ensemble). Et les deux contre-exemples brouwériens que je viens de donner sont vraiment les deux phénomènes à garder à l'esprit s'agissant d'un ensemble en maths constructives : en gros, on ne sait pas forcément décider si un élément potentiel est vraiment un élément, et on ne sait pas forcément décider si deux éléments coïncident.

Quelques propriétés de la finitude

Les ensembles finis sont stables par réunions disjointes binaires et par produits cartésiens binaires, c'est-à-dire que si F et F′ sont finis alors F⊎F′ et F×F′ sont finis. En effet, il suffit de le montrer pour les ensembles {1,…,m}, et c'est essentiellement l'existence de l'addition et de la multiplication sur les entiers naturels. (En revanche, comme on l'a expliqué plus haut, mais ça vaut la peine de le redire encore une fois on ne peut pas affirmer qu'une partie ou un quotient d'un ensemble fini soit fini.)

La stabilité par réunions disjointes (resp. produits cartésiens) binaires entraîne aussi la stabilité par réunions disjointes (resp. produits cartésiens) finis, justement. C'est-à-dire que si F₁,…,F_n sont finis, alors F₁⊎⋯⊎F_n, et F₁×⋯×F_n sont finis : ceci se démontre par récurrence immédiate sur n à partir du cas n=0 qui est évident et du cas successeur qui découle du cas binaire.

Bien sûr, on peut aussi reformuler les affirmations du paragraphe précédent en disant que si I est fini et que chacun des F_i l'est alors ⨄_i∈I F_i est fini (cette réunion disjointe est, si on veut, l'ensemble des couples (i,x) avec x dans la réunion banale des F_i tels que i∈I et x∈F_i). Et il en va de même du produit cartésien ∏_i∈I F_i (qui est l'ensemble des fonctions de I dans la réunion banale des F_i qui prennent en chaque i∈I une valeur appartenant à F_i).

En revanche, si on parle non pas de réunions disjointes mais de réunions de parties d'un ensemble U ambiant, on ne peut pas affirmer que la réunion de deux ensembles finis soit finie (reprendre le contre-exemple brouwérien donné plus haut où la finitude du quotient {0,1}/R implique p∨¬p, et remarquer que {0,1}/R est trivialement la réunion de deux singletons).

Voici un résultat positif plutôt rassurant :

Proposition : Les parties finies d'un ensemble fini X sont les mêmes que ses parties finiment énumérées, et ce sont aussi exactement ses parties décidables (je rappelle qu'une partie E⊆X est dite décidable ou complémentée lorsque ∀x∈X.(x∈E ∨ ¬x∈E)). De plus, elles forment elles-mêmes un ensemble fini ; précisément, l'ensemble des parties finies de {1,…,n} est en bijection avec {0,1}^{1,…,n} via la fonction indicatrice : son cardinal est donc 2ⁿ si n est celui de X.

Démonstration : Il suffit de le montrer pour X={1,…,n}.

Dans un sens, on veut montrer qu'une partie finiment énumérée de {1,…,n} est décidable. Ceci revient à montrer que l'image de n'importe quelle fonction h : {1,…,m} → {1,…,n} est décidable. Pour cela, on procède par récurrence sur m. Le cas m=0 étant trivial, considérons une fonction h : {1,…,m+1} → {1,…,n}. Soit i ∈ {1,…,n}. Comme {1,…,n} est discret (c'est-à-dire que pour tous i,j de {1,…,n} on a (i=j ∨ ¬(i=j))), soit on a i=h(m) soit ¬(i=h(m)). Dans le premier cas, i est bien dans l'image de h. Dans le second cas, i est dans l'image de h si et seulement si i est dans l'image par h de {1,…,m}, et, par l'hypothèse de récurrence (qui assure que cette partie est décidable), ceci est soit vrai soit faux. Donc on a bien montré que tout i est dans l'image de h ou bien n'est pas dans l'image de h, c'est-à-dire que l'image de h est décidable. Ceci conclut la récurrence.

Dans l'autre sens, on veut montrer qu'une partie décidable E de {1,…,n} est finie. On procède par récurrence sur n. Le cas n=0 étant trivial, considérons une partie décidable E de {1,…,n+1}. La partie E′ := E ∩ {1,…,n} est décidable (comme partie d'un ensemble décidable), donc par l'hypothèse de récurrence elle est finie. Comme E est décidable, on a soit n+1 ∈ E soit ¬(n+1 ∈ E). Dans le premier cas, E = E′ ∪ {n+1}, et cette réunion est disjointe, si bien que E est finie. Dans le second cas, E = E′, et de nouveau E est finie. Ceci conclut la récurrence.

Enfin, le fait que les parties décidables de X soient en bijection avec les fonctions X→{0,1} a déjà été signalé. ∎

(Cette preuve aurait probablement été plus claire en utilisant la définition des parties finies de X comme le plus petit ensemble de parties de X contenant le vide et stable par réunion disjointe avec un singleton.)

L'idée intuitive à retenir est que la notion de partie générale d'un ensemble, en maths constructives, est une notion très difficile à gérer, même quand l'ensemble est supposé fini : il y a potentiellement « plein » de parties (d'ailleurs l'hypothèse, que j'ai faite, de l'existence des ensembles de parties, est une hypothèse hautement « imprédicative », qui n'est pas du tout anodine : on peut mettre en doute le fait qu'on ait le droit de collecter quelque chose d'aussi monstrueux pour former un ensemble) ; en revanche, si on se limite aux parties décidables, on a une situation beaucoup plus analogue aux maths classiques (mais évidemment, est-ce vraiment ce qu'on veut ? si on cherche les maths classiques, on sait où les trouver).

❇

Les ensembles finiment énumérés, eux, sont stables par réunions disjointes finies, mais aussi par réunions finies dans un ensemble U ambiant, par quotients, et par produits cartésiens finis.

Si on veut, les ensembles finiment énumérés sont même stables par réunions (disjointes ou dans un ensemble ambiant) indicées par des ensembles eux-mêmes finiment énumérés : c'est-à-dire que si J est finiment énuméré et que chacun des F_i pour i∈J est finiment énuméré, alors ⋃_j∈J F_j (dans un ensemble ambiant U) ou ⨄_j∈J F_j est finiment énuméré. Cette affirmation résulte juste du fait que si J est finiment énuméré, on peut trouver h:I→J surjective avec I fini, et alors ⋃_j∈J F_j = ⋃_i∈I F_h(i), tandis que ⨄_j∈J F_j est un quotient de ⨄_i∈I F_h(i) (par la relation d'équivalence qui identifie les éléments de F_h(i) et les éléments correspondants de F_h(i′) lorsque h(i)=h(i′)), donc on est ramené au cas fini.

En revanche, on ne peut pas affirmer qu'un produit cartésien indicé par un ensemble finiment énuméré d'ensembles finiment énumérés (ou même finis) est finiment énuméré. (Comme je me suis gratté la tête à ce sujet, et que la construction est intéressante pour comprendre les produits cartésiens indicés par des ensembles non supposés discrets, voici un contre-exemple brouwérien illustrant ce fait. Soit p une valeur de vérité, soit U := {x∈{0,1} : (x=0)∨p} et V := {x∈{0,1} : (x=1)∨p} comme dans la preuve du théorème de Diaconescu ; et soit Y = {U, V}, qu'on peut aussi considérer comme le quotient de {0,1} par la relation d'équivalence R = {(i,j)∈{0,1}² : (i=j) ∨ p}, puisque U est la classe de 0 et V celle de 1 pour cette relation d'équivalence. Donc bien sûr Y est finiment énuméré. Maintenant posons F_y={0,1} pour tout y∈Y. Manifestement ils sont tous finis. Le produit cartésien ∏_y∈Y F_y, qui est simplement l'ensemble {0,1}^Y des fonctions Y→{0,1}, peut s'identifier (en relevant de Y à {0,1}) à la partie de ∏_i∈{0,1} F_i = {0,1}^{0,1} formée des fonctions h:{0,1}→{0,1} telles que p ⇒ (h(0)=h(1)). Si cet ensemble est finiment énuméré, en vertu de la proposition vue ci-dessus, il c'est une partie décidable de {0,1}^{0,1}. En regardant notamment la fonction identité {0,1}→{0,1}, la décidabilité de p ⇒ (h(0)=h(1)) est celle de ¬p. Autrement dit, on a ¬p∨¬¬p. Donc l'affirmation un produit cartésien indicé par un ensemble finiment énuméré d'ensembles finis est finiment énuméré implique la loi faible du tiers exclu. ∎) Néanmoins, ce produit cartésien est au moins sous-finiment énuméré (car si h:I→J surjective avec I fini alors ∏_j∈J F_j est une partie de ∏_i∈I F_h(i)).

Proposition : l'ensemble des parties finiment énumérées d'un ensemble finiment énuméré est lui-même finiment énuméré.

Démonstration : si h:X→Y est surjective, le principe de choix fini (qui, on le rappelle, est un théorème, démontré par récurrence) assure que toute partie finiment énumérée de Y est l'image par h d'une partie finiment énumérée de X (en effet, donnés des éléments y(1),…,y(n) de Y, on peut trouver x(1),…,x(n) de X qui aient ceux-ci pour image par h). Ceci montre que l'ensemble des parties finiment énumérées de Y est l'image de l'ensemble des parties finiment énumérées de X par l'application image par h sur les parties. Maintenant, si Y est finiment énuméré, il existe X fini qui le surjecte, et l'ensemble des parties finiment énumérées de X est fini comme on l'a vu plus haut, donc l'ensemble des parties finiment énumérées de Y est finiment énuméré comme image d'un ensemble fini. ∎

Proposition : un ensemble est fini si et seulement si il est à la fois finiment énuméré et discret (rappelons une fois de plus que X est dit discret lorsque ∀x∈X.∀y∈X.(x=y ∨ ¬(x=y))).

Démonstration : Un ensemble fini est trivialement finiment énuméré, et on a déjà observé plus haut qu'il était discret. Il s'agit donc de démontrer la réciproque : que tout ensemble finiment énuméré et discret est fini.

Si h:{1,…,n}→X est surjective, dire que X est discret équivaut à dire que la relation d'équivalence ∼ sur {1,…,n} définie par h(i)=h(j) est décidable (c'est-à-dire soit i∼j soit ¬(i∼j)). Bref, il s'agit de montrer que le quotient d'un ensemble fini — ou disons précisément de {1,…,n} — par une relation d'équivalence décidable est fini.

Mais si ∼ est une relation d'équivalence décidable sur {1,…,n}, chacune des classes d'équivalence est décidable (puisque la relation d'équivalence l'est), et elle est habitée (puisque c'est une classe d'équivalence). On a vu plus haut qu'une partie décidable habitée de ℕ a un plus petit élément. On peut donc choisir donc comme représentant de chaque classe d'équivalence ce plus petit élément.

L'application {1,…,n} → {1,…,n} qui à chaque élément de {1,…,n} associe le plus petit élément de sa classe d'équivalence est, comme on vient de le voir, bien définie, et son image Y est en bijection avec le quotient X = {1,…,n}/∼. Cette image Y est finiment énumérée par construction, mais on a vu qu'une partie finiment énumérée d'un ensemble fini était finie, donc Y est fini, donc X l'est aussi. ∎

En particulier, comme on a déjà observé plus haut que les ensembles sous-finis sont discrets, un ensemble à la fois finiment énuméré et sous-fini est fini (ouf !).

❇

Les ensembles sous-finis sont sans doute moins intéressants et importants que les ensembles finis et les ensembles finiment énumérés. Les ensembles sous-finis sont stables par réunions disjointes finies, ou même sous-finies, et par produits cartésiens finis, ou même indicés par un ensemble finiment énuméré il me semble (mais je vérifie tout ça un peu rapidement et il se peut que je me trompe). Attention, cependant, même si tout ensemble sous-fini est par définition en bijection avec une partie d'un ensemble fini, on ne peut pas affirmer qu'une partie sous-finie d'un ensemble X est forcément une partie d'une partie finie de X (penser au cas où X = p = {● : p} avec p∈Ω : alors X est lui-même une partie sous-finie de X, s'il est une partie d'une partie finie de X, cette partie doit être vide ou habitée, donc p∨¬p).

Je devrais peut-être à ce sujet rappeler la notion d'ensemble sous-terminal : c'est un ensemble dont tous les éléments sont égaux.

Proposition : un ensemble sous-terminal est sous-fini.

Démonstration : soit X un ensemble sous-terminal, et on veut montrer qu'il est sous-fini. Considérons la partie D := {0 : X est habité} = {i∈{0} : ∃x∈X.(⊤)} de {0} (autrement dit, on met l'élément 0 dans D lorsque X est habité, et c'est tout). Maintenant, considérons la fonction h:D→X définie ainsi : si i∈D, alors X est habité, donc il existe x∈X et on peut définir h(i)=x, ce qui a bien un sens parce que tous les éléments de X sont égaux. (Si on préfère, le graphe de h est… l'ensemble D×X tout entier.) Cette fonction h est injective car tous les éléments de D sont égaux, et elle est surjective car si x∈X alors 0∈D et h(0)=x. Donc on a bien établi une bijection entre une partie de {0} et X, ce qui montre que X est sous-fini. ∎

Tant que j'y suis, et pour dissiper une autre fausse idée qu'on pourrait avoir : on ne peut pas affirmer que toute partie sous-terminale, de {0,1}, est une partie d'un singleton de {0,1} (l'ensemble {0,1} n'est pas forcément « flasque »). (Contre-exemple brouwérien : si c'est le cas, soit p une valeur de vérité et considérons la partie {0 : p} ∪ {1 : ¬p} ; il est évident qu'elle est sous-terminale ; néanmoins, si c'est une partie de {0} alors on a ¬¬p, et si c'est une partie de {1} alors on a ¬p, donc si c'est une partie d'un singleton de {0,1} on a ¬p∨¬¬p. Donc l'affirmation que toute partie sous-terminale de {0,1} est une partie d'un singleton de {0,1} implique la loi faible du tiers exclu. ∎)

Quant aux ensembles sous-finiment énumérés, ils sont stables par réunions finies, ou même indicées par un ensemble sous-finiment énuméré, et par produits cartésiens finis, ou ou même indicés par un ensemble finiment énuméré. Je ne sais pas si on peut dire plus.

❇

Bien sûr, les quatre notions discutées ci-dessus ne sont pas les seules notions de finitude qu'on peut introduire qui soient assez naturelles et qui se réduisent à fini dans le cadre de ZFC. Par exemple, on peut définir la notion d'ensemble Dedekind-fini :

• Un ensemble Dedekind-fini est un ensemble X pour lequel toute injection X→X est automatiquement une bijection.

• Un ensemble dual-Dedekind-fini est un ensemble X pour lequel toute surjection X→X est automatiquement une bijection.

J'ai démontré que les ensembles sous-finiment énumérés (et a fortiori les finis, les finiment énumérés et les sous-finis) sont Dedekind-finis. Mais cette notion n'est pas très agréable : on ne peut pas affirmer qu'un quotient ni une partie d'un ensemble Dedekind-fini est Dedekind-finie (cette fois je n'ai pas de contre-exemple brouwérien à proposer, mais des contre-exemples utilisant des topos sont donnés dans cet article). La principale raison de s'intéresser à la Dedekind-finitude est que l'ensemble Ω des valeurs de vérité est Dedekind-fini (en raison du théorème de l'involution de Higgs, démontré ci-dessus, qui affirme que toute injection Ω→Ω est involutive, et en particulier, est bijective).

Je ne sais essentiellement rien sur la notion d'ensemble dual-Dedekind-fini, à part qu'elle est impliquée par « fini » et n'est pas équivalente à celle d'être Dedekind-fini.

On peut bien sûr multiplier les définitions. Mon propos ici n'est pas tellement de le faire mais d'illustrer la manière dont une seule notion en maths classiques peut facilement déboucher sur un labyrinthe de notions en maths constructives : on peut voir ça comme un défaut (la plupart de ces notions sont sans grand intérêt et peuvent être classées comme de simples curiosités académiques), ou comme un avantage (après tout, ce sont plein de problèmes intellectuellement intéressants), mais cela peut être aussi une façon de sélectionner la « bonne » façon de définir la finitude (celle qui marche le mieux même dans un contexte constructif) pour tel ou tel type de problème.

Suites, ensembles de Cantor et de Baire

Une suite à valeurs dans un ensemble X est simplement une fonction ℕ→X (i.e., un élément de X^ℕ). On note généralement, par la notation des familles, (u_n)_n∈ℕ une suite, et u_n son n-ième terme.

La sorte la plus simple de suite sont les suites binaires, c'est-à-dire les suites à valeur dans 2 := {0,1} (ensemble fini à deux éléments que je noterai ‘0’ et ‘1’). L'ensemble 2^ℕ des suites binaires s'appelle souvent l'ensemble de Cantor (parce qu'on peut l'identifier assez naturellement à l'ensemble des nombres réels de [0,1] ayant une écriture ternaire formée uniquement des chiffres 0 et 2, ou ensemble triadique de Cantor, mais pour l'instant je n'ai pas dit ce qu'est un nombre réel). On peut aussi l'identifier à l'ensemble des parties décidables (i.e., complémentées) de ℕ, via la fonction indicatrice (la partie étant l'ensemble des points où la suite binaire vaut 1, et la suite étant définie comme valant 1 sur la partie et 0 sur son complémentaire, ce qui définit bien une suite justement parce que la partie est supposée décidable).

Un petit peu plus compliqué que les suites binaires on a les suites d'entiers naturels : l'ensemble ℕ^ℕ de ces suites est souvent appelé l'espace de Baire.

Deux suites sont égales, bien sûr, lorsque chacun de leurs termes sont égaux : u=v signifie ∀n∈ℕ.(u_n=v_n). Maintenant, si on parle de suites binaires ou de suites d'entiers naturels, deux termes donnés de la suite sont égaux ou ne sont pas égaux ({0,1}=:2 et ℕ sont des ensembles discrets) : on peut écrire u_n≠v_n (un symbole que je réserve pour les ensembles discrets, justement) ou u_n⋕v_n (le symbole d'une relation de discernement, un concept expliqué plus haut) pour ¬(u_n=v_n). Il est alors tentant de définir :

Définition : On dit que deux suites binaires, ou d'entiers naturels, sont discernées, et on note u⋕v lorsqu'il existe un terme où ces suites diffèrent : ∃n∈ℕ.(u_n≠v_n). La relation ‘⋕’ ainsi définie sur l'ensemble de Cantor ou l'espace de Baire est appelée sa relation de discernement standard (et c'est celle qu'on utilise par défaut quand on parle de discernement sur ces espaces).

(Je rappelle que j'utilise le terme de discerné et de discernement pour rendre ce qui se dit en anglais par apart et apartness. Je rappelle aussi que certains auteurs utilisent le symbole ‘≠’ pour ce que je note ‘⋕’, ce que je n'accepte de faire que pour un ensemble discret.)

Il est facile de vérifier qu'il s'agit bien d'une relation de discernement, c'est-à-dire irréflexive, symétrique et cotransitive : les deux premières propriétés sont triviales, et pour la troisième il s'agit de montrer que si u,v,w sont trois suites (à valeurs dans {0,1} ou ℕ ou plus généralement un ensemble discret) et qu'on a u⋕w, alors soit u⋕v soit v⋕w : or l'hypothèse u⋕w assure l'existence d'un n tel que u_n≠w_n, et pour ce n précis, puisque ‘≠’ est elle-même un discernement (sur l'ensemble discret où les suites prennent leurs valeurs), on a soit u_n≠v_n soit v_n≠w_n, ce qui donne la conclusion annoncée.

Classiquement, bien sûr, u⋕v signifie simplement ¬(u=v), et classiquement on a soit u=v soit u⋕v. Mais constructivement, que faut-il penser du rapport entre les énoncés u⋕v et u=v (et leurs négations) ?

La première chose qu'on peut remarquer, c'est que le discernement standard ‘⋕’ qu'on vient de définir est un discernement serré, c'est-à-dire que ¬(u⋕v) signifie exactement u=v (la partie intéressante est le implique, parce que l'implication réciproque est juste l'irréflexivité du discernement). En effet, ¬∃n∈ℕ.(u_n≠v_n) signifie ∀n∈ℕ.¬(u_n≠v_n) par pure logique, et ¬(u_n≠v_n) est synonyme de u_n=v_n car on est à valeurs dans un ensemble discret (en particulier, (¬¬)-séparé si on veut utiliser cette terminologie), bref, on tombe sur ∀n∈ℕ.(u_n=v_n) comme annoncé, et ¬(u⋕v) signifie bien u=v.

Donc, sur l'ensemble de Cantor ou l'espace de Baire, la négation de u⋕v équivaut à u=v. Mais dans l'autre sens ? Quel est le rapport entre u⋕v et la négation de u=v ?

Divers principes d'omniscience

C'est là qu'interviennent les postulats standards au nom assez ridicule de principes d'omniscience. Je les énonce pour une une suite binaire et pour la comparaison la suite identiquement nulle (notée 0), mais il y a toutes sortes de reformulations évidentes avec l'ensemble ℕ^ℕ des suites d'entiers à la place de celui 2^ℕ des suites binaires (il s'agit essentiellement juste de remplacer =1 par ≠0 partout), et/ou en comparant deux suites entre elles au lieu d'une suite à zéro :

• Le principe limité d'omniscience ou LPO (limited principle of omniscience) affirme qu'une suite binaire est soit nulle soit a un terme non-nul : ∀u∈2^ℕ.(u=0 ∨ u⋕0), c'est-à-dire ∀u∈2^ℕ.((∀n∈ℕ.(u_n=0)) ∨ (∃n∈ℕ.(u_n=1))).

  Ce principe LPO équivaut trivialement à la conjonction des deux principes qui suivent.

• Le principe limité faible d'omniscience ou WLPO (weak limited principle of omniscience) affirme qu'une suite binaire est soit nulle soit n'est pas nulle : ∀u∈2^ℕ.(u=0 ∨ ¬(u=0)), c'est-à-dire ∀u∈2^ℕ.((∀n∈ℕ.(u_n=0)) ∨ ¬(∀n∈ℕ.(u_n=0))).

  Cela revient à affirmer que l'ensemble de Cantor (ou l'espace de Baire, c'est équivalent) est un ensemble discret (au sens où deux éléments sont soit égaux soit non-égaux).

• Le principe de Markov ou MP (Markov's principle, nommé d'après Andrej Markov fils) affirme qu'une suite binaire qui n'est pas nulle a un terme non-nul : ∀u∈2^ℕ.((¬(u=0)) ⇒ (u⋕0)), c'est-à-dire ∀u∈2^ℕ.((¬(∀n∈ℕ.(u_n=0))) ⇒ (∃n∈ℕ.(u_n=1))).

  Cela revient à affirmer que le discernement standard ‘⋕’ sur l'ensemble de Cantor (ou l'espace de Baire, c'est équivalent) est la négation de l'égalité.

Le principe limité d'omniscience est juste (équivalent à) la conjonction du principe limité faible d'omniscience et du principe de Markov. Mais comme il est sans doute plus important que chacun des deux séparément, il est utile d'avoir un nom pour lui.

(Pour ceux qui se posent la question, le principe d'omniscience tout court serait la loi du tiers exclu, mais ce terme n'est plus utilisé : on écrit LEM pour law of excluded middle et pas PO. Le terme d'omniscience vient du fait que, pour Brouwer, l'affirmation que P est vrai ou P est faux se comprenait comme on sait que P est vrai ou on sait que P est faux, et affirmer ça pour tout P est une forme d'omniscience, tandis que l'affirmer pour tout P de la forme la suite <machin> prend une valeur non-nulle est une forme limitée d'omniscience. Mais on n'est — heureusement ! — pas obligé d'adhérer à la confusion malencontreusement entretenue par Brouwer entre P est vrai et on sait que P est vrai pour faire des mathématiques constructives ou pour s'y intéresser !)

Aucun de ces principes n'est valable constructivement au sens où il serait démontrable (dans le cadre dans lequel je me suis placé), ni admissible au sens où il serait « souhaitable » d'en faire un axiome : ce sont des tabous constructifs et ils sont très importants parce qu'ils servent à jauger la non-constructivité de différents énoncés et à produire des contre-exemples brouwériens comme je vais l'expliquer.

Le principe de Markov est « moins tabou » que les autres, si j'ose dire, et il a été admis par l'école russe du constructivisme (que Bridges & Richman appellent RUSS) qui avait pour intérêt l'étude de calculabilité à travers la logique intuitionniste. L'explication intuitive de pourquoi le principe de Markov fait sens dans ce contexte (mais je répète qu'il ne s'agit pas d'une preuve, il n'y en a pas, simplement d'une justification de pourquoi on pourrait vouloir admettre le principe de Markov dans le cadre d'une étude de la calculabilité) est que si on a un dispositif qui produit une suite de 0 et de 1 et qu'on sait qu'il est impossible qu'il ne produise que des 0, il y a un moyen « effectif » de trouver un 1 qui consiste simplement à… attendre qu'un 1 soit produit. Je renvoie à l'excellent article très pédagogique d'Andrej Bauer, First Steps in Synthetic Computability Theory (2006) pour une introduction à la calculabilité synthétique (dans un cadre dans lequel le principe de Markov est pris pour axiome, 3.18 dans l'article cité). (Le principe de Markov semble avoir un rapport fort avec l'opérateur μ de Kleene permettant des recherches non bornées en calculabilité classique ; mais j'avoue que le rapport exact m'échappe ; néanmoins, je peux signaler que le principe de Markov est valable dans le topos effectif, essentiellement pour la raison que je viens d'esquisser.)

Le principle limité d'omniscience, et même le principe limité faible d'omniscience, sont en tout cas des tabous en mathématiques constructives. Pourquoi leur donner un nom, alors ? Essentiellement parce qu'ils permettent des contre-exemples brouwériens : si on découvre qu'un certain énoncé P implique LPO (ce qui est une situation assez courante), on saura qu'on ne doit pas chercher à démontrer P constructivement. La situation est la même qu'avec la loi du tiers exclu (principe d'omniscience tout court), mais le principe limité d'omniscience est, comme son nom l'indique, plus limité (et a fortiori le principe limité faible d'omniscience), donc il y a plus de P qu'on pourra rejeter constructivement au motif qu'ils impliquent un principe inadmissible.

(Bien sûr, pour que ce raisonnement permette de conclure que P est effectivement indémontrable, il faut avoir préalablement vérifié que le principe limité, même faible, d'omniscience, n'est pas démontrable constructivement, ce que Brouwer n'avait pas fait et n'avait pas les moyens de faire ; cela se fait aisément en construisant un topos approprié mais je ne vais pas en parler ici. La situation est analogue à la situation dans ZF classique des variantes plus faibles de l'axiome du choix avant qu'on sache que l'axiome du choix n'est pas démontrable : le fait qu'un énoncé implique une variante faible de l'axiome du choix suggérait au moins que cet énoncé n'était pas démontrable sans choix.)

On peut évoquer dans ce contexte le terme de mathématiques constructives “à rebours” (pour une introduction, voir par exemple ce texte, qui a cependant l'inconvénient d'admettre l'axiome du choix dépendant ; ou bien celui-ci, qui fait sans mais est plus limité dans son étude). L'idée général est de chercher à dégager les implications précises entre différents principes de référence constructivement inadmissibles (mais plus faibles que la loi du tiers exclu), et voir quels énoncés sont équivalents à quels principes de référence. Par exemple, j'ai montré plus haut dans ce texte que divers énoncés (comme une partie d'une ensemble fini est finie) sont équivalents à la loi du tiers exclu : on peut dire qu'il s'agit d'une forme de mathématiques à rebours.

Outre LPO, WLPO et MP, on peut aussi mentionner les principes suivants, également importants en mathématiques constructives « à rebours » et occasionnellement utiles pour s'assurer qu'un énoncé n'est pas démontrable constructivement : je les énonce avec deux suites u et v mais on peut préférer le faire avec les termes pairs et impairs d'une même suite :

• Le moindre principe limité d'omniscience ou LLPO (lesser limited principle of omniscience) affirme à propos de deux suites d'entiers que s'il n'est pas vrai que toutes les deux ont un terme non-nul, alors l'une des deux est nulle : ∀u∈2^ℕ.∀v∈2^ℕ.((¬((u⋕0) ∧ (v⋕0))) ⇒ (u=0) ∨ (v=0)) (on rappelle à toutes fins utiles que ¬(u⋕0) équivaut à u=0), c'est-à-dire ∀u∈2^ℕ.∀v∈2^ℕ.((¬((∃n∈ℕ.(u_n=1)) ∧ (∃n∈ℕ.(v_n=1)))) ⇒ (∀n∈ℕ.(u_n=0)) ∨ (∀n∈ℕ.(v_n=0))).

• Le moindre principe limité faible d'omniscience ou WLLPO (weak lesser limited principle of omniscience — terme moins standard, on trouve aussi ce principe sous le nom de lesser limited principle of existence, LLPE, ou bien de disjunctive Markov principle, MP^∨) affirme à propos de deux suites d'entiers que s'il n'est pas vrai que toutes les deux sont nulles, alors l'une des deux n'est pas nulle : ∀u∈2^ℕ.∀v∈2^ℕ.((¬((u=0) ∧ (v=0))) ⇒ ((¬(u=0)) ∨ (¬(v=0)))), c'est-à-dire ∀u∈2^ℕ.∀v∈2^ℕ.((¬((∀n∈ℕ.(u_n=0)) ∧ (∀n∈ℕ.(v_n=0)))) ⇒ ((¬(∀n∈ℕ.(u_n=0))) ∨ (¬(∀n∈ℕ.(v_n=0))))).

(Avec les termes pairs et impairs d'une même suite, WLLPO s'énonce sous la forme : si une suite binaire [ou d'entiers] n'est pas nulle, alors soit la suite de ses termes pairs n'est pas nulle soit la suite de ses termes impairs n'est pas nulle, ce qui est peut-être plus parlant. Mais pour LLPO il faut modifier un peu les choses : si une suite binaire a au plus un 1 [au sens où si deux termes valent 1 alors leurs indices sont égaux] alors soit la suite de ses termes pairs est nulle soit la suite de ses termes impairs est nulle.)

Ces principes admettent de nombreuses reformulations ou affirmations équivalentes. Par exemple :

Observation : WLLPO équivaut à l'affirmation que la non-égalité est cotransitive (ou ce qui revient au même, est un discernement) : ∀x∈2^ℕ.∀y∈2^ℕ.∀z∈2^ℕ.((¬(x=z)) ⇒ ((¬(x=y)) ∨ (¬(y=z)))).

Démonstration : pour démontrer que WLLPO implique (¬(x=z)) ⇒ ((¬(x=y)) ∨ (¬(y=z))), on peut supposer sans perte de généralité que y=0 (quitte à ajouter modulo 2 la suite y aux suites x et z) ; or si on a ¬(x=z), on a certainement ¬((x=0) ∧ (z=0)), qui d'après WLLPO entraîne la conclusion souhaitée (¬(x=0)) ∨ (¬(z=0)).

Réciproquement, en supposant la cotransitivité de la non-égalité, si on a (¬((u=0)∧(v=0))), cela revient simplement à ¬(w=0) où w(n)=max(u(n),v(n)), et la cotransitivité permet d'affirmer que soit ¬(u=0) soit ¬(w=u) et ce dernier entraîne ¬(v=0) puisque w=u lorsque v=0. ∎

Pour ce qui est des implications entre les principes que j'ai évoqués, on a :

LEM (le tiers exclu) ⇒ LPO ⇒ WLPO ⇒ LLPO ⇒ WLLPO ⇒ ⊤ (énoncé tautologiquement vrai),
et LPO ⇒ MP ⇒ WLLPO,

et aucune de ces implications n'est réversible (au sens où l'implication réciproque serait prouvable ; j'ai mis ⇒⊤ à la fin pour que l'affirmation aucune de ces implications n'est réversible inclue notamment l'affirmation que même WLLPO n'est pas constructivement prouvable). Je ne peux pas montrer l'indémontrabilité des réciproques (ceci nécessite de construire des modèles parfois assez subtils), mais les implications elles-mêmes ne sont pas très difficiles (quoique pas forcément complètement évidentes non plus). Montrons les plus intéressantes :

Proposition : WLPO implique LLPO.

Démonstration : supposons WLPO vrai : le but est de montrer LLPO. Pour cela, supposons que u et v soient deux suites binaires telles que ¬((u⋕0) ∧ (v⋕0)) (i.e., il n'est pas vrai que toutes les deux ont un terme non nul), et on cherche à montrer que (u=0) ∨ (v=0) (i.e., l'une des deux est nulle).

D'après WLPO appliqué à u, on a soit u=0 soit ¬(u=0) ; et de même pour v on a soit v=0 soit ¬(v=0). Dans trois des quatre cas, on a la conclusion (u=0) ∨ (v=0) souhaitée.

Reste le cas où ¬(u=0) ∧ ¬(v=0), c'est-à-dire ¬¬(u⋕0) ∧ ¬¬(v⋕0), ce qui est pareil que ¬¬((u⋕0) ∧ (v⋕0)), et ce qui contredit l'hypothèse ¬((u⋕0) ∧ (v⋕0)) qu'on a faite : ce cas est donc exclu, et on a bien prouvé (u=0) ∨ (v=0). ∎

Proposition : LLPO implique WLLPO.

Démonstration : supposons LLPO vrai : le but est de montrer WLLPO. Pour cela, supposons que u et v soient deux suites binaires telles que ¬((u=0) ∧ (v=0)) (i.e., il n'est pas vrai que toutes les deux sont nulles), et on cherche à montrer que (¬(u=0)) ∨ (¬(v=0)) (i.e., l'une des deux n'est pas nulle).

Appelons a la suite binaire dont le n-ième terme vaut 1 lorsque u(n)=1 et v(n)=0, et que pour tout k<n on a u(k)=0 et v(k)=0, et 0 sinon : ceci définit bien une suite binaire (le sinon a un sens) car u(n)=1 ∧ v(n)=0 ∧ ∀k<n.(u(k)=0) ∧ ∀k<n.(v(k)=0) est une valeur de vérité décidable (soit elle est vraie soit sa négation l'est) car chaque terme de la conjonction l'est (pour pour les ∀k<n cela résulte d'une récurrence sur n).

Appelons symétriquement b la suite binaire dont le n-ième terme vaut 1 lorsque u(n)=0 et v(n)=1 et que pour tout k<n on a u(k)=0 et v(k)=0, et 0 sinon.

Il est clair sur la définition que si a(n)=1 alors b est identiquement nulle, et si b(n)=1 alors a est identiquement nulle : on a donc ¬((a⋕0) ∧ (b⋕0)) (i.e., il n'est pas vrai que a et b toutes les deux ont un terme non nul).

Alors LLPO permet de conclure que (a=0) ∨ (b=0). Dans le cas où a=0, si on suppose v=0 on a aussi u=0 (par récurrence), ce qui contredit l'hypothèse faite que ¬((u=0) ∧ (v=0)) : c'est une absurdité, et ceci montre que ¬(v=0) (toujours dans le cas où a=0). De même, dans le cas où b=0, on a ¬(u=0). Ainsi, on a (¬(u=0)) ∨ (¬(v=0)), ce qu'on voulait. ∎

Comme autre principe dans le même genre, je pourrais aussi mentionner le principe de Markov faible ou WMP (weak Markov principle) qui affirme que si u est une suite binaire telle que pour toute suite binaire w on ait soit ¬(w=0) soit ¬(w=u), alors en fait on a u⋕0. Autrement dit, ∀u∈2^ℕ.((∀w∈2^ℕ.((¬(w=0)) ∨ (¬(w=u)))) ⇒ (u⋕0)) c'est-à-dire ∀u∈2^ℕ.((∀w∈2^ℕ.((¬∀n∈ℕ.(w_n=0)) ∨ (¬∀n∈ℕ.(w_n=u_n)))) ⇒ (∃n∈ℕ.(u_n=1))). Lui non plus n'est pas prouvable constructivement. On peut vérifier que MP est équivalent à la conjonction de WLLPO et de WMP.