Lemme de König

Le lemme de Kőnig permet de démontrer que : étant donné un ensemble de tuiles de Wang, le plan est pavable si, et seulement si tout carré fini est pavable si, et seulement si le quart de plan est pavable[2].

Le lemme de Kőnig intervient dans la démonstration du fait que si un langage est décidé par une machine de Turing non-déterministe (qui s'arrête sur toutes les entrées) alors il est décidé par une machine de Turing déterministe[3]. La démonstration considère l'arbre de calcul de la machine de Turing non-déterministe. Comme toutes les branches sont de longueur finie (car la machine s'arrête sur toutes les entrées) et que l'arbre de calcul est à branchement fini, le lemme de Kőnig implique que l'arbre de calcul est fini. On construit alors une machine de Turing déterministe qui réalise un parcours en largeur de l'arbre de calcul. Ce parcours termine puisque l'arbre de calcul est fini.

Smullyan a utilisé le lemme de Kőnig pour démontrer la terminaison du jeu "arbres et boules"[4]. Le jeu fonctionne comme suit. Au début, la boîte contient une boule numérotée par un nombre positif. À chaque étape, le joueur tire une boule numérotée k de la boîte puis place un nombre arbitrairement grand de boules numérotées par des nombres positifs strictement inférieurs à k. Le jeu s'arrête lorsque le joueur tire une boule numérotée 0. L'arbre dont les nœuds sont les boules manipulées et on met un arc entre une boule k et une autre k' avec k' < k si le joueur a mis k' à l'étape où la boule k a été tiré. L'arbre est à branchement fini et toutes les branches sont finies (vu que les numéros des boules décroissent strictement). Par le lemme de Kőnig, l'arbre est fini.

Dans cette sous-section, on donne une autre reformulation[5] du lemme de Kőnig qui ne fait pas référence à l'infini (le mot "infini" n'apparaît pas). En particulier, la démonstration n'utilise pas de négation (le mot "fini" n'est pas sous la portée d'une négation). Le lemme de Kőnig est une conséquence de la propriété suivante :

Une relation acyclique à branchement fini est globalement finie si et seulement si tous les éléments sont accessibles.

Une relation ${\displaystyle \,R}$ sur ${\displaystyle \,E}$ est à branchement fini si pour tout ${\displaystyle x\in E}$ l'ensemble ${\displaystyle \{y\in E\mid xRy\}}$ est fini.

Une relation ${\displaystyle \,R}$ est globalement finie si pour tout ${\displaystyle x\in E}$ l'ensemble ${\displaystyle \{y\in E\mid xR^{*}y\}}$ est fini, où ${\displaystyle \,R^{*}}$ est la fermeture réflexive et transitive de ${\displaystyle \,R}$.

Une relation ${\displaystyle \,R}$ est acyclique si ${\displaystyle x\,R^{*}\,y}$ et ${\displaystyle y\,R^{*}\,x}$ implique ${\displaystyle x\,=\,y}$.

L'ensemble des éléments accessibles par ${\displaystyle \,R}$ est le plus petit ensemble tel que ${\displaystyle ((\forall y\in E)~xRy\Rightarrow Acc_{R}(y))\Rightarrow Acc_{R}(x)}$.

La démonstration utilise l'axiome du choix dépendant, forme faible de l'axiome du choix.

De façon assez surprenante, le lemme de Kőnig ne se généralise pas aux arbres non dénombrables ; voir l'article Arbre d'Aronszajn pour plus de détails.