 The second-order theory of even the empty vocabulary is undecidable, as we noted in  §5.1.  In contrast, monadic second-order logic gives rise to many important decidability results. Let us first observe that (not only in the empty vocabulary but also) in a monadic vocabulary, i.e., one consisting of monadic predicates only, monadic second-order logic is certainly decidable as proved already in 1915 by Löwenheim (1915) in one of the earliest papers on the mathematical aspects of formal logic. Löwenheim’s result can be proved easily by quantifier elimination, or alternatively by the more recent method of Ehrenfeucht-Fraïssé-games (see  §3).  However, monadic third (and higher) order logic in monadic vocabulary, with quantifiers over not only subsets and also over sets of subsets of the domain, is undecidable (Tharp 1973). We now focus on vocabularies which are not merely monadic.