Monadic predicate calculus

In logic, the monadic predicate calculus (also called monadic first-order logic) is the fragment of first-order logic (also called predicate calculus) in which all relation symbols in the signature are monadic (that is, they take only one argument), and there are no function symbols. In other words, all atomic formulas are of the form ${\displaystyle P(t)}$, where ${\displaystyle P}$ is a relation symbol and ${\displaystyle t}$ is a term.

Monadic predicate calculus contrasts with the standard predicate calculus, which allows relation symbols that take two or more arguments. When we wish to emphasize the fact that the standard predicate calculus is not monadic, we would call it "polyadic predicate calculus".

Without polyadic relation symbols, monadic predicate calculus is weaker than the full predicate calculus. Indeed, it is even a decidable logic. That is, there exists a decision algorithm 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.