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.

翻译：我们重新审视了允许同时包含受限于有限域的无解释关系以及无限域上有解释词汇的逻辑公式的评估问题。这种形式化方法在过去被称为嵌入式有限模型论。显然，这类公式的表达能力和评估复杂度在很大程度上依赖于无限结构。如果嵌入到像整数加法与乘法算术这样的任意结构中，逻辑将具有极强的表达能力，且公式难以评估。另一方面，对于某些已知的可判定结构，其表达能力和评估复杂度与没有额外基础设施的情况类似。后一种现象通过“受限量词坍缩”概念得以形式化：对无限结构的量化添加并不会增加表达能力。在这两个极端之间，我们知之甚少。在本工作中，我们展示了表达能力和复杂度的可能性范围要广泛得多。我们证明，在保持可判定结构的同时，评估复杂度几乎可以达到任何可能的级别。我们还证明了在某些可判定结构中，逻辑的表达能力与复杂度之间存在脱节——我们无法消除对结构的量化，但这并非因为逻辑能够嵌入复杂的关系计算。我们证明了有限域理论及相关伪有限域理论中的坍缩失败，这将涉及在逻辑中对计算进行编码。作为这一结果的副产品，我们为包括有限域理论在内的若干可判定域理论的判定过程复杂度建立了新的下界。在研究这一图景的过程中，我们探讨了坍缩的若干弱化形式。