Théorie des modèles finis

La question générale se formule comme suit : Est-ce qu'un langage L est assez expressif pour décrire une structure finie S (à un isomorphisme près) ?

Deux graphes (1) et (1') qui ont des propriétés en commun.

Une structure comme figurée par le graphe (1) peut être décrite par des expressions de logique du premier ordre comme :

1. Chaque sommet est relié à un autre sommet : ${\displaystyle \forall x\exists yG(x,y)}$ ;
2. Aucun sommet n'a d'arête qui le relie à lui-même : ${\displaystyle \forall x\neg G(x,x)}$ ;
3. Au moins un sommet est relié à tous les autres sommets : ${\displaystyle \exists x\forall y(x\neq y\Rightarrow G(x,y))}$.

Mais ces propriétés ne suffisent pas à décrire la structure de manière unique (à un isomorphisme près) : la structure (1') vérifie toutes ces propriétés et les deux structures (1) et (1') ne sont pas isomorphes.

La question qui se pose est la suivante : est-il possible d'ajouter assez de propriétés pour que ces propriétés, dans leur ensemble, décrivent (1) exactement, et aucune autre structure (toujours à un isomorphisme près).

Pour une structure finie isolée, il est toujours possible de décrire sa structure par une seule formule de logique du premier ordre. Le principe est illustré pour une structure avec une relation binaire R et sans constantes :

1. exprimer qu'il y a au moins ${\displaystyle n}$ éléments : ${\displaystyle \varphi _{1}=\bigwedge _{1\leq i<j\leq n}\neg (x_{i}=x_{j})}$ ;
2. exprimer qu'il y a au plus ${\displaystyle n}$ éléments : ${\displaystyle \varphi _{2}=\forall y\bigvee _{1\leq i\leq n}(x_{i}=y)}$ ;
3. décrire tous les couples dans la relation ${\displaystyle R}$ : ${\displaystyle \varphi _{3}=\bigwedge _{(a_{i},a_{j})\in R}R(x_{i},x_{j})}$ ;
4. décrire tous les couples qui ne sont pas dans la relation ${\displaystyle R}$ : ${\displaystyle \varphi _{4}=\bigwedge _{(a_{i},a_{j})\notin R}\neg R(x_{i},x_{j})}$

pour le même n-uplet ${\displaystyle x_{1},\ldots ,x_{n}}$, ce qui donne la formule du premier ordre ${\displaystyle \exists {x_{1}}\dots \exists {x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})}$.

La méthode qui consiste à décrire une structure isolée par une formule du premier ordre peut être facilement étendue à tout nombre fixe fini de structures. Une description unique peut être obtenue par la disjonction des descriptions de chaque structure. Par exemple, pour deux structures cela donnerait :

${\displaystyle \exists {x_{1}}\dots \exists {x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})\lor \exists {x_{1}}\dots \exists {x_{n}}(\varrho _{1}\land \varrho _{2}\land \varrho _{3}\land \varrho _{4}).}$

Par définition, un ensemble contenant une structure infinie sort du cadre de la théorie des modèles finis. Les structures infinies ne peuvent jamais être définies dans la logique du premier ordre à cause du théorème de compacité de la théorie des modèles classique : pour tout modèle infini, il existe un modèle non isomorphe qui possède exactement les mêmes propriétés du premier ordre.

L'exemple le plus célèbre est probablement le théorème de Skolem qui affirme l'existence d'un modèle dénombrable non standard de l'arithmétique.

La question générale se formule comme suit : Est-ce qu'un langage L est assez expressif pour décrire une des structures finies qui ont en commun une certaine propriété P (à un isomorphisme près) ?

Ensemble de n structures.

Les descriptions données jusqu'à maintenant spécifient toutes le nombre d'éléments de l'univers. Toutefois, les ensembles de structures les plus intéressantes ne sont pas réduites à une taille donnée, comme les graphes qui sont des arbres, ou qui sont connexes ou sans cycle. La possibilité de discriminer un ensemble fini de structures est donc particulièrement important.

Plutôt que de formuler un énoncé général, voici une esquisse d'une méthode qui permet de distinguer les structures que l'on peut discriminer des autres.

1.- L'idée centrale est que pour savoir si une propriété P est exprimable en logique du premier ordre, on choisit des structures A et B, où A possède la propriété P et B ne la possède pas. Si les mêmes formules du premier ordre sont valables pour les structures A et B, alors P n'est pas définissable en logique du premier ordre. En bref :

${\displaystyle A\in P,B\notin P}$ et ${\displaystyle A\equiv B}$

où ${\displaystyle A\equiv B}$ est une abréviation pour ${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$ pour toute formule du premier ordre ${\displaystyle \alpha }$, et où ${\displaystyle P}$ représente la classe des structures ayant la propriété P.

2.- La méthode considère un nombre dénombrable de sous-ensembles du langage dont la réunion compose le langage tout entier. Par exemple, pour la logique du premier ordre, on considère des classes FO[m] pour chaque entier m. Pour chaque m, le test ci-dessus doit être effectué et l'équivalence montrée. En d'autres termes :

${\displaystyle A\in P,B\notin P}$ et ${\displaystyle A\equiv _{m}B}$

avec un couple ${\displaystyle A,B}$ pour chaque ${\displaystyle m}$ et ${\displaystyle \alpha }$ de FO[m]. Il peut être utile de choisir les classes FO[m] de sorte qu'elles forment une partition du langage.

3.- Une façon usuelle de définir FO[m] est par le rang de quantificateurs ${\displaystyle q(\alpha )}$ qui est le niveau de profondeur de l'imbrication des quantificateurs dans une formule ${\displaystyle \alpha }$. Pour une formule en forme prénexe, le rang est simplement le nombre de ses quantificateurs. On peut alors définir FO[m] comme l’ensemble des formules du premier ordre ${\displaystyle \alpha }$ dont le rang de quantificateurs ${\displaystyle q(\alpha )}$ est au plus m (ou, si l'on cherche une partition, comme celles dont le rang est égal à m).

4.- Tout ceci réduit la preuve de ${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$ aux sous-ensembles FO[m]. L'approche principale employée ici est la caractérisation algébrique fournie par le jeu d'Ehrenfeucht-Fraïssé. De manière informelle, on prend un isomorphisme partiel entre ${\displaystyle A}$ et ${\displaystyle B}$ et on l'étend m fois, en vue de prouver ou d'invalider ${\displaystyle A\equiv _{m}B}$, en fonction du gagnant du jeu.

Dans cet exemple, on montre que la propriété « La taille d'une structure ordonnée ${\displaystyle A=(A,\leq )}$ est paire » ne peut être exprimée en logique du premier ordre.

1.- L'idée est de prendre ${\displaystyle A}$ dans ${\displaystyle {\mathcal {P}}}$ et ${\displaystyle B}$ en dehors de ${\displaystyle {\mathcal {P}}}$, où ${\displaystyle {\mathcal {P}}}$ désigne la classe des structures de taille paire.

2.- On commence avec deux structures ${\displaystyle A_{2}}$ et ${\displaystyle B_{2}}$ avec univers ${\displaystyle A_{2}=\{1,2,3,4\}}$ et ${\displaystyle B_{2}=\{1,2,3,4,5\}}$. Évidemment, ${\displaystyle A_{2}}$ est dans ${\displaystyle {\mathcal {P}}}$ et ${\displaystyle B_{2}}$ n'y est pas.

3.- Pour ${\displaystyle m=2}$, on peut montrer (le détail de l'emploi du jeu d'Ehrenfeucht-Fraïssé est omis ici) qu'en deux mouvements d'un jeu d'Ehrenfeucht-Fraïssé sur ${\displaystyle A_{2}}$ et ${\displaystyle B_{2}}$, le duplicateur gagne toujours, et que ${\displaystyle A_{2}}$ et ${\displaystyle B_{2}}$ ne peuvent être distingués dans FO[2], c'est-à-dire que ${\displaystyle A_{2}\models \alpha \iff B_{2}\models \alpha }$ pour toute formule ${\displaystyle \alpha }$ de FO[2].

4.- On monte maintenant d'échelle en augmentant m. Par exemple, pour m = 3, il faut trouver ${\displaystyle A_{3}}$ et ${\displaystyle B_{3}}$ tels que le duplicateur gagne toujours dans un jeu à trois mouvements. On peut montrer que cela est possible avec ${\displaystyle A_{3}=\{1,\ldots ,8\}}$ et ${\displaystyle B_{3}=\{1,\ldots ,9\}}$. Plus généralement, on peut prendre ${\displaystyle A_{m}=\{1,\ldots ,2^{m}\}}$ et ${\displaystyle B_{m}=\{1,\ldots ,2^{m}+1\}}$; pour tout m, le duplicateur gagne toujours un jeu en m mouvements pour ce couple de structures.

5.- Ceci prouve que la propriété d'avoir un nombre pair d'éléments, pour des structures finies, n'est pas définissable en logique du premier ordre.

Les propriétés suivantes ne sont pas définissables par des formules du premier ordre ; la preuve est par le jeu d'Ehrenfeur-Fraïssé :

• La propriété « avoir un nombre pair d'éléments » (comme démontré ci-dessus) ;
• La propriété « être connexe » pour un graphe ;
• La propriété « être acyclique » pour un graphe ;
• La propriété « être transitif » pour un graphe[4].

Une partie substantielle du langage SQL, à savoir celui qui correspond à l'algèbre relationnelle, est basée sur la logique du premier ordre, car il peut être traduit en calcul relationnel par le théorème de Codd. Voici un exemple illustratif. Imaginons une table de base de données "GARÇONS" avec deux colonnes "PRÉNOM" et "NOM". Ceci correspond à une relation binaire, disons G(f,l) sur le produit PRÉNOM X NOM. Une requête du premier ordre {l : G('Paul', l)} retourne tous les noms qui correspondent au prénom 'Paul'. En SQL, elle s'écrit comme suit :

select NOM
from GARÇONS
where PRÉNOM = 'Paul'

On suppose ici que les noms de famille n'apparaissent qu'une fois dans la liste. Voici une requête plus complexe. En plus de la table "GARÇONS", on suppose qu'on a une table "FILLES", avec les mêmes deux colonnes. On cherche maintenant les noms des garçons que ont le même nom de famille qu'une fille. La requête en premier ordre est {(f,l) : ∃h ( G(f, l) ∧ B(h, l) )}, et l'instruction SQL est :

select PRÉNOM, NOM 
from GARÇONS
where NOM IN (select NOM from FILLES);

Pour exprimer le "∧", on a introduit le nouvel élément "IN" avec une instruction de sélection. Ceci rend le langage plus expressif, mais on peut aussi utiliser un opérateur "JOIN", et écrire

select distinct g.PRÉNOM, g.NOM
from GARÇONS g, FILLES b
where g.NOM=b.NOM;

La logique du premier ordre est trop restrictive pour certaines applications en bases de données, par exemple par l'impossibilité d'y exprimer la transitive closure. Ceci a conduit à l'ajout d'opérateurs plus puissants aux langages de requêtes des bases de données, tels que la clause WITH dans la version SQL:1999. Des versions plus expressives de logique, comme la logique du point fixe (en), ont alors été étudiées dans le cadre de la théorie des modèles finis, à cause de leur rapport avec la théorie des bases de données et de ses applications.

Un exemple de la théorie des langages formels[1]. On considère un alphabet binaire ${\displaystyle \{a,b\}}$. Pour un mot ${\displaystyle w=a_{1}\cdots a_{n}}$ on crée une structure ${\displaystyle M_{w}}$ comme suit : l'univers est l'ensemble ${\displaystyle \{1,\ldots ,n\}}$ correspondant aux positions dans le mot, avec l'ordre usuel. Deux relations unaires ${\displaystyle R_{a}}$ et ${\displaystyle R_{b}}$ sont vraies selon la valeur de la lettre : ${\displaystyle R_{a}(i)}$ est vrai si ${\displaystyle a_{i}=a}$ et ${\displaystyle R_{b}(i)}$ est vrai si ${\displaystyle a_{i}=b}$. Par exemple, ${\displaystyle M_{abba}}$ a l'univers ${\displaystyle \{1,2,3,4\}}$, et ${\displaystyle R_{a}}$ est vrai pour ${\displaystyle \{1,4\}}$ et ${\displaystyle R_{b}}$ pour ${\displaystyle \{2,3\}}$. Un exemple de formule de logique du premier ordre est :

${\displaystyle \lnot (\exists i\exists j((i<j)\land R_{b}(i)\land R_{a}(j))}$

Cette formule décrit le fait que les lettres ${\displaystyle b}$ suivent les lettres ${\displaystyle a}$ dans le mot, en d'autres termes que le mot appartient au langage rationnel dont une expression régulière est ${\displaystyle a^{*}b^{*}}$. Le lien entre les langages rationnels et les formules logiques est le suivant :

• Il existe une formule du premier ordre pour décrire un langage si et seulement s'il est un langage sans étoile[7] ;
• Les langages rationnels sont exactement les langages décrits par la logique du second ordre dite monadique, c'est-à-dire avec des quantificateurs du second ordre portant sur des ensembles de positions[1].

Par exemple, le langage ${\displaystyle (aa)^{*}}$ formé des mots de longueur paire sur un alphabet unaire n'est pas exprimable par une formule du premier ordre[1].

• Arnaud Durand, « Logique, jeux et définissabilité », Notes du cours Théorie des modèles finis du Master Logique Mathématique et Fondements de l'Informatique, Université Paris-7 Diderot.
• Leonid Libkin, « The finite model theory toolbox of a database theoretician », dans PODS 2009: Proceedings of the twenty-eighth ACM SIGACT–SIGMOD symposium on Principles of database systems, 2009 (DOI 10.1145/1559795.1559807, lire en ligne), p. 65–76. Utile comme introduction générale et comme survol.
• Leonid Libkin. Elements of Finite Model Theory, Introduction. Motivation des trois domaines principaux d'application : bases de données, complexité et langages formels.
• Jouko Väänänen, « A Short Course on Finite Model Theory ». Department of Mathematics, University of Helsinki. Basé sur un cours de 1993-1994.
• Anuj Dawar. Infinite and Finite Model Theory, transparents, University of Cambridge, 2002.
• « Algorithmic Model Theory », RWTH Aachen (consulté le 7 novembre 2013). Contient une liste de problèmes ouverts.

• Heinz-Dieter Ebbinghaus et Jörg Flum, Finite Model Theory, Springer, 1995, 327 p. (ISBN 978-3-540-60149-4)

• Leonid Libkin, Elements of Finite Model Theory, Springer, 2004, 318 p. (ISBN 3-540-21202-7, lire en ligne)

• (en) Serge Abiteboul, Richard Hull et Victor Vianu, Foundations of Databases, Reading, Mass, Addison-Wesley, 1995, 685 p. (ISBN 0-201-53771-0)

• (en) Neil Immerman, Descriptive Complexity, New York, Springer, 1999, 268 p. (ISBN 0-387-98600-6, lire en ligne)

• Complexité descriptive
• Théorie des bases de données
• Théorie des jeux
• Langage formel
• Calcul des prédicats
• Théorème de Löwenheim-Skolem
• Moshe Vardi
• Ronald Fagin