Paper detail

Feferman-Vaught Decompositions for Prefix Classes of First Order Logic

The Feferman-Vaught theorem provides a way of evaluating a first order sentence $φ$ on a disjoint union of structures by producing a decomposition of $φ$ into sentences which can be evaluated on the individual structures and the results of these evaluations combined using a propositional formula. This decomposition can in general be non-elementarily larger than $φ$. We show that for first order sentences in prenex normal form with a fixed number of quantifier alternations, such a decomposition, further with the same number of quantifier alternations, can be obtained in time elementary in the size of $φ$. We obtain this result as a consequence of a more general decomposition theorem that we prove for a family of infinitary logics we define. We extend these results by considering binary operations other than disjoint union, in particular sum-like operations such as ordered sum and NLC-sum, that are definable using quantifier-free interpretations.