What interested me is that Rabin's theorem gives a rich decidable world: the complete infinite binary tree, together with monadic second-order logic, which can quantify over arbitrary sets of nodes.
Decidability results make me curious about their boundaries. I wanted to know what happens when this tree is given one more operation, especially one resembling arithmetic.
The part I liked most is that the question begins as a geometric one about branching trees and ends up being mostly about the powers of one semigroup element.
The tree has one root, every node has exactly two children, and it
continues forever.
It can conveniently be encoded by finite binary strings:
ε for the root and w0,w1 for the children of
w.
The strings are only an encoding; the branching tree is the object.
The tree has an ancestor order ≼, which under the string
encoding is the prefix order.
Nodes on different branches can be incomparable.
Rabin's theorem says that the MSO theory of this tree is decidable. MSO is much richer than first-order logic because it can quantify over sets of nodes, and it is closely connected with automata on infinite trees.
My question was whether adding an operation that looks a little like addition could destroy this decidability. There is no canonical addition of tree nodes, so the real question is what properties should make an operation “addition-like”.
Associativity, commutativity, and an identity are not enough: idempotent operations can satisfy such algebraic laws without exhibiting anything like arithmetic growth. The intuition I actually wanted was that adding nonzero things should not collapse back into one of them.
The obvious positivity condition from numbers is too strong.
Requiring x+y to be a strict descendant of both
x and y cannot work when the two nodes lie on
different branches.
With associativity, positive growth rules out idempotent non-root
elements.
Standard facts about monogenic semigroups then imply that the powers
a,a²,a³,… of every non-root a are distinct.
MSO can define the subsemigroup generated by a using its
usual reachability-via-closed-sets trick.
Therefore the expanded tree interprets (N>0,+), whose full
MSO theory is undecidable.
MSO(T,S0,S1,+) undecidable.
In particular, such an operation cannot already be MSO-definable in
Rabin's original tree.
At this point the tree has mostly disappeared from the argument. Its order supplied a condition that forced distinct powers; the powers themselves carry the arithmetic.
The route matters to me: a boundary question about Rabin's theorem led to an attempt to formalize positive addition on a branching tree; that condition forced distinct powers; the powers, rather than the tree, carried the arithmetic.