Tree languages defined in first-order logic with one quantifier alternation (Q6829992)

\textit{J.-E. Pin} and \textit{P. Weil} have shown in [``Polynomial closure and unambiguous product'', Theory Comput. Syst. 30, No. 4, 383--422 (1997; Zbl 0872.68119)] that a (word) language is \(\Delta_2\)-definable, in the language of alphabet labels and order, if and only if its syntactic monoid satisfies the identity \((xy)^\omega=(xy)^\omega x(xy)^\omega\). Recall that a language is \(\Delta_2\)-definable whenever it can be defined by a \(\Sigma_2\)-formula and by another \(\Pi_2\)-formula. In this paper, the authors show the analogous result for unranked ordered trees and forest languages. For a forest language, a (syntactic) forest algebra is associated, and it is shown that a forest language is definable in \(\Delta_2\), in the language of descending order and label tests, if and only if its syntactic forest algebra satisfies the following two identities:\N\N(1) \(h+g=g+h\), and (2) \(v^\omega wv^\omega=v^\omega\) for \(w\preceq v\).\N\NThus, it is decidable whether a forest language can be defined in \(\Delta_2\).\N\NFor the entire collection see [Zbl 1141.68001].