In
logic
, the
monadic predicate calculus
(also called
monadic first-order logic
) is the fragment of
first-order logic
in which all relation symbols
[
clarification needed
]
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.
Expressiveness
[
edit
]
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
).
[1]
[2]
Adding a single binary relation symbol to monadic logic, however, results in an undecidable logic.
Relationship with term logic
[
edit
]
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
[
clarification needed
]
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)
",
. Reasoning about such statements can, however, still be handled within the framework of term logic, although not by the 19 classical Aristotelian
syllogisms
alone.
Taking
propositional logic
as given, every formula in the monadic predicate calculus expresses something that can likewise be formulated in term logic. On the other hand, a modern view of the
problem of multiple generality
in traditional logic concludes that quantifiers cannot nest usefully if there are no polyadic predicates to relate the bound variables.
Variants
[
edit
]
The formal system described above 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
[
citation needed
]
[
clarification needed
]
, whereas admitting even a single binary function letter results in an undecidable logic.
Monadic second-order logic
allows predicates of higher
arity
in formulas, but restricts second-order quantification to
unary
[
clarification needed
]
predicates, i.e. the only second-order variables allowed are
subset variables
.
- ^
Heinrich Behmann
,
Beitrage zur Algebra der Logik, insbesondere zum Entscheidungsproblem
, in
Mathematische Annalen
(1922)
- ^
Lowenheim, L.
(1915) "Uber Moglichkeiten im Relativkalkul,"
Mathematische Annalen
76: 447-470. Translated as "On possibilities in the calculus of relatives" in Jean van Heijenoort, 1967.
A Source Book in Mathematical Logic
, 1879-1931. Harvard Univ. Press: 228-51.