论文标题
迈向有序逻辑的模型理论:表达和插值(扩展版本)
Towards a Model Theory of Ordered Logics: Expressivity and Interpolation (Extended version)
论文作者
论文摘要
我们考虑了一个受保护和无人看守的有序逻辑的家庭,构成了最近重新发现的一阶逻辑(FO)片段的家庭,其中变量的量化顺序与这些变量作为预测参数的顺序相吻合。 尽管现在已经确立了他们的满足性问题的复杂性,但他们的模型理论却鲜为人知。 我们的论文旨在提供一些了解。 首先,我们为有序逻辑提供合适的分合概念。 接下来,我们采用两次仿制来比较有序逻辑的相对表达能力,并将我们的逻辑描述为fo a la van benthem的三拟合不变片段。 之后,我们研究Craig插值特性〜(CIP)。 我们通过表明凹槽和前进的碎片不喜欢CIP来驳斥臭名昭著的作品中的另一项主张。 我们通过表明有序的片段和受保护的有序逻辑享受CIP来补充这一结果。 这些积极的结果依赖于新颖和复杂的模型结构,这些模型结构充分利用了我们逻辑的“远期”。
We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. While the complexities of their satisfiability problems are now well-established, their model theory, however, is poorly understood. Our paper aims to provide some insight into it. We start by providing suitable notions of bisimulation for ordered logics. We next employ bisimulations to compare the relative expressive power of ordered logics, and to characterise our logics as bisimulation-invariant fragments of FO a la van Benthem. Afterwards, we study the Craig Interpolation Property~(CIP). We refute yet another claim from the infamous work by Purdy, by showing that the fluted and forward fragments do not enjoy CIP. We complement this result by showing that the ordered fragment and the guarded ordered logics enjoy CIP. These positive results rely on novel and quite intricate model constructions, which take full advantage of the "forwardness" of our logics.