 Imagine a tree that has been built up in levels. At the bottom level there is a single root node, but a left branch and a right branch come up from it. At the next level up there are two nodes, one on each branch, and from each of these nodes a left branch and a right branch grow up. So on the next level up there are four nodes, and again the tree branches into left and right at each of these nodes. Continued to infinity, this tree is called the tree of two successor functions (namely left successor and right successor). Taking the nodes as elements and introducing two function symbols for left and right successor, we have a structure. A powerful theorem of Michael Rabin states that there is an algorithm which will tell us, for every monadic second-order sentence \(\phi\) in the language appropriate for this structure, whether or not \(\phi\) is true in the structure. (’Monadic second-order’ means that the logic is like first-order, except that we can also quantify over sets of elements—but not over binary relations on elements, for example.)