Decidability of second-order theories and automata on infinite trees.
Michael O. Rabin · Transactions of the American Mathematical Society · 1969
the first-order theory of the lattice of all closed subsets of the real line is decidable.Through Stone's representation theorm, the results concerning Cantor's discontinuum lead to results about boolean algebras.Thus the theory of countable boolean algebras with quantification over ideals, is decidable.The first-order theory of arbitrary boolean algebras with a sequence of distinguished ideals is decidable.This last result is an improvement of Tarski's result [15], and of Ershov's [6, Theorem 9].Finally, we give an application to the theory of games.We show that the statement, proved by Wolfe [17], that every Gale-Stewart game (see §2.5 for terminology) with a set in F0 is determinate, is expressible in the second-order theory of two successor functions.Thus Wolfe's theorem could be proved by applying the decision procedure.Due to the fact that we use reductions to a second-order theory, our decidability proofs are very direct.Through appropriate interpretations, the set variables allow us to talk about all structures in a certain class.Thus, for example, for every sentence F of the second-order theory of linear ordering, we write a sentence F of the second-order theory of (T, r0, r{) which asserts that F holds in all countable linearly ordered sets.Since we can decide whether Fis true in X.The set of all 2-trees is denoted by Vs.A S-automaton is a system 21 = , where 5 is a finite set, M: S x X -> P(S x S), S0£ S, and F^P(S).We define the notion of a finite automaton % accepting a S-tree v.The set of all S-trees accepted by 9Í is denoted by 7\9t).A set A ç Vs is called finite automaton (f.a.) definable if for some 5t, T(Sâ)=A.For a Sj x 22-tree v the projection on Si is the Si-tree pxv, where px(x, y) = x.The basic properties of f.a.definable sets are as follows.If AçVz, B^VZ, and C S^sixsa are f.a.definable, then so are A\J B, V%-A, and px{C).Automata defining the latter sets can be effectively constructed from automata defining the sets A, B, and C.The emptiness problem, whether for a given automaton 91 we have r(9í)= 0, is effectively solvable.Now let Sn be {0, 1}".We set up a one-to-one correspondence t between «-tuples Ä=(Als..., An) eP(T)n of subsets of T, and 5>-trees.Namely, t{Ä) = vx where vä(x) = (xa1(x), ..., XaXx))> xeT, where xa denotes the characteristic function of A.For every formula F(Alt..., An) of the second-order theory of two successor