title: Logique monadique du premier ordre
text: # Logique monadique du premier ordre
  
  En logique mathématique, la logique monadique du premier ordre est le fragment syntaxique de la logique du premier ordre où il n'y a que des prédicats unaires. Les syllogismes usuels, comme ceux issus de la Logique de Port-Royal relèvent de cette logique partielle.
  
  ## Définition formelle
  
  La logique monadique du premier ordre est le fragment syntaxique de la logique du premier ordre où les formules atomiques sont de la forme $P(x)$, où $P$ un symbole de prédicat unaire et $x$ est une variable.
  
  On peut y exprimer moult théories et aussi des syllogismes comme :
  
  Tous les chiens sont des mammifères
  
  et
  
  Aucun oiseau n'est un mammifère
  
  Donc
  
  Aucun chien n'est un oiseau.
  
  Raisonnement qui se formalise par : $[\forall x\,(estChien(x)\Rightarrow estMammifere(x))\land \neg \exists y\,(estMammifere(y)\land estOiseau(y))]\rightarrow \neg \exists z\,(estChien(z)\land estOiseau(z))$qui se lit
  
  ("pour tout x, si x est un chien alors x est un mammifère" et "il est faux qu'il existe y qui est à la fois un mammifère et un oiseau") implique qu'il est faux qu'il existe z qui est à la fois un chien et un oiseau".
  
  ## Cette logique est décidable
  
  La question de savoir si une théorie exprimée en logique monadique du premier ordre est cohérente est décidable. Ce qui signifie qu'il existe des algorithmes, comme la méthode des tableaux, permettant de décider en un nombre fini d'étapes si une telle théorie est cohérente ou non. Par opposition, la logique du calcul des prédicats du premier ordre générale (qui peut se ramener à la logique dyadique du premier ordre, soit avec des prédicats au plus binaires) n'est que semi-décidable : on peut toujours démontrer qu'une théorie est incohérente si elle l'est, mais on ne peut pas toujours démontrer qu'une théorie est cohérente lorsqu'elle l'est.
  
  