Théorème de Knaster-Tarski
{{#invoke:Bandeau|ébauche}} Le théorème de Knaster-Tarski est un théorème de point fixe pour une application croissante d'un treillis complet dans lui-même. Il est nommé d'après Bronislaw Knaster et Alfred Tarski.
Histoire
Knaster et Tarski, deux mathématiciens amis en Pologne, ont proposé la première version du théorème en 1928<ref>Modèle:Article With A. Tarski.</ref>. Le théorème de Knaster-Tarski est aussi appelé simplement théorème de point fixe de Tarski, le théorème ayant été publié par Tarski dans sa forme générale en 1955<ref>Modèle:Article</ref>. En 1955, Anne C. Davis montre une sorte de réciproque<ref>Modèle:Article</ref>.
En fait, Moschovakis, dans son livre de théorie des ensembles cité dans la bibliographie, fait remonter ce type de théorème de point fixe à la démonstration par Zermelo de son théorème éponyme, et ne nomme à ce sujet aucun autre mathématicien, sans doute pour éviter la loi de Stigler.
Énoncé
L'énoncé de Knaster-Tarski n'est pas le plus puissant du genreModèle:C'est-à-dire mais il est relativement simple : Modèle:Énoncé
Démonstrations
La démonstration Modèle:Refnec est Modèle:Refnec:
Soit <math>F</math> l'ensemble des points fixes de <math>f</math>. Montrons que dans <math>F</math>, toute partie <math>G</math> possède une borne supérieure. Pour cela, notons <math>m</math> la borne inférieure de l'ensemble <math>S:=\{x\in T\mid x\ge G\quad\text{et}\quad f(x)\le x\}</math>. Alors :
- <math>m\ge G</math> (car <math>S\ge G</math>) ;
- <math>f(m)\le m</math>. En effet, <math>f(m)\le S</math> car pour tout <math>x\in S</math>, d'une part <math>f(m)\le f(x)</math> (car <math>m\le x</math>) et d'autre part <math>f(x)\le x</math> ;
- <math>f(m)\ge m</math>. En effet, <math>f(m)\in S</math> car (d'après les deux points précédents) <math>f(m)\ge f(G)=G</math> et <math>f(f(m))\le f(m)</math> ;
- tout point fixe de <math>f</math> qui majore <math>G</math> appartient à <math>S</math> donc est minoré par <math>m</math>.
Par conséquent, <math>m</math> est la borne supérieure de <math>G</math> dans <math>F</math>.
Une seconde démonstration, d'un théorème plus faible, est la suivante : on démontre par récurrence transfinie que <math>f</math> a un point fixe.
On pose <math>x_0=</math> le plus petit élément de <math>T</math>, puis on construit une « fonction » <math>x</math> par récursion transfinie comme suit : si <math>\alpha</math> est un ordinal quelconque, <math>x_{\alpha+1}:= f(x_\alpha)</math>, et si <math>\alpha</math> est un ordinal limite, <math>x_\alpha</math> est la borne supérieure de <math>\{x_\beta\mid\beta < \alpha \}</math>. D'après le choix de <math>x_0</math> et la croissance de <math>f</math>, <math>\alpha\mapsto x_\alpha</math> est croissante. En choisissant un ordinal qui ne s'injecte pas dans <math>T</math> (par exemple son ordinal de Hartogs), on voit que <math>\alpha\mapsto x_\alpha</math> ne peut pas être injective et donc il existe <math>\gamma<\beta</math> tels que <math>x_{\gamma}=x_\beta</math>. Par croissance de <math>\alpha\mapsto x_\alpha</math>, <math>x_{\gamma}\le x_{\gamma+1}\le x_{\beta}=x_{\gamma}</math> donc <math>x_{\gamma}=x_{\gamma+1}=f(x_{\gamma})</math> : on a trouvé un point fixe.
Applications
En mathématiques
On peut démontrer le théorème de Cantor-Bernstein en appliquant celui de Knaster-Tarski : voir le § « Deuxième démonstration » de l'article sur ce théorème.
En informatique
Les principaux domaines d'applications sont la sémantique des langages de programmation et l'Modèle:Lien par interprétation abstraite ou model checking, domaines qui se recouvrent fortement.