Steps toward proving the non-well-founded-induction theorem by a fixed point argument.

1 files changed, 74 insertions, 13 deletions

diff --git a/notes-mitro206.tex b/notes-mitro206.tex
index 3effa67..49eecc5 100644
--- a/notes-mitro206.tex
+++ b/notes-mitro206.tex
@@ -35,6 +35,7 @@
 \newcommand{\outnb}{\operatorname{outnb}}
 \newcommand{\downstr}{\operatorname{downstr}}
 \newcommand{\mex}{\operatorname{mex}}
+\newcommand{\id}{\operatorname{id}}
 \newcommand{\limp}{\Longrightarrow}
 %
 \DeclareUnicodeCharacter{00A0}{~}
@@ -1203,19 +1204,79 @@ fonction $f$ qu'on vient de décrire est définie \emph{au moins} sur la
 partie bien-fondée de $G$.
 \end{thm}
 \begin{proof}
-Soit $\Gamma$ le plus petit ensemble de couples $(x,z) \in G \times Z$
-tel que (*) à chaque fois que $x\in G$ et que $g\colon \outnb(x)
-\dasharrow Z$ est inclus dans $\Gamma$ (au sens où $(y,g(y)) \in
-\Gamma$ pour chaque $y$ sur lequel $g$ est défini) on ait $(x,
-\Phi(x,g)) \in \Gamma$.  Ce plus petit ensemble a bien un sens car une
-intersection quelconque de parties de $G\times Z$ vérifiant (*)
-vérifie encore (*) (ceci est vrai puisque la condition (*) est de la
-forme « si certains éléments appartiennent à la partie, alors d'autres
-  éléments appartiennent à la partie »).
-
-Afin de pouvoir définir $f(x)$ comme le $z$ tel que $(x,z) \in \Gamma$
-s'il existe (autrement dit, la fonction de graphe $\Gamma$), il faut
-montrer qu'il y a \emph{au plus un} tel $z$.  \textcolor{red}{...}
+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}$}.
+\end{proof}
+
+\begin{lem}
+Soient $X$ et $Z$ deux ensembles quelconques : notons $\mathscr{D}$
+l'ensemble des fonctions partielles $X\dasharrow Z$, qu'on verra comme
+des parties de $X\times Z$ ne contenant jamais deux couples $(x,z_1)$
+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)$.
+\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
+\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.}
 \end{proof}