On the monadic theory ofω 1 without A.C.

Buchi inLecture Notes in Mathematics, Decidable Theories II (1973) by using A.C. characterized the theoriesMTβ, <] forβ<ω ₁ and showed thatMTω ₁, <] is decidable. We extend Buchi’s results to a larger class of models of ZF (without A.C.) by proving the following under ZF only: (1) There is a choice function which chooses a “good” run of an automaton on countable input (Lemma 5.1). It follows that Buchi’s results cocerning countable ordinals are provable within ZF. (2) Let U.D. be the assertion that there exists a uniform denumeration ofω ₁ (i.e. a functionf: ω ₁ → ω ₁ ^ω such that for everyα<ω ₁,f(α) is a function fromω ontoα). We show that U.D. can be stated as a monadic sentence, and thereforeω ₁ is characterizable by a sentence. (3) LetF be the filter of the cofinal closed subsets ofω ₁. We show that if U.D. holds thenMTω ₁, <] is recursive in the first order theory of the boolean algebraP (ω ₁)/F. (We can effectively translate each monadic sentence Σ to a boolean sentenceσ such that ω ₁, <] ⊨ Σ iffP(ω ₁)/F⊨σ). (4) As every complete boolean algebra theory is recursive we have that in every model of ZF+U.D.,MTω ₁, <] is recursive. All our proofs are within ZF. Buchi’s work is often referred to. Following Buchi, the main tool is finite automata. We don’t deal withMTω ₁, <] forω ₁ which doesn’t satisfy U.D. The results in this paper appeared in the author’s M.Sc. thesis, which was prepared at the Hebrew University under the supervision of Professor M. Rabin.