Many-valued models generalise the structures from classical model theory by defining truth values for a model with an arbitrary algebra. Just as algebraic varieties provide semantics for many non-classical propositional logics, models defined over algebras in a variety provide the semantics for the corresponding non-classical predicate logics. In particular, models defined over varieties of residuated lattices represent the model theory for first-order substructural logics. In this paper we study the extent to which the classical locality theorems from Hanf and Gaifman hold true in the residuated lattice setting. We demonstrate that the answer is sensitive both to how locality is understood in the generalised context and the behaviour of the truth-defining algebra. In the case of Hanf's theorem, we will show that the theorem fails for the natural understanding of local neighbourhoods, but is recoverable with an alternative understanding for well-connected residuated lattices. For Gaifman's theorem, rather than consider Gaifman normal forms directly we focus on the main lemma of the theorem from textbook proofs - that models which satisfy the same basic local sentences are elementarily equivalent. We prove that for a number of different understandings of locality, provided the algebra is well-behaved enough to express locality in its syntax, this main lemma can be recovered. In each case we will see the importance of an order-interpreting connective which creates a link between the modelling relation for models and formulas and the valuation function from formulas into the algebra. This link enables a syntactic encoding of back-and-forth systems providing the main technical ingredient to proofs of the main locality results.
翻译:多值模型通过为模型定义任意代数上的真值,推广了经典模型论中的结构。正如代数簇为许多非经典命题逻辑提供语义一样,在簇中代数上定义的模型为相应的非经典谓词逻辑提供语义。特别地,在剩余格簇上定义的模型表示了一阶子结构逻辑的模型论。本文研究经典局部性定理(Hanf 定理和 Gaifman 定理)在剩余格框架下成立的程度。我们证明,答案既取决于在广义语境下如何理解局部性,也取决于真值定义代数的行为。对于 Hanf 定理,我们将证明该定理在自然理解的局部邻域下不成立,但对于良连通剩余格,在另一种理解下可恢复。对于 Gaifman 定理,我们不直接考虑 Gaifman 范式,而是聚焦于教科书证明中该定理的主要引理——即满足相同基本局部语句的模型是初等等价的。我们证明,对于多种不同的局部性理解,只要代数行为足够良好,能在其句法中表达局部性,就可以恢复这一主要引理。在每种情况下,我们将看到序解释联结词的重要性,它在模型与公式的建模关系以及从公式到代数的赋值函数之间建立了联系。这种联系使得来回系统的句法编码成为可能,为主要局部性结果的证明提供了关键技术要素。