Tree Languages Defined in First-Order Logic with One Quantifier Alternation

TL;DR

This paper characterizes tree languages definable by first-order formulas with a single quantifier alternation, providing algebraic conditions for their definability over trees with specific relations.

Contribution

It offers an effective algebraic characterization of -definable tree and forest languages, extending prior work from words to trees.

Findings

Effective algebraic characterization of -definable tree languages

Characterization applies to signatures with descendant and lexicographical order

Extends algebraic framework from words to trees

Abstract

We study tree languages that can be defined in \Delta_2 . These are tree languages definable by a first-order formula whose quantifier prefix is forall exists, and simultaneously by a first-order formula whose quantifier prefix is . For the quantifier free part we consider two signatures, either the descendant relation alone or together with the lexicographical order relation on nodes. We provide an effective characterization of tree and forest languages definable in \Delta_2 . This characterization is in terms of algebraic equations. Over words, the class of word languages definable in \Delta_2 forms a robust class, which was given an effective algebraic characterization by Pin and Weil.