Je suis un peu débordé en ce moment par la préparation de deux cours[#] qui commencent dans deux semaines et dont je n'ai pour l'instant que des notes très éparses et inachevées, d'autant plus que j'enseigne autre chose en ce moment. Mais pendant la préparation d'un de ces cours, je suis tombé sur une difficulté mathématique au sujet de laquelle j'aimerais l'avis de mes lecteurs mathématiciens (il doit bien y en avoir) ou amateurs de mathématiques : ce n'est pas que je ne sache pas démontrer quelque chose, mais que je m'étonne de la façon dont je le démontre, et je trouve qu'il y a quelque chose de surprenant dans toute l'histoire. Bref, je vais commenter les ressemblances et différences entre quelques énoncés apparemment très semblables et surtout différentes démonstrations des énoncés en question.
[#] L'un de ces cours
concerne la théorie des jeux ; ou plutôt les
théories des jeux, parce qu'il y a plusieurs
domaines que leurs spécialistes
appellent théorie des jeux
, selon le type de jeux étudiés, et
dont l'intersection est relativement faible : pensez à celle (que je
ne sais pas nommer plus précisément) qui cherche
des équilibres
de Nash et celle (en gros,
la théorie
combinatoire des jeux) qui cherche à calculer
des valeurs
de Sprague-Grundy, par exemple, chacune a tendance à se définir
comme « la » théorie des jeux, et d'ailleurs ça m'énerve, en tout cas
je voudrais parler des deux et de quelques autres
encore. Mes
notes en cours d'écriture sont ici. L'autre cours concerne les
courbes algébriques, pour lequel il va s'agir de remanier profondément
un cours de géométrie algébrique
(anciennes
notes ici) que je donnais déjà.
Voici quatre énoncés mathématiques très simples, en théorie élémentaire des ensembles, que je pourrais regrouper sous le label général de théorèmes de points fixes, et que je vais appeler successivement (P), (P$), (F) et (F$) :
(P) Soit X un ensemble : on note 𝒫(X) son ensemble des parties. Soit Ψ:𝒫(X)→𝒫(X) une application vérifiant les deux propriétés suivantes : (i) Ψ est progressive, c'est-à-dire que Ψ(A)⊇A pour tout A∈𝒫(X), et (ii) Ψ est croissante, c'est-à-dire que si A⊇B alors Ψ(A)⊇Ψ(B). Alors il existe un plus petit A∈𝒫(X) tel que Ψ(A)=A (c'est-à-dire un A tel que Ψ(A)=A et que si A′ vérifie aussi Ψ(A′)=A′ alors A⊆A′).
(P$) [Exactement le même énoncé que (P) sans supposer (i).] Soit X un ensemble : on note 𝒫(X) son ensemble des parties. Soit Ψ:𝒫(X)→𝒫(X) une application vérifiant la propriété suivante : Ψ est croissante, c'est-à-dire que si A⊇B alors Ψ(A)⊇Ψ(B). Alors il existe un plus petit A∈𝒫(X) tel que Ψ(A)=A. [Un peu mieux : il existe un plus petit A tel que Ψ(A)⊆A, et ce A vérifie Ψ(A)=A.]
Pour les deux énoncés suivants, j'ai besoin de rappeler la notion de fonction partielle : si X et Z sont deux ensembles, une fonction partielle X⇢Z est une fonction définie sur une partie de X et à valeurs dans Z ; on peut aussi la voir comme une partie de X×Z (à savoir, le graphe de la fonction) qui soit fonctionnelle au sens où si elle contient à la fois (x,z₁) et (x,z₂) pour le même x∈X alors forcément z₁=z₂. La relation f⊇g entre fonctions partielles signifie alors que la fonction f prolonge la fonction g (i.e., que f est définie partout où g l'est, et qu'alors leurs valeurs coïncident).
(F) [Exactement le même énoncé que (P) avec des fonctions partielles X⇢Z au lieu de parties de X.] Soient X et Z deux ensembles : on note 𝒟 l'ensemble des fonctions partielles X⇢Z. Soit Ψ:𝒟→𝒟 une application vérifiant les deux propriétés suivantes : (i) Ψ est progressive, c'est-à-dire que Ψ(f)⊇f pour tout f∈𝒟, et (ii) Ψ est croissante, c'est-à-dire que si f⊇g alors Ψ(f)⊇Ψ(g). Alors il existe une plus petite f∈𝒟 telle que Ψ(f)=f (c'est-à-dire un f tel que Ψ(f)=f et que si f′ vérifie aussi Ψ(f′)=f′ alors f⊆f′). [Précision : on me fait remarquer à juste titre que cet énoncé est en fait totalement creux (cf. la
mise à jourci-dessous).](F$) [Exactement le même énoncé que (F) sans supposer (i), donc exactement le même que (P$) avec des fonctions partielles au lieu de parties.] Soient X et Z deux ensembles : on note 𝒟 l'ensemble des fonctions partielles X⇢Z. Soit Ψ:𝒟→𝒟 une application vérifiant la propriété suivante : Ψ est croissante, c'est-à-dire que si f⊇g alors Ψ(f)⊇Ψ(g). Alors il existe une plus petite f∈𝒟 telle que Ψ(f)=f. [Un peu mieux : il existe un plus petit f tel que Ψ(f)⊆f, et ce f vérifie Ψ(f)=f.]
(Nomenclature : j'appelle (P) et (P$) les énoncés sur les Parties,
(F) et (F$) ceux sur les Fonctions partielles, et (P$) et (F$) les
énoncés qui vous en donnent plus pour votre argent.) J'espère que
j'ai écrit ces énoncés de façon à ce qu'il n'y ait pas le moindre
doute sur leur signification formelle. L'objet dont chacun de ces
énoncés affirme l'existence peut être qualifié de plus petit point
fixe
de Ψ.
Commentaires : Le sens intuitif de ces résultats
est quelque chose comme le suivant : on a une opération Ψ
qui, pour prendre l'exemple de l'énoncé (F), prend une
fonction f et l'étend en une fonction peut-être définie sur
un peu plus de points, et par ailleurs, Ψ possède une
propriété de cohérence, à savoir que si on étend f, on
étend aussi le résultat de l'opération Ψ(f) ;
alors il existe une « clôture du vide » pour l'opération Ψ,
c'est-à-dire qu'en partant de rien, l'opération Ψ vous
permet d'arriver à une certaine fonction f à partir de
laquelle l'opération Ψ ne la fait plus grandir. Pour
donner un exemple d'application de (P$), considérer
l'ensemble X=ℕ des entiers naturels, et
l'opération Ψ qui à un ensemble A de naturels
associe l'ensemble formé des entiers 2, 3 et tous les produits de deux
éléments de A : le plus petit point fixe sera alors
l'ensemble de tous les entiers qu'on peut fabriquer en multipliant 2
et 3 autant qu'on veut ensemble (à savoir l'ensemble des
2i·3j avec au moins un
de i et j non-nul, mais peu importe) ; plus
généralement, (P) ou (P$) peut servir à montrer l'existence de toutes
sortes de « clôtures » sous des opérations variées. Généralement
parlant, le concept
de plus
petit point fixe
(ou de point fixe en général)
apparaît très
souvent en mathématiques, et il existe tout
un labyrinthe — mais je crois
vraiment que les énoncés que j'ai cités ci-dessus sont parmi les plus
naturels.
Il est complètement évident que (P$)⇒(P) (parce qu'on suppose
quelque chose de plus fort dans (P) pour arriver à la même conclusion)
et de même que (F$)⇒(F). Il est aussi facile de voir que (F)⇒(P) et
(F$)⇒(P$) grâce à l'« astuce » (si on peut l'appeler comme ça…)
consistant à prendre pour Z un singleton (:=ensemble ayant
un seul élément), de sorte qu'une fonction
partielle X⇢Z est essentiellement la même chose
qu'une partie de X (à savoir la partie sur laquelle la
fonction est définie). Du coup, (F$) est assurément le résultat le
plus fort des quatre. (Les remarques que j'ai introduites par un
peu mieux
sont encore plus fortes que (P$) et (F$), on pourrait
les appeler (P€) et (F€), mais en fait elles ne m'intéressent pas
tellement en tant que telles : c'est juste que je ne sais pas
démontrer (P$) ou (F$) sans obtenir directement ces résultats plus
forts, et par ailleurs ils aident vaguement à comprendre comment les
choses se passent.)
Mais si je prends la peine d'énoncer quatre résultats différents, c'est que le résultat (P) est extrêmement facile à démontrer :
Démonstration de (P) : Il existe des A tels que Ψ(A)=A (puisque l'ensemble X tout entier en est un). Soit C l'intersection de tous ces A. Alors C est inclus dans chacun de ces A, donc par (ii), Ψ(C) est inclus dans chacun des Ψ(A)=A ; du coup, Ψ(C) est inclus dans l'intersection des A en question, qui est justement C, et comme (i) donne l'inclusion dans l'autre sens, on a Ψ(C)=C. La construction même de C fait qu'il est bien le plus petit.
Je pense que n'importe quel mathématicien non seulement sait
démontrer le résultat (P) à la lecture, mais tombera de plus
essentiellement sur la démonstration que je viens de dire. Dans
n'importe quel livre de maths, la démonstration serait simplement
condensée en quelque chose comme l'intersection des points fixes
de Ψ est elle-même un point fixe de Ψ comme on
le vérifie facilement, et c'est donc le plus petit pour
l'inclusion
.
Bon, autant vous en donner un peu plus pour votre argent et démontrer (P$). Je vais le faire de deux façons différentes :
Démonstration de (P$) en utilisant (P) : Je suppose que Ψ seulement croissante (i.e., vérifiant (ii)), et j'appelle Ψ₁(A) := A ∪ Ψ(A). Alors Ψ₁ vérifie (i) et (ii), donc par (P), il existe un plus petit A tel que Ψ₁(A)=A, ce qui signifie exactement Ψ(A)⊆A. Comme du coup (ii) donne Ψ(Ψ(A))⊆Ψ(A), le fait que A soit le plus petit à vérifier Ψ(A′)⊆A′ garantit A⊆Ψ(A), et on a bien Ψ(A)=A (et comme tout A′ qui vérifie Ψ(A′)=A′ vérifie en particulier Ψ(A′)⊆A′, il est bien inclus dans A, qui est donc le plus petit à vérifier Ψ(A′)=A′).
Démonstration directe de (P$) : Il existe des A tels que Ψ(A)⊆A (puisque l'ensemble X tout entier en est un). Soit C l'intersection de tous ces A. Alors C est inclus dans chacun de ces A, donc par croissance, Ψ(C) est inclus dans chacun des Ψ(A)⊆A ; du coup, Ψ(C) est inclus dans l'intersection des A en question, qui est justement C, ce qui prouve Ψ(C)⊆C. Par croissance, on a aussi Ψ(Ψ(C))⊆Ψ(C). Du coup, Ψ(C) est l'un des A qu'on a intersectés pour former C, ce qui montre Ψ(C)⊇C, et donc Ψ(C)=C. La construction même de C fait qu'il est le plus petit A′ tel que Ψ(A′)⊆A′, et comme tout A′ qui vérifie Ψ(A′)=A′ vérifie en particulier Ψ(A′)⊆A′, il est bien inclus dans C, qui est donc le plus petit à vérifier Ψ(A′)=A′.
Ça reste très simple même si je trouve ça un chouïa moins transparent. Mais là où les choses sont bizarres, c'est quand on considère (F) et (F$). C'est ici que j'invite mes lecteurs mathématiciens à faire une pause pour se demander comment ils démontreraient ces énoncés, parce que je serais vraiment curieux de savoir à quoi ils penseront spontanément. Je n'arrive pas à décider s'il y a une vraie difficulté ou pas : vue la tête de l'énoncé et vue les démonstrations que j'ai données de (P) et (P$), on se dit que (F) et (F$) ne doivent pas être difficiles. Mais l'idée qu'on a envie d'essayer en premier est sans doute de prendre l'intersection de toutes les fonctions partielles f telles que Ψ(f)⊆f, et elle se heurte à l'obstacle qu'il n'est pas évident a priori qu'il existe un tel f (i.e., qui soit une fonction partielle) ; ou alors, on peut être tenté de prendre l'intersection de toutes les parties A de X×Z telles que Ψ(A)⊆A (en prolongeant un peu intelligemment Ψ de 𝒟 à 𝒫(X×Z)), mais alors il n'est pas du tout évident que cette intersection soit une fonction. Non, vraiment, réfléchissez-y avant de lire la suite !
Voici maintenant une démonstration de (F$), que je trouve presque hallucinante, même s'il faut admettre qu'elle a une certaine beauté :
Démonstration de (F$) :
Montrons d'abord que si il existe une fonction partielle f∈𝒟 telle que Ψ(f)=f, ou même simplement Ψ(f)⊆f, alors il en existe une plus petite. Pour cela, il suffit de considérer l'intersection h de toutes les f telles que Ψ(f)⊆f (considérées comme des parties de X×Z) : dès lors qu'il existe au moins un f∈𝒟 tel que Ψ(f)⊆f, cette intersection h est bien définie et est bien un élément de 𝒟. Si Ψ(f)⊆f alors h⊆f (puisque h est l'intersection des f), donc Ψ(h)⊆Ψ(f) (par croissance de Ψ), donc Ψ(h)⊆f (par transitivité), et comme ceci est vrai pour tous les f dont l'intersection est h, on a finalement Ψ(h)⊆h ; mais la croissance de Ψ donne alors aussi Ψ(Ψ(h))⊆Ψ(h), et du coup Ψ(h) est l'une des f qu'on a intersectées pour former h, et on a ainsi h⊆Ψ(h) ; bref, Ψ(h)=h, et h est à la fois le plus petit élément f∈𝒟 vérifiant Ψ(f)⊆f (de par sa construction) et le plus petit vérifiant Ψ(f)=f (puisqu'il vérifie cette propriété plus forte).
Reste à montrer qu'il existe bien une fonction partielle f telle que Ψ(f)=f, ou même simplement Ψ(f)⊆f. Pour cela, on introduit l'ensemble ℰ des f∈𝒟 qui vérifient Ψ(f)⊇f (inclusion dans le sens opposé du précédent !). Notons que ℰ n'est pas vide puisque ∅∈ℰ (où ∅ est la fonction vide, définie nulle part).
Soit maintenant 𝔐 l'ensemble des applications (totales !) T:ℰ→ℰ qui vérifient (i) T(f)⊇f pour tout f∈ℰ et (ii) si f⊇g alors T(f)⊇T(g). Ainsi idℰ∈𝔐 (trivialement) et Ψ∈𝔐 (par définition de ℰ et par croissance de Ψ) ; et si T,T′∈𝔐 on a T′∘T ∈ 𝔐 (en notant T′∘T la composée). L'observation suivante sera cruciale : si g∈ℰ et T,T′∈𝔐, alors on a à la fois (T′∘T)(g) ⊇ T(g) (d'après (i) pour T′) et (T′∘T)(g) ⊇ T′(g) (d'après (i) pour T et (ii) pour T′).
Affirmation : si g∈ℰ alors la réunion des T(g) pour tous les T∈𝔐 est, en fait, une fonction partielle. En effet, l'observation faite ci-dessus montre que si T,T′ ∈ 𝔐 alors les fonctions partielles T(g) et T′(g) sont toutes deux restrictions d'une même fonction partielle (T′∘T)(g), donc il ne peut pas y avoir de conflit entre leurs valeurs (au sens où si toutes les deux sont définies en un x∈ X, elles y coïncident) — c'est exactement ce qui permet de dire que la réunion est encore une fonction partielle. Notons U(g) := ⋃T∈𝔐(T(g)) cette réunion. On a au moins U(g)∈𝒟. Mais en fait, comme U(g) prolonge tous les T(g), la croissance de Ψ assure que Ψ(U(g)) prolonge tous les Ψ(T(g)), qui prolongent eux-mêmes les T(g) (puisque T(g) ∈ ℰ), bref Ψ(U(g)) ⊇ U(g) et ainsi U(g)∈ℰ.
Mais alors U∈𝔐 (on vient de voir que U est une fonction ℰ→ℰ, et les propriétés (i) et (ii) sont claires). En particulier, Ψ∘U∈𝔐, donc (Ψ∘U)(g) est l'une des T(g) dont U(g) est la réunion, et on a donc (Ψ∘U)(g) ⊆ U(g), l'inclusion réciproque ayant déjà été vue (et de toute façon on n'en a pas besoin). On a donc bien trouvé une fonction partielle f := U(∅) telle que Ψ(f)⊆f (même Ψ(f)=f).
C'est quand même bizarrement compliqué, comme façon de faire ! (D'ailleurs, je veux quand même bien qu'on me confirme que c'est correct et compréhensible, comme démonstration.)
Bon, ceci étant, le David Madore étant un grand fan des ordinaux, on peut aussi procéder comme ceci :
Seconde démonstration de (F$) (utilisant les ordinaux) :
On pose f0 = ∅, et par induction sur l'ordinal α on définit fα+1 = Ψ(fα) et si δ est un ordinal limite alors fδ = ⋃γ<δ fγ. On montre simultanément par induction sur α que fα est bien définie, est une fonction partielle, et, grâce à la croissance de Ψ, prolonge fβ pour chaque β<α (c'est ce dernier point qui permet de conclure que ⋃γ<δ fγ est une fonction partielle lorsque δ est un ordinal limite : la réunion d'une famille totalement ordonnée pour l'inclusion de fonctions partielles est encore une fonction partielle). Les inclusions fβ ⊆ fα pour β<α ne peuvent pas être toutes strictes sans quoi on aurait une surjection d'un ensemble sur la classe des ordinaux. Il existe donc τ tel que fτ+1 = fτ, c'est-à-dire Ψ(fτ) = fτ. D'autre part, si Ψ(h) = h, alors par induction sur α on montre fα ⊆ h pour chaque α (l'étape successeur étant que si fα ⊆ h alors fα+1 = Ψ(fα) ⊆ Ψ(h) = h), donc en particulier fτ ⊆ h, et fτ est bien le plus petit f tel que Ψ(f) = f.
Oui, c'est beaucoup plus simple. Ça pourrait servir de pub pour les ordinaux, je devrais m'en réjouir.
Mais là, je me dis : ce n'est pas moral : l'énoncé élémentaire (F$), qui ne fait pas intervenir d'ordinaux, ne devrait pas en avoir besoin pour sa démonstration, et de fait, (P$) n'en avait pas besoin. Comment se fait-il que la démonstration de (P$) sans ordinaux se complique immensément quand on passe à (F$), alors qu'avec les ordinaux les quatre énoncés se démontrent exactement pareil (construire l'itération transfinie de Ψ, et constater que c'est l'objet recherché). J'ai passé beaucoup de temps à me gratter la tête sur comment « enlever » les ordinaux dans la démonstration ci-dessus, sans succès.
Il y a sans doute aussi moyen de s'en sortir en invoquant astucieusement le lemme de Zorn. Mais c'est encore pire, comme atteinte aux bonnes mœurs mathématiques : le résultat ne dépend en aucune manière de l'Axiome du Choix (et l'objet construit est complètement canonique), il est scandaleux de se servir du Choix pour abréger la démonstration. Au contraire, le genre de théorèmes de points fixes que j'ai cités peut servir à démontrer le lemme de Zorn à partir de l'Axiome du Choix.
J'ai aussi passé pas mal de temps à chercher à passer de (F) à (F$) un peu de la manière dont je suis passé de (P) à (P$) ci-dessus, là aussi sans succès (si on tente de définir Ψ₁(f) := f ∪ Ψ(f), rien ne garantit que c'est une fonction ; si on cherche à se limiter aux f pour lesquels ç'en est une, il me semble que ça ne marche vraiment pas).
Mise à jour () : Fab, dans les commentaires, me fait remarquer à juste titre que l'énoncé (F), quoique juste, est, en fait, creux. En effet, soit Z est un singleton, auquel cas (F) est équivalent à (P) (toujours grâce à l'« astuce » consistant à remarquer qu'une fonction partielle X⇢Z est alors essentiellement la même chose qu'une partie de X, à savoir la partie sur laquelle la fonction est définie). Soit Z est vide, auquel cas tout est trivial. Soit Z a strictement plus d'un élément, auquel cas le plus petit point fixe de Ψ est automatiquement la fonction vide. En effet, si Ψ(∅) est une fonction g non vide, disons g(x)=z avec x∈X et z∈Z, on considère h telle que h(x)=z′ où z′≠z (possible car Z n'est pas un singleton) : on a alors d'une part Ψ(h)⊇Ψ(∅)=g par croissance, et d'autre part Ψ(h)⊇h par progressivité, or g et h sont incompatibles en x, contradiction (c'est donc que Ψ(∅)=∅, et il est le plus petit point fixe de Ψ). Il n'était donc pas étonnant que je n'arrivasse pas à déduire (F$) de (F). Maintenant, je ne sais pas si cette remarque rend toute l'histoire plus claire ou encore plus mystérieuse…
Donc, quelque chose me gêne vraiment dans l'histoire, pas tellement au niveau mathématique mais au niveau métamathématique. Parfois l'histoire ne s'arrête pas à démontrer un théorème, mais à comprendre les différentes façons de le démontrer, et comment elles se relient les unes aux autres.
Mais il faut que j'admette que j'ai caché quelque
chose dans l'histoire, parce que j'en sais plus que je ne l'ai dit :
c'est le contenu de cet
article d'Andrej Bauer et Peter LeFanu Lumsdaine
(On the Bourbaki-Witt Principle in
Toposes), duquel d'ailleurs (cf. leur théorème 3.2, qui
n'est pas de ces auteurs mais que j'ai appris par eux) je tire
essentiellement la première démonstration (« hallucinante ») de (F$)
donnée ci-dessus. Pour décoder un peu ce qu'ils racontent, ils
s'intéressent à des principes affirmant l'existence de points fixes
d'opérateurs Ψ:𝒟→𝒟 (où 𝒟 est un
ensemble partiellement ordonné) en supposant soit (i) que Ψ
est progressif, i.e., x≤Ψ(x) pour
tout x, soit (ii) que Ψ est croissant, i.e.,
que x≤y
implique Ψ(x)≤Ψ(y), et en
supposant que 𝒟 admet des bornes supérieures soit
(a) quelconques, soit (b) de parties dirigées (:=dans lesquelles un
nombre fini quelconque d'éléments admettent toujours un majorant),
soit (c) de chaînes (:=parties totalement ordonnées). Cela donne six
principes de points fixes en combinant les hypothèses (i) et (ii) avec
les hypothèses (a), (b) et (c) : parmi eux, (i.a) est trivial, (ii.a)
et (ii.b) sont démontrables de façon « constructive » (valables dans
un « topos élémentaire »), c'est-à-dire sans utiliser le tiers exclu
ni l'Axiome de Remplacement[#2],
tandis que ni (i.b) et (i.c) (qui sont équivalents, et qu'ils
appellent théorème de Bourbaki-Witt) ni (ii.c) (qu'ils appellent
théorème de Knaster-Tarski) ne sont démontrables « constructivement »,
et ce défaut de constructivité passe par une question d'existence
d'assez d'ordinaux (et la démonstration non-« constructive » se fait
par induction transfinie exactement comme ci-dessus). • Le rapport
avec ce que je disais au-dessus, c'est que l'ensemble des parties d'un
ensemble X vérifie l'hypothèse (a) d'existence de bornes
supérieures quelconques, tandis que l'ensemble des fonctions
partielles X⇢Z vérifie seulement (b) (et du coup
(c) aussi, qui est plus faible). Ceci fournit une certaine lumière
sur le problème : d'abord, ceci « explique » pourquoi (P) est plus
simple que (P$), parce que la démonstration de l'existence
d'un point fixe dans le cas (i.a) est triviale, on prend
juste le plus grand élément de 𝒟, alors que dans le cadre
(ii.a) il faut réfléchir un petit peu plus ; d'autre part, les
ordinaux permettent d'utiliser la démonstration de (ii.c), tandis que
si on veut éviter le Remplacement qu'ils utilisent intrinsèquement, il
faut passer par (ii.b), or l'hypothèse (b) est plus délicate à mettre
en œuvre que (c) (on n'a pas juste à prendre des unions de familles
totalement ordonnées de fonctions, mais des familles dirigées
de fonctions, et c'est ce que fait la démonstration qui explique
que T(g) et T′(g) sont
toutes deux restrictions d'une même fonction partielle
(T′∘T)(g), donc il ne peut pas y
avoir de conflit entre leurs valeurs
). • Mais ceci ne clarifie pas
complètement les choses, parce que le cadre dans lequel je me place
est quand même différent : d'abord, je n'ai aucune objection à
utiliser le tiers exclu, d'autre part, pour ce qui est de (F) je suis
prêt à prendre (i) et (ii) comme hypothèses, pas juste l'une
des deux, ensuite je me place dans un cadre où il y a des bornes
inférieures représentées par les intersections, et de fait, je demande
le plus petit point fixe, et enfin, il est parfaitement imaginable
qu'une démonstration beaucoup plus simple existe dans le cadre concret
d'un ensemble de fonctions partielles que dans le cadre abstrait d'un
ensemble partiellement ordonné fût-il complet en tel ou tel sens.
Donc je ne peux pas dire que j'aie la clé du mystère
métamathématique.
[#2] En fait, je crois
que ce n'est pas tant un question de tiers exclu, et moralement la
démonstration vers les ordinaux ne l'utilise pas plus que les autres,
que de Remplacement, qui fait marcher les ordinaux,
donc constructif
n'est peut-être pas le bon terme (c'est le
terme standard, mais il suggère la mauvaise idée —
moralement, les ordinaux même immenses sont parfaitement constructifs,
c'est juste que le cadre métamathématique qu'on utilise pour faire des
maths constructives limite aussi les ordinaux, et du coup on en est
venu à utiliser un même terme pour une combinaison de choses
différentes). Mais j'avoue que mes idées sur le rôle de Remplacement
de l'affaire sont très incertaines : notamment, est-ce que l'énoncé
(ii.c) si Ψ:𝒟→𝒟 est une application
croissante où 𝒟 est un ensemble partiellement ordonné dans
lequel toutes les chaînes admettent une borne supérieure,
alors Ψ a un point fixe
est un théorème de la théorie
des ensembles de Zermelo ?