 The proof goes via a reduction to automata. An automaton is a restricted form of a Turing machine. In an automaton the machine never writes on the tape, so the tape just contains the input (Rabin &amp; Scott 1959). However, the computation may be infinite. The input is considered accepted in the case of an infinite computation if an accepting state is reached infinitely many times. (There are also more complicated criteria of acceptance). With monadic second-order logic we can guess an accepting computation of the automaton. It is possible but more difficult to show that an automaton can check the truth of a monadic second-order sentence. The monadic second-order theory of ordinals \((\alpha,&lt;)\) have been studied extensively from the point of view of decidability. For example, the monadic second-order theory of all countable ordinals, the theory of \(\omega_1\), and the theory of all ordinals \(&lt;\omega_2\) are decidable (Büchi 1973), but ZFC cannot decide whether the monadic second-order theory of \(\omega_2\) is decidable (Gurevich, Magidor, &amp; Shelah 1983).