Expressing that a tree has an even number of nodes in monadic second order logic

Question

Let $C^{fin}_2$ be the set of finite trees with outdegree at most two considered as a structure in a signature $Child(,)$. I'm trying to find a sentence in monadic second order logic that holds on $T \in C^{fin}_2$ iff $T$ has an even number of nodes.

I've been thinking about this problem for a while now. I thought about expressing a total order on the nodes of $T$ (in this case I would know how to finish), but I don't see how that's possible if I only have the $Child(,)$ relation.

Any ideas?

Answer 1

For a set variable $X$, you can write down a formula $\varphi(X)$ expressing that $X$ contains exactly those nodes in the tree which have an odd number of nodes strictly above them in the tree order (in other words, $X$ contains those nodes whose induced subtree has an even number of nodes). Then the desired statement says that the root of the tree is contained in $X$.

The trick for defining $X$ is to use recursive clauses. In detail, $\varphi(X)$ is the formalization of the following statement:

"For all nodes $y$,

• If $y$ has outdegree $0$, then $y\notin X$;
• If $y$ has outdegree $1$ and $z$ is its unique child node, then $y\in X$ iff $z\notin X$;
• If $y$ has outdegree $2$ and $z_1,z_2$ are its child nodes, then $y\in X$ iff ($z_1\in X \leftrightarrow z_2\notin X$)."

Now, letting $\psi(r)$ be the (first-order) formula which defines the root of the tree, what you need is the sentence

$$ \forall r\forall X(\varphi(X)\land \psi(r)\rightarrow r\in X). $$