Monadic second order definable relations on the binary tree
H. Läuchli, Christian Savioz · Journal of Symbolic Logic · 1987
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.