Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
Concept
Logique monadique du premier ordre
Résumé
In logic, the monadic predicate calculus (also called monadic first-order logic) is the fragment of first-order logic in which all relation symbols in the signature are monadic (that is, they take only one argument), and there are no function symbols. All atomic formulas are thus of the form , where is a relation symbol and is a variable.
Monadic predicate calculus can be contrasted with polyadic predicate calculus, which allows relation symbols that take two or more arguments.
The absence of polyadic relation symbols severely restricts what can be expressed in the monadic predicate calculus. It is so weak that, unlike the full predicate calculus, it is decidable—there is a decision procedure that determines whether a given formula of monadic predicate calculus is logically valid (true for all nonempty domains). Adding a single binary relation symbol to monadic logic, however, results in an undecidable logic.
The need to go beyond monadic logic was not appreciated until the work on the logic of relations, by Augustus De Morgan and Charles Sanders Peirce in the nineteenth century, and by Frege in his 1879 Begriffsschrifft. Prior to the work of these three men, term logic (syllogistic logic) was widely considered adequate for formal deductive reasoning.
Inferences in term logic can all be represented in the monadic predicate calculus. For example the argument
All dogs are mammals.
No mammal is a bird.
Thus, no dog is a bird.
can be notated in the language of monadic predicate calculus as
where , and denote the predicates of being, respectively, a dog, a mammal, and a bird.
Conversely, monadic predicate calculus is not significantly more expressive than term logic. Each formula in the monadic predicate calculus is equivalent to a formula in which quantifiers appear only in closed subformulas of the form
or
These formulas slightly generalize the basic judgements considered in term logic. For example, this form allows statements such as "Every mammal is either a herbivore or a carnivore (or both)", .
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.