Monadic second order definable relations on the binary tree

Abstract

Abstract Let S2S [WS2S] respectively be the strong [weak] monadic second order theory of the binary tree T in the language of two successor functions. An S2S-formula whose free variables are just individual variables defines a relation on T (rather than on the power set of T ). We show that S2S and WS2S define the same relations on T , and we give a simple characterization of these relations.