Feferman-Vaught Decompositions for Prefix Classes of First Order Logic

TL;DR

This paper presents an efficient method for decomposing first-order logic sentences with fixed quantifier complexity on structures, enabling faster evaluation of logical properties on combined structures.

Contribution

It introduces an elementary-time decomposition technique for prenex first-order sentences with fixed quantifier alternations, extending to sum-like operations beyond disjoint unions.

Findings

Decomposition can be achieved in elementary time for fixed quantifier alternations.

The method applies to various binary operations like ordered sum and NLC-sum.

Results extend to a family of infinitary logics.

Abstract

The Feferman-Vaught theorem provides a way of evaluating a first order sentence $\varphi$ on a disjoint union of structures by producing a decomposition of $\varphi$ 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 $\varphi$. 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 $\varphi$. 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.