On first-order definable operations on relational structures
This work is foundational for researchers in logic and theoretical computer science, providing a framework for understanding how first-order properties are preserved under definable operations on relational structures.
This paper surveys first-order (FO) definable unary and binary operations on relational structures, focusing on Backwards Translation Theorems and Splitting Theorems. It shows that FO properties of output structures can be expressed using FO properties of input structures, with quantifier-heights preserved for quantifier-free operations.
We survey the definitions and main properties of first-order (FO) definable unary operations on relational structures, called FO-transductions, and of FO-definable binary operations based on disjoint union and Cartesian product. We focus our study on Backwards Translation Theorems and Splitting Theorems that permit to express FO properties of output structures in terms of finitely many FO properties of the corresponding input ones. In the particular cases where the operations are defined by quantifier-free (QF) formulas, the quantifier-heights of the obtained sentences are no larger than those of the input ones. It follows that the class of finite models of a FO sentence is recognizable with respect to the considered QF operations. Recognizability has interesting algorithmic properties based on finite automata on terms, for structures having bounded tree-width or clique-width. We extend our results to FO sentences constructed with modulo counting existential quantifiers.