Proof of Decidability of Monadic First Order Logic I'm looking for the proof of decidability of Monadic FOL (i.e. FOL limited to predicate symbols of arity at most one and no function symbols). In the Wikipedia page there are two references (dated 1915, 1922, both in German) but I couldn't find the English version of them. Besides, since decidability and "effective computation" was made precise in 30's (Church, Turing), I'm not sure these sources are the right ones. Do you know any book/paper that have the proof (sketch)? **Edit** : As pointed out by Achilles, it follows from the following proposition (proven in the book "The Classical Decision Problem"): _Proposition 6.2.1. **Let $\psi$ be a relational monadic formula, possibly with equality, of quantifier-rank $q$ with $m$ predicates. If $\psi$ is satisfiable, then it has a model of cardinality at most $q2^m$_.**

I have no reference, but it seems to me fairly straightforward that monadic FOL would be decidable: If you only have monadic predicates, and given that any sentence in monadic FOL would have only a finite number of monadic predicates (say $n$), then you can distinguish at most $2^n$ different 'kinds' of objects in terms of them having or not having the property as expressed by the predicate for each of the $n$ predicates. And without being able to express identity (which requires an at least 2-place relation), you cannot express that there are at least two of a certain 'kind'. Ergo: if there are no models for a sentence with $2^n$ objects in its domain, then there are no models either with more than $2^n$ objects in its domain. So, to see whether some sentence is a monadic FOL valid sentence, just check see if there is a model for its negation with $2^n$ objects: if ao, then the sentence is not valid, but if not, then it is.