We consider the monadic second order logic with two successor functions and equality, interpreted on the binary tree. We show that a set of assignments is definable in the fragment ∑{sub}2 of this logic if and only if it is definable by a Büchi automaton. Moreover we show that every set of second order assignments definable in ∑{sub}2 with equality is definable in ∑{sub}2 without equality as well. The present paper is sketchy due to space constraints; for more details and proofs see [7].
展开▼
