Logique monadique du premier ordre

Cet article ne cite pas suffisamment ses sources (octobre 2016).

Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références ». En pratique : Quelles sources sont attendues ? Comment ajouter mes sources ?

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.

La logique monadique du premier ordre est le fragment syntaxique de la logique du premier ordre où les formules atomiques sont de la forme ${\displaystyle P(x)}$, où ${\displaystyle P}$ un symbole de prédicat unaire et ${\displaystyle 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 : ${\displaystyle [\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".

La question de savoir si une théorie exprimée en logique monadique du premier ordre est cohérente est décidable^[1]. 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^[2]) 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^[3].

• Classe de Bernays-Schönfinkel
• Logique monadique du second ordre

• Portail de la logique