Tree Canonization and Transitive Closure

We prove that tree isomorphism is not expressible in the language (FO + TC + COUNT). This is surprising since in the presence of ordering the language captures NL, whereas tree isomorphism and canonization are in L (1992, S. Lindell, in “24th Symp. on Theory of Comput.” pp. 400–404). Our proof uses an Ehrenfeucht–Fraı̈ssé game for transitive closure logic with counting (1990, E. Grädel, Lecture Notes in Computer Science, Vol. 626, pp. 149–163, Springer-Verlag, Berlin; 1990, N. Immerman and E. Lander, in “Complexity Theory Retrospective,” pp. 59–81, Springer-Verlag, Berlin). As a corresponding upper bound, we show that tree canonization is expressible in (FO + COUNT)[log n]. The best previous upper bound had been (FO + COUNT)[nO(1)] (1990, P. Dublish and S. Mahesnwari, Lecture Notes in Computer Science, Vol. 452, Springer-Verlag, Berlin). The lower bound remains true for bounded-degree trees, and we show that for bounded-degree trees counting is not needed in the upper bound. These results are the first separations of the unordered versions of the logical languages for NL, AC1, and ThC1. Our results were motivated by our conjecture that (FO + TC + COUNT + 1LO) = NL, i.e., that a one-way local ordering sufficed to capture NL. We disprove this conjecture, but we prove that a two-way local ordering does suffice, i.e., (FO + TC + COUNT + 2LO) = NL.