Logique monadique du premier ordre

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