# Logique monadique du second ordre

En logique mathématique et en informatique théorique, la logique monadique du second ordre (abrégé en MSO pour monadic second order) est l'extension de la logique du premier ordre avec des variables dénotant des ensembles. De manière équivalente, c'est le fragment de la logique du second ordre où les quantifications du second ordre ne portent que sur des prédicats unaires (d'où le terme monadique), c'est-à-dire sur des ensembles. Par exemple :
* $\exists Z(\exists u,u\in Z)\land \forall x,(x\in Z\rightarrow \exists y,({\text{fils}}(x,y)\land y\in Z))$ est une formule de MSO et elle se lit « il existe un ensemble Z tel qu'il existe un élément u qui appartient à Z et pour tout x, si x est dans Z, alors il existe y tel que y est fils de x et y est dans Z ». Ce n'est pas une formule de la logique du premier ordre car il y a une quantification du second ordre sur Z ;
* Toutes les formules de la logique du premier ordre sont des formules de MSO ;
* La formule $\exists R,\exists x,\forall y,R(x,y)$ n'est pas une formule de MSO car il y a une quantification sur un prédicat binaire R.
Le problème de satisfiabilité de la logique du premier ordre étant indécidable, comme MSO est une extension conservatrice de la logique du premier ordre, le problème de satisfiabilité de MSO est aussi indécidable. Mais selon Yuri Gurevich, MSO est une source de théories logiques à la fois expressives et décidables.

## Exemples de formules

La formule qui définit la récurrence, $\forall X,(X(0)\land (\forall y,X(y)\rightarrow X(y+1)))\rightarrow (\forall z,X(z))$ et qui se lit « pour tout ensemble X, si 0 appartient à X, et si pour tout y, y appartient à X implique y+1 appartient à X alors pour tout z, z appartient à X » est une formule de MSO. Les quantifications « pour tout y » et « pour tout z » sont des quantifications du premier ordre. La quantification « pour tout X » est une quantification du second ordre.
Toutes les formules de la logique du premier ordre sont des formules de MSO.

## MSO et graphes

MSO a été défini sur des classes de graphes (par exemple, non orientés). Par exemple, on peut exprimer en MSO qu'un graphe n'est pas connexe : $\exists Z,(\exists x,x\in Z\land \exists y,y\not \in Z)\land (\forall u,v,{\text{arête}}(u,v)\rightarrow (u\in Z\leftrightarrow v\in Z))$ qui se lit « il existe un ensemble de sommets Z tel qu'il existe un sommet x contenu dans Z et un sommet y en dehors de Z et tel que si deux sommets u et v sont reliés par une arête, alors u est dans Z si et seulement si v est dans Z » (voir figure à droite). La connexité n'est pas définissable en logique du premier ordre (c'est une conséquence du théorème de compacité de la logique du premier ordre). Ainsi MSO est strictement plus expressive que la logique du premier ordre sur les graphes.
Sur une classe finie, MSO et la logique du premier ordre ont une expressivité équivalente. Il existe des classes infinies où MSO et la logique du premier ordre ont une expressivité équivalente$^,$.
Le théorème de Courcelle est un résultat algorithmique sur MSO et les graphes : toute propriété de MSO est décidable en temps linéaire dans la classe des graphes avec une largeur arborescente bornée. Par exemple, d'après le théorème de Courcelle, savoir si un graphe est coloriable avec 3 couleurs est décidable en temps linéaire sur la classe des graphes avec un treewidth borné. En effet, on peut exprimer en MSO qu'un graphe est coloriable avec trois couleurs avec la formule suivante : $\exists C_{1},\exists C_{2},\exists C_{3},\left(\forall s,\bigvee _{i=1}^{3}C_{i}(s)\right)\land \left(\forall s\bigwedge _{i,j=1 \atop i\neq j}^{3}(\lnot C_{i}(s)\lor \lnot C_{j}(s))\right)\land \left(\forall s,t,{\text{arête}}(s,t)\rightarrow \bigwedge _{i=1}^{3}(\lnot C_{i}(s)\lor \lnot C_{i}(t))\right)$. La formule se lit « il existe des ensembles de sommets C1, C2, C3 qui forment une partition du graphe et tels que deux sommets adjacents ne soient pas dans un même Ci ». Par contre, le problème de décision qui consiste à savoir si n'importe quel graphe est coloriable avec 3 couleurs est un problème NP-complet.

## Théorie des langages

La structure sur laquelle est définie MSO change grandement les résultats de définissabilité, de calculabilité, et de complexité.

### Mots finis

Büchi a démontré qu'un langage de mots finis est régulier si et seulement s'il est décrit par une formule de MSO sur les mots. MSO est strictement plus expressive que la logique du premier ordre sur les mots finis : la classe des langages de mots finis définis par la logique du premier ordre est la classe des langages sans étoile$^,$.

### Mots infinis

Büchi a aussi démontré qu'un langage est régulier si et seulement s'il est décrit par une formule de MSO sur les mots.
S1S (pour second-order with 1 successor) est une variante de MSO interprétée sur le domaine des entiers, avec un prédicat pour le successeur et un pour l'ordre. Büchi a démontré en 1962 que S1S est décidable en établissant une correspondance entre la satisfiabilité d'une formule de S1S et la vacuité d'un automate de Büchi. Elgot et Rabin ont démontré que l'on peut ajouter à S1S le prédicat unaire « être un nombre factoriel » ou « être une puissance de k » tout en restant décidable. Par contre, si on ajoute la fonction « fois 2 » au langage, on obtient toute l'arithmétique sur les entiers avec addition et multiplication et on obtient une logique indécidable.

### Arbres binaires

On appelle S2S (pour second-order with 2 successors) la variante de MSO pour parler de propriétés sur le modèle de l'arbre binaire infini. Rabin a montré que l'on peut plonger les MSO sur les arbres d'arité 3, 4 et même les arbres d'arité infinie dénombrable dans S2S. Rabin a démontré la décidabilité de S2S par réduction à la vacuité d'un automate d'arbre infini. Par contre, la logique monadique du second ordre sur l'arbre binaire infini avec en plus la relation « même niveau » est indécidable.

## Version faible

Une variante de MSO, dite faible (et notée WMSO pour weak MSO), a été considérée où la quantification du second ordre porte sur des sous-ensembles finis.

### WS1S

WS1S (pour weak second-order with 1 successor) est une variante de S1S où la quantification du second ordre porte uniquement sur les sous-ensembles finis. La décidabilité de WS1S a été démontré avant celle de S1S, par Büchi en 1960 et Algot en 1961. La preuve de décidabilité de WS1S s'obtient directement de celle de S1S puisque WS1S peut être vu comme un fragment syntaxique de S1S (on peut exprimer la finitude d'un ensemble dans S1S). On peut démontrer que l'arithmétique de Presburger est décidable en transformant une formule de l'arithmétique de Presburger en une formule de WS1S.
Büchi a montré qu'il y a équivalence, pour tout langage de mots infinis L, entre :
* L est définissable par une propriété S1S ;
* L est définissable par une propriété WS1S ;
* L est reconnaissable par un automate de Büchi.
Les équivalences sont effectives : on transforme une formule S1S en un automate de Büchi. Ainsi, la logique S1S (et WS1S) est décidable. La logique S1S est de complexité non élementaire.

### WS2S

WS2S (pour weak second-order with 2 successors) est une variante de S2S où la quantification du second ordre est uniquement sur les sous-ensembles finis. WS2S est décidable. WS2S est strictement plus faible que S2S. L'inclusion WS2S ⊆ S2S est stricte, en effet : pour tout langage L d'arbres binaires infinis, on a équivalence entre$^,$ :
* L et son complémentaire sont reconnaissables par un automate d'arbres avec condition de Büchi ;
* L est définissable dans WS2S.
Plus précisément, le langage défini par « il y a un chemin contenant une infinité de b » est reconnaissable par un automate de Büchi alors que son complémentaire ne l'est pas. Ainsi, ce langage est définissable dans S2S, mais pas dans WS2S.

## Théorie des groupes

MSO sur les groupes abéliens ordonnés où la quantification du second ordre est restreinte aux sous-groupes convexes est décidable.

## Invariance par bisimulation

À l'instar du théorème de Van Benthem qui dit que toute formule du première ordre $\phi (x)$ invariante par bisimulation est équivalente à (la traduction standard d') une formule de la logique modale, Janin et Walukiewicz ont démontré que toute formule de MSO invariante par bisimulation est équivalente à une formule du mu-calcul.
Il est folklore (voir) d'avoir la variante du théorème de Van Benthem suivante pour WMSO sur les arbres à arité fixée : toute formule de WMSO sur les arbres d'arité k invariante par bisimulation est équivalente à une formule du fragment mu-calcul sans alternance (Arnold et Niwinski ont donné la preuve complète dans le cas des arbres binaires, c'est-à-dire pour WS2S).
Le résultat est plus compliqué pour les arbres d'arités quelconques non fixées. D'une part, il existe une autre variante de MSO qui correspond au fragment sans alternance du mu-calcul. D'autre part, il existe un fragment du fragment du mu-calcul sans alternance qui correspond WMSO invariant par bisimulation.

## Axiomatisation

MSO sur les mots infinis peut être complètement axiomatisée. En partant du système d'axiomatisation de la logique du premier ordre, il suffit d'ajouter le schéma d'axiomes de compréhension ainsi qu'une version au second ordre de l'axiome de récurrence de Peano.

## Nombre d'alternances entre quantificateurs

Selon la structure sur laquelle MSO est interprétée, le nombre d'alternances entre quantificateurs existentiels et universels du second ordre nécessaires pour obtenir l'expressivité maximale de la logique varie. Dans l'interprétation de MSO sur les arbres infinis, toute formule MSO est équivalente à une formule utilisant deux alternances de quantificateurs monadiques. Dans l'interprétation sur des modèles finis à deux dimensions et coloriés (pictures model), une seule alternance suffit. Dans le cas des structures finies, il n'est par contre pas possible de restreindre le nombre d'alternances.

## Compacité de MSO

La logique monadique du second ordre est compacte.