Feferman-Vaught Decompositions for Prefix Classes of First Order Logic
share
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.
READ FULL TEXT