paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Locality in Residuated-Lattice Structures

剩余格结构中的局部性
LMCS vol.Volume 22, Issue 32026匹配度 1/10 · 论文研究剩余格多值模型中的 Hanf/Gaifman 局部性定理,属于数理逻辑与形式语义,与用户关注的程序静态分析、浮点/贝叶斯程序分析及 LLM/Agent 交叉方向无直接关联。引用 0 inbox
James Carr
crossref: 2026-09-10

AI 速览

一句话:研究经典 Hanf 与 Gaifman 局部性定理在剩余格多值模型中的推广与失效条件,并借助序解释连接词恢复主引理。

多值模型以任意代数定义真值,剩余格簇上的模型为一阶子结构逻辑提供语义。本文考察经典 Hanf 与 Gaifman 局部性定理在剩余格设定下成立到何种程度。结果依赖对广义局部性的理解以及真值代数的行为:Hanf 定理在自然的局部邻域理解下失效,但在 well-connected 剩余格上可用另一种理解恢复;对 Gaifman 定理,作者聚焦其主引理,即满足相同基本局部句子的模型初等等价,并证明在多种局部性理解下,若代数足以在语法中表达局部性,该引理仍可恢复。关键工具是序解释连接词,它连接模型—公式满足关系与公式到代数的赋值,从而支持来回系统的语法编码。

问题
经典 Hanf 与 Gaifman 局部性定理能否推广到以剩余格为真值代数的多值一阶子结构逻辑模型?其成立是否依赖局部性定义与真值代数性质?
方法
在剩余格结构上采用不同局部邻域与局部性理解,分析真值代数行为,并利用序解释连接词在语法中编码来回系统以证明局部性结果。
评估
证明 Hanf 定理在自然局部邻域理解下失败,但在 well-connected 剩余格上可经替代理解恢复;对 Gaifman 主引理,在若干局部性理解下,若代数能语法表达局部性则可恢复。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{Carr26,
  title = {Locality in Residuated-Lattice Structures},
  author = {James Carr},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 22, Issue 3},
  year = {2026},
  doi = {10.46298/lmcs-22(3:7)2026}
}