Embedded Finite Models Beyond Restricted Quantifier Collapse
Michael Benedikt, Ehud Hrushovski
TL;DR
This work expands embedded finite model theory beyond restricted quantifier collapse by introducing higher-order restricted-quantifier forms ($k$-RQ and $\text{ω}$-RQC) and examining their relation to expressiveness and evaluation complexity. It proves that for any fixed $k$ there are decidable theories that are $(k+2)$-RQC but not $k$-RQC, linking these separations to pure $k$-order spectra via Fraïssé limits. The paper also shows that natural decidable theories such as finite and pseudo-finite fields can fail to have any nontrivial RQC level, and in many cases entail non-elementary lower bounds on quantifier elimination and decision procedures. It further analyzes how expansions of the signature can sometimes restore collapse, while identifying persistent unrestrictedness in theories like atomless Boolean algebras. Together, these results map a richer landscape where expressiveness and complexity can decouple in intriguing ways, with implications for logic in databases, finite model theory, and the complexity of logical theories.
Abstract
We revisit evaluation of logical formulas that allow both uninterpreted relations, constrained to be finite, as well as an interpreted vocabulary over an infinite domain. This formalism was denoted embedded finite model theory in the past. It is clear that the expressiveness and evaluating complexity of formulas of this type depends heavily on the infinite structure. If we embed in a wild structure like the integers with additive and multiplicative arithmetic, logic is extremely expressive and formulas are impossible to evaluate. On the other hand, for some well-known decidable structures, the expressiveness and evaluating complexity are similar to the situation without the additional infrastructure. The latter phenomenon was formalized via the notion of ``Restricted Quantifier Collapse'': adding quantification over the infinite structure does not add expressiveness. Beyond these two extremes little was known. In this work we show that the possibilities for expressiveness and complexity are much wider. We show that we can get almost any possible complexity of evaluation while staying within a decidable structure. We also show that in some decidable structures, there is a disconnect between expressiveness of the logic and complexity, in that we cannot eliminate quantification over the structure, but this is not due to an ability to embed complex relational computation in the logic. We show failure of collapse for the theory of finite fields and the related theory of pseudo-finite fields, which will involve coding computation in the logic. As a by-product of this, we establish new lower-bounds for the complexity of decision procedures for several decidable theories of fields, including the theory of finite fields. In the process of investigating this landscape, we investigate several weakenings of collapse.