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[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]

Voir aussi

Notes et références

John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 1^er janvier 2009, 681 p. (ISBN 978-0-521-89957-4 et 0-521-89957-5, lire en ligne)
Par théorème de complétude et fait que la théorie des ensembles n'a comme symboles non logiques que les symboles binaires que sont l'appartenance et l'égalité
Les cas "résistants" sont les théories qui sont cohérentes mais uniquement dans des modèles infinis. Voir aussi sur ce sujet les théorèmes d'incomplétude de Gödel.

Portail de la logique

Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.

[1] John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 1^er janvier 2009, 681 p. (ISBN 978-0-521-89957-4 et 0-521-89957-5, lire en ligne)

[2] Par théorème de complétude et fait que la théorie des ensembles n'a comme symboles non logiques que les symboles binaires que sont l'appartenance et l'égalité

[3] Les cas "résistants" sont les théories qui sont cohérentes mais uniquement dans des modèles infinis. Voir aussi sur ce sujet les théorèmes d'incomplétude de Gödel.