一句话:重新审视嵌入式有限模型理论,扩展量词坍缩分析并比较签名与可判定理论。
本文重新审视嵌入式有限模型理论中的公式求值问题:公式同时包含被约束为有限的无解释关系以及无限域上的解释词汇。传统“坍缩”结果指可把无限域上的一阶量化消去,转化为有限结构上的量化。作者研究坍缩的若干弱化:一是允许对有限结构进行高阶量化,二是允许对理论作扩张;并给出了一元签名与一般签名下坍缩性质的比较,以及对若干自然可判定理论中坍缩现象的新分析。结果为在混合有限/无限域逻辑中判定与量化消去提供了更一般的框架。
We revisit evaluation of logical formulas that allow both uninterpreted relations, constrained to be finite, as well as interpreted vocabulary over an infinite domain: denoted in the past as embedded finite model theory. We extend the analysis of "collapse results": the ability to eliminate first-order quantifiers over the infinite domain in favor of quantification over the finite structure. We investigate several weakenings of collapse, one allowing higher-order quantification over the finite structure, another allowing expansion of the theory. We also provide results comparing collapse for unary signatures with general signatures, and new analyses of collapse for natural decidable theories.