一阶逻辑片段的Lindström定理
计算机科学中的逻辑
2015-07-01 v2
摘要
Lindström定理根据模型论条件（如紧致性和Löwenheim-Skolem性质）来刻画逻辑。大多数现有的此类刻画涉及一阶逻辑的扩展。但另一方面，许多与计算机科学相关的逻辑是一阶逻辑的片段或片段的扩展，例如k-变量逻辑和各种模态逻辑。为这些语言寻找Lindström定理可能具有挑战性，因为大多数已知技术依赖于编码论证，这些论证似乎需要一阶逻辑的完整表达能力。在本文中，我们为一阶逻辑的几个片段提供了Lindström定理，包括k>2的k-变量片段、Tarski关系代数、分级模态逻辑和二元有保护片段。我们使用了两种不同的证明技术。一种是对原始Lindström证明的修改。另一种涉及模态概念：互模拟、树展开和有限深度。我们的结果也蕴含了语义保持定理。
引用
@article{arxiv.0905.3668,
title = {Lindstrom theorems for fragments of first-order logic},
author = {Johan van Benthem and Balder ten Cate and Jouko Vaananen},
journal= {arXiv preprint arXiv:0905.3668},
year = {2015}
}
备注
Appears in Logical Methods in Computer Science (LMCS)