Ehrenfeucht, Vaught, and the decidability of the weak monadic theory of successor
Wolfgang H Thomas · ACM SIGLOG News · 2018
The decidability of the weak monadic theory of successor is usually considered as a consequence of the connection between monadic second-order logic and finite automata, as established around 1960 in papers of Büchi, Elgot, and Trakhtenbrot. However, there are several remarks and footnotes in papers of that time indicating that the result is also derivable from a theorem of A. Ehrenfeucht using an unpublished remark of R. L. Vaught. In the present note we review these hints and provide a proof along these lines. This simple argument is of methodological interest since it relies solely on first-order model theory and does not use finite automata.