DETERMINISTIC AUTOMATA AND THE MONADIC THEORY OF ORDINALS < ω 2

For any ordinal α let MT[α, <] be the monadic (second order) theory of [α, <] The language of MT[α, <] contains propositional connectives ~, ∨, ∧, ⊃, ≡, T, F; a binary predicate letter < interpreted as the order relation on α; individual variables t, x, y, z,..., ranging over α and monadic predicate or set variables X, Y, Z,..., ranging over subsets of α with quantification over both types of variables. MT[α, <] consists of all those sentences which are true in [α, <] with respect to the intended interpretation.