Monadic second-order logic comes in two variants. In the variant considered over structures such as graphs and in Courcelle's theorem, the formula may involve non-monadic predicates (in this case the binary edge predicate E(x, y)), but quantification is restricted to be over monadic predicates only. In the variant considered in automata theory and the Büchi-Elgot-Trakhtenbrot theorem, all predicates, including those in the formula itself, must be monadic, with the exceptions of equality (=) and ordering (<) relations.
