Monadic predicate calculus

From Wikipedia, the free encyclopedia

In logic, the monadic predicate calculus is the fragment of predicate calculus in which all predicate letters are monadic (that is, they take only one argument), and there are no function letters. This means that all atomic formulae have the form P(x), where P is a predicate letter and x is a variable.

The absence of predicates with more than one argument severely restricts what can be expressed in the monadic predicate calculus. In fact, and in contrast to full predicate calculus, it is decidable whether a given monadic predicate calculus formula is logically valid. According to the modern viewpoint, the decidability of monadic predicate calculus exposes it as inadequate for general mathematical reasoning. It is, however, interesting that the need to go beyond monadic logic was only realized quite late in the history of mathematics.

Prior to the work of Frege in the late 19th century, syllogistic term logic was widely considered to be the universal foundation for all deductive reasoning. Inferences in term logic can all be represented in the monadic predicate calculus; for example the syllogism

All dogs are mammals
No mammal is a herbivore
Thus, no dog is a herbivore

can be notated in the language of monadic predicate calculus as

(\forall x\,D(x)\Rightarrow M(x))\land \neg(\exists y\,M(y)\land H(y)) \Rightarrow \neg(\exists z\,D(z)\land H(z))

where D, M and H denote the predicates of being, respecively, a dog, a mammal, and a herbivore.

Conversely, monadic predicate calculus is arguably not significantly more expressive than term logic. One easily proves that every formula in the monadic predicate calculus is equivalent to a formula in which quantifiers do not nest and appear only in closed subformulae of the shape

\forall x\,P_1(x)\lor\cdots\lor P_n(x)\lor\neg P'_1(x)\lor\cdots\lor \neg P'_m(x)

or

\exists x\,\neg P_1(x)\land\cdots\land\neg P_n(x)\land P'_1(x)\land\cdots\land P'_m(x),

which are each other's negations and slightly generalize the form of 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)", (\forall x\,\neg M(x)\lor H(x)\lor C(x)). Reasoning about such statements can, however, still be handled within the framework of term logic, although not by the 19 classical Aristotelian syllogisms alone. Thus, if propositional logic is taken for granted, every formula in monadic predicate calculus expresses something that can also be spoken about in traditional logic. On the other hand, a modern view of the problem of multiple generality in traditional logic is exactly that quantifiers cannot usefully nest if one has no multiary predicates with which to relate the bound variables.

[edit] Variants

The concept described here is sometimes called the pure monadic predicate calculus, where "pure" signifies the absence of function letters. Allowing monadic function letters changes the logic only superficially, whereas even a single binary function letter would allow an easy encoding of full predicate calculus.

Monadic predicate calculus is also called monadic first-order logic. Monadic second-order logic keeps the requirement that all predicates are unary, but allows for quantification over predicates.