Monadic First-Order Logic

Origin. Leopold Löwenheim, "Über Möglichkeiten im Relativkalkül" (Mathematische Annalen 76, 1915, 447–470), proved satisfiability decidable for first-order formulas whose predicates are all unary — the first substantial decidability result for a fragment of first-order logic, in the same paper that proved the Löwenheim–Skolem theorem. Thoralf Skolem, "Untersuchungen über die Axiome des Klassenkalküls" (1919), extended decidability to monadic second-order logic, and Heinrich Behmann's Habilitation thesis (Mathematische Annalen, 1922) solved the class again independently; the word "Entscheidungsproblem" itself first appears in Behmann's Göttingen lecture of 10 May 1921. The small-model argument that became the textbook proof was outlined by Hilbert and Bernays in their 1922/23 lecture course and printed in Hilbert–Ackermann (1928). Harry R. Lewis, "Complexity Results for Classes of Quantificational Formulas" (Journal of Computer and System Sciences 21, 1980), settled the complexity: NEXPTIME-complete.

Models. First-order logic with every predicate unary: properties, never relations. A structure is then a partition of the domain into at most 2ᵏ atom types — the Boolean combinations of the k predicates — and a formula can see nothing beyond which types are inhabited and, with equality, how many elements each holds up to the number of quantifiers. That poverty is the decidability. The syllogistic is its ancient fragment: every categorical form of Aristotelian syllogistics — all A are B, some A is not B — is a monadic sentence. Where the two-variable, guarded and fluted fragments restrict how relations may be used, the monadic class removes them; the fluted fragment properly contains its equality-free part.

Formalism.

Language: unary predicates P₁, …, Pₖ; individual variables; no function symbols; equality optional.

Atom types: τ(x) := L₁(x) ∧ … ∧ Lₖ(x), each Lᵢ either Pᵢ(x) or ¬Pᵢ(x). 2ᵏ types over k predicates; a monadic structure is its census of inhabited types.

One-variable normal form: Without equality, every sentence is equivalent to a Boolean combination of sentences ∃x τ(x). One variable suffices semantically; quantifier nesting adds nothing.

Finite model property: Satisfiable without equality → model of size ≤ 2ᵏ (the Hilbert–Bernays argument). Satisfiable with equality → model of size ≤ q·2ᵏ, q the number of quantifiers.

Complexity: NEXPTIME-complete (Lewis 1980); the bound is unchanged by equality.

What destroys decidability: One binary predicate: a reduction class — every first-order formula reduces, validity preserved, to one over a single binary relation (Kalmár 1937), so Church (1936) and Turing (1936) make the extension undecidable. Unary function symbols, without equality: still decidable. Monadic second-order quantification: still decidable (Skolem 1919) — set variables are only more unary predicates.

Symbols.

Metatheory. Decidability is Theorem 4 of Löwenheim's 1915 paper, reproved by Skolem (1919) — who proved it for monadic second-order logic, where quantified set variables behave as further unary predicates — and by Behmann (1922). The standard argument is Hilbert and Bernays': a satisfiable sentence with k predicates has a model of size at most 2ᵏ, since collapsing each inhabited atom type to a single element preserves truth, so satisfiability is a finite search. With equality the collapse must keep up to q representatives per type, q the number of quantifiers, giving the q·2ᵏ bound and preserving decidability (the bounds are in Börger, Grädel and Gurevich, The Classical Decision Problem, 1997). Satisfiability is NEXPTIME-complete with or without equality (Lewis 1980). The boundary is one binary predicate away: first-order logic over a single binary relation is a reduction class for all of first-order logic (Kalmár 1937), hence undecidable by Church (1936) and Turing (1936). Monadic second-order logic over the successor structure is also decidable, but by Büchi's automata method — a different theorem with a different proof, treated under monadic second-order logic; successor is a binary relation, exactly what this class forbids.

Applies to. The syllogistic, formalized: every categorical sentence is monadic. The classical decision problem, as its first decidable class. Boolean reasoning about sets — membership and emptiness constraints over combinations of properties. Decidable fragments.

Limitations. Nothing relational is expressible: no orders, no graphs, no functions viewed as relations — each quantified element is described in isolation by its atom type. One binary relation symbol already ends decidability. Expressiveness inside the class is exhausted by type counting: "there are more As than Bs" is already beyond it, since no monadic sentence compares the cardinalities of two types. Satisfiability is NEXPTIME-complete (Lewis 1980), so no polynomial-time decision procedure exists, unconditionally. Equality adds counting of each type up to the number of quantifiers, and no more.

© 2026 Lingenic LLC