From ae52bfa212546e28747b2f2e0e2f6d977278005b Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Sat, 30 Jan 2016 01:44:24 +0100 Subject: Steps toward proving the non-well-founded-induction theorem by a fixed point argument. --- notes-mitro206.tex | 87 ++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 74 insertions(+), 13 deletions(-) (limited to 'notes-mitro206.tex') 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} -- cgit v1.2.3