Complete/fix the proof of the non-well-founded induction theorem (and its key lemma).

1 files changed, 76 insertions, 59 deletions

diff --git a/notes-mitro206.tex b/notes-mitro206.tex
index 49eecc5..01790ef 100644
--- a/notes-mitro206.tex
+++ b/notes-mitro206.tex
@@ -1205,24 +1205,16 @@ partie bien-fondée de $G$.
 \end{thm}
 \begin{proof}
 Soit $\mathscr{D}$ l'ensemble des fonctions partielles $f \colon G
-\dasharrow Z$ telles que \emph{si} $f(x)$ est définie \emph{alors}
-$\Phi(x,\, f|_{\outnb(x)})$ l'est aussi et elles coïncident, autrement
-dit, telles que $f \subseteq (x \mapsto \Phi(x, f|_{\outnb(x)}))$.
-Pour $f \in \mathscr{D}$, on définit $\Psi(f)$ comme la fonction
-partielle $x \mapsto \Phi(x, f|_{\outnb(x)})$ (i.e., le prolongement
-de $f$ prescrit par la fonction $\Phi$ appliquée aux différentes
-restrictions de $f$).  Remarquons que (i) $\Psi(f)$ prolonge $f$
-(c'est la définition de $\mathscr{D}$) et (ii) si $f$ prolonge $g$
-dans $\mathscr{D}$ alors $\Psi(f)$ prolonge $\Psi(g)$ (c'est une
-traduction de la cohérence supposée sur $\Phi$).  Remarquons aussi que
-$\Psi(f)$ est encore un élément de $\mathscr{D}$ (car le fait que
-$\Psi(f)$ prolonge $f$ et le fait que $\Phi$ soit cohérente assurent
-que $x \mapsto \Phi(x, \Psi(f)|_{\outnb(x)})$ prolonge $x \mapsto
-\Phi(x, f|_{\outnb(x)})$, c'est-à-dire $\Psi(f)$).  Le lemme suivant
-permet de conclure {\color{red}moyennant quelques vérifications
-  sur $\mathscr{D}$}.
+\dasharrow Z$.  Pour $f \in \mathscr{D}$, on définit $\Psi(f)$ comme
+la fonction partielle $x \mapsto \Phi(x, f|_{\outnb(x)})$.  Remarquons
+que si $f$ prolonge $g$ dans $\mathscr{D}$ alors $\Psi(f)$
+prolonge $\Psi(g)$ (c'est une traduction de la cohérence supposée
+sur $\Phi$).  Le lemme suivant (appliqué à $X=G$, les autres notations
+étant inchangées) permet de conclure.
 \end{proof}
 
+La démonstration du théorème repose entièrement sur le lemme suivant,
+dont on va donner deux démonstrations :
 \begin{lem}
 Soient $X$ et $Z$ deux ensembles quelconques : notons $\mathscr{D}$
 l'ensemble des fonctions partielles $X\dasharrow Z$, qu'on verra comme
@@ -1231,52 +1223,77 @@ et $(x,z_2)$ avec la même première coordonnée.  (Lorsque $f\supseteq
 g$, on dit que « $f$ prolonge $g$ ».)
 
 Soit $\Psi \colon \mathscr{D} \to \mathscr{D}$ une fonction (totale !)
-vérifiant : (i) $\Psi$ est \emph{progressive}, c'est-à-dire que
-$\Psi(f)$ prolonge $f$ pour tout $f\in \mathscr{D}$, et (ii) $\Psi$
-est \emph{croissante} pour l'inclusion, c'est-à-dire que si $f$
-prolonge $g$, alors $\Psi(f)$ prolonge $\Psi(g)$.  Alors il existe une
-plus petite (au sens du prolongement) fonction partielle $f \in
-\mathscr{D}$ telle que $f = \Psi(f)$.
+vérifiant : $\Psi$ est \emph{croissante} pour l'inclusion,
+c'est-à-dire que si $f$ prolonge $g$, alors $\Psi(f)$
+prolonge $\Psi(g)$.  Alors il existe une plus petite (au sens du
+prolongement) fonction partielle $f \in \mathscr{D}$ telle que
+$\Psi(f) = f$.
 \end{lem}
 \begin{proof}[Première démonstration]
-Remarquons d'abord que s'il existe une fonction $f$ telle que $f =
-\Psi(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 =
-\Psi(f)$ (considérées comme des parties de $X\times Z$) : vu que
-chaque $f$ telle que $f = \Psi(f)$ prolonge $h$, l'hypothèse (ii)
-assure que chaque $f$ prolonge aussi $\Psi(h)$, mais du coup $h$ (qui
-est l'intersection de ces $f$) prolonge $\Psi(h)$, et comme (i) assure
-que réciproquement $\Psi(h)$ prolonge $h$, on a $\Psi(h) = h$.
-
-Il reste donc à montrer l'existence de $f$ vérifiant $f = \Psi(f)$
-(i.e., un point fixe de $\Psi$).
-
-Pour cela, soit $\mathfrak{M}$ l'ensemble des applications (totales !)
-$T\colon\mathscr{D}\to\mathscr{D}$ qui vérifient (i) $T(f)$
-prolonge $f$ pour tout $f\in \mathscr{D}$ et (ii) si $f$ prolonge $g$
-alors $T(f)$ prolonge $T(g)$.  Ainsi $\id_{\mathscr{D}} \in
-\mathfrak{M}$ et $\Psi \in \mathfrak{M}$, et si $T, T' \in
+Montrons d'abord que \emph{si} il existe une fonction partielle $f \in
+\mathscr{D}$ telle que $\Psi(f) = f$, ou même simplement $\Psi(f)
+\subseteq f$, alors il en existe une plus petite.  Pour cela, il
+suffit de considérer l'intersection $h$ de toutes les $f$ telles que
+$\Psi(f) \subseteq f$ (considérées comme des parties de $X\times Z$) :
+dès lors qu'il existe au moins un $f \in \mathscr{D}$ tel que $\Psi(f)
+\subseteq f$, cette intersection $h$ est bien définie et est bien un
+élément de $\mathscr{D}$.  Si $\Psi(f) \subseteq f$ alors $h \subseteq
+f$ (puisque $h$ est l'intersection des $f$), donc $\Psi(h) \subseteq
+\Psi(f)$ (par croissance de $\Psi$), donc $\Psi(h) \subseteq f$ (par
+transitivité), et comme ceci est vrai pour tous les $f$ dont
+l'intersection est $h$, on a finalement $\Psi(h) \subseteq h$ ; mais
+la croissance de $\Psi$ donne alors aussi $\Psi(\Psi(h)) \subseteq
+\Psi(h)$, et du coup $\Psi(h)$ fait partie des $f$ qu'on a
+intersectées pour former $h$, et on a ainsi $h \subseteq \Psi(h)$ ;
+bref, $\Psi(h) = h$, et $h$ est à la fois le plus petit élément $f \in
+\mathscr{D}$ vérifiant $\Psi(f) \subseteq f$ (de par sa construction)
+et le plus petit vérifiant $\Psi(f) = f$ (puisqu'il vérifie cette
+propriété).
+
+Reste à montrer qu'il existe bien une fonction partielle $f$ telle que
+$\Psi(f) = f$, ou même simplement $\Psi(f) \subseteq f$.  Pour cela,
+on introduit l'ensemble $\mathscr{E}$ des $f \in \mathscr{D}$ qui
+vérifient $\Psi(f) \supseteq f$ (inclusion dans le sens opposé du
+précédent !).  Notons que $\mathscr{E}$ n'est pas vide puisque
+$\varnothing \in \mathscr{E}$ (où $\varnothing$ est la fonction vide,
+définie nulle part).
+
+Soit maintenant $\mathfrak{M}$ l'ensemble des applications (totales !)
+$T\colon\mathscr{E}\to\mathscr{E}$ qui vérifient (i) $T(f) \supseteq
+f$ pour tout $f\in \mathscr{E}$ et (ii) si $f \supseteq g$ alors $T(f)
+\supseteq T(g)$.  Ainsi $\id_{\mathscr{E}} \in \mathfrak{M}$
+(trivialement) et $\Psi \in \mathfrak{M}$ (par définition de
+$\mathscr{E}$ et par croissance de $\Psi$) ; et si $T, T' \in
 \mathfrak{M}$ on a $T'\circ T \in \mathfrak{M}$ (en notant $T'\circ T$
-la composée).  Affirmation : si $g \in \mathscr{D}$ alors la réunion
-des $T(g)$ pour tous les $T\in\mathfrak{M}$ est, en fait, une
-fonction.  En effet, si $T,T' \in \mathfrak{M}$, alors $(T'\circ T)(g)
-= T'(T(g))$ prolonge $T(g)$ (d'après (i) pour $T'$) et aussi $T'(g)$
-(d'après (i) pour $T$ et (ii) pour $T'$), donc il ne peut pas y avoir
-de conflit.  Si on note $U(g) := \bigcup_{T\in\mathfrak{M}} T(g)$
-cette réunion dont on vient de voir qu'elle est dans $\mathcal{D}$,
-alors $U\colon \mathcal{D} \to \mathcal{D}$ est lui-même
-dans $\mathfrak{M}$ puisque les propriétés (i) et (ii) sont évidentes,
-et la définition fait que $U(g)$ prolonge $T'(g)$ pour
-\emph{tout} $T'\in\mathfrak{M}$.  En particulier, $T\circ U = U$,
-puisque d'une part $(T\circ U)(g)$ prolonge $U(g)$ (remarqué
-ci-dessus) et d'autre part $U(g)$ prolonge $(T\circ U)(g)$ comme il
-prolonge n'importe quel $T'(g)$.  Notamment, $\Psi\circ U = U$, et en
-appliquant à la fonction vide, on a $\Psi(f) = f$ si $f =
-U(\varnothing) = \bigcup_{T\in\mathfrak{M}} T(\varnothing)$.
-
-{\color{red}À modifier pour retirer la condition (i) (remplacer
-  $\mathscr{D}$ par l'ensemble des $f$ tels que $\Psi(f)$
-  prolonge $f$), quitte à déporter la partie « plus petit » ailleurs.}
+la composée).  L'observation suivante sera cruciale : si $g \in
+\mathscr{E}$ et $T, T' \in \mathfrak{M}$, alors on a à la fois
+$(T'\circ T)(g) \supseteq T(g)$ (d'après (i) pour $T'$) et $(T'\circ
+T)(g) \supseteq T'(g)$ (d'après (i) pour $T$ et (ii) pour $T'$).
+
+Affirmation : si $g \in \mathscr{E}$ alors la réunion des $T(g)$ pour
+tous les $T\in\mathfrak{M}$ est, en fait, une fonction partielle.  En
+effet, l'observation faite ci-dessus montre que si $T, T' \in
+\mathfrak{M}$ alors les fonctions partielles $T(g)$ et $T'(g)$ sont
+toutes deux restrictions d'une même fonction partielle $(T'\circ
+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\in 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) :=
+\bigcup_{T\in\mathfrak{M}} T(g)$ cette réunion.  On a au moins $U(g)
+\in \mathscr{D}$.  Mais en fait, comme $U(g)$ prolonge tous les
+$T(g)$, la croissance de $\Psi$ assure que $\Psi(U(g))$ prolonge tous
+les $\Psi(T(g))$, qui prolongent eux-mêmes les $T(g)$ (puisque $T(g)
+\in \mathscr{E}$), bref $\Psi(U(g)) \supseteq U(g)$ et ainsi $U(g) \in
+\mathscr{E}$.
+
+Mais alors $U \in \mathfrak{M}$ (on vient de voir que $U$ est une
+fonction $\mathscr{E}\to\mathscr{E}$, et les propriétés (i) et (ii)
+sont claires).  En particulier, $\Psi\circ U \in \mathfrak{M}$, donc
+$(\Psi\circ U)(g)$ fait partie des $T(g)$ dont $U(g)$ est la réunion,
+et on a donc $(\Psi\circ U)(g) \subseteq 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(\varnothing)$ telle
+que $\Psi(f) \subseteq f$ (même $\Psi(f) = f$).
 \end{proof}