title: Théorème de Fagin
text: # Théorème de Fagin
  
  Le théorème de Fagin est un résultat de théorie de la complexité des algorithmes, montrant l'égalité de la classe NP et de la classe des problèmes exprimables en logique du second ordre existentielle, c'est-à-dire en logique du premier ordre enrichie de quantifications existentielles sur les ensembles. C'est le résultat fondateur de la complexité descriptive.
  
  Ce résultat est remarquable, puisqu'il caractérise la classe NP sans avoir recours à une notion de modèle de calcul comme la machine de Turing.
  
  La preuve de ce résultat fut établie en 1973 par Ronald Fagin dans sa thèse de doctorat. Elle a été depuis reformulée et améliorée, notamment grâce au théorème de Lynch et à des résultats de Grandjean.
  
  On trouve une preuve de ce théorème dans le livre de complexité descriptive de Neil Immerman.
  
  ## Exemples
  
  Le problème de 3-coloration est dans NP et est décrit par le langage {G | il existe une 3-coloration des sommets de G telle deux sommets adjacentes ne soient pas de la même couleur}. Le théorème de Fagin dit qu'il est décrit par une formule de la logique du second ordre existentielle. En fait, il est décrit par 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=1i\neq j}^{3}(\lnot C_{i}(s)\lor \lnot C_{j}(s))\right)\land \left(\forall t,R(s,t)\rightarrow \bigwedge _{i=1}^{3}(\lnot C_{i}(s)\lor \lnot C_{i}(t))\right)$.
  
  Par exemple, le graphe ci-contre est un modèle de cette formule car il est coloriable avec trois couleurs.
  
  