混合动态Ehrenfeucht-Fraisse博弈
计算机科学中的逻辑
2025-06-12 v3
摘要
Ehrenfeucht-Fraisse博弈提供了一种刻画一阶逻辑初等等价性的方法，并通过标准翻译也适用于模态逻辑。我们提出了一种针对混合动态逻辑的Ehrenfeucht-Fraisse博弈的新颖推广，该推广是直接且完全模块化的：由我们希望包含的混合语言特征（例如，模态和混合语言算子以及一阶存在量化）参数化。我们使用这些博弈为混合动态命题逻辑及其各种片段建立了一个新的模块化Fraisse-Hintikka定理。我们研究了可数博弈等价（由可数Ehrenfeucht-Fraisse博弈确定）与互模拟（由可数back-and-forth系统确定）之间的关系。一般而言，前者弱于后者，但在语言的某些条件下，两者重合。我们还使用博弈证明，对于可达的像有限Kripke结构，初等等价性蕴含同构。
引用
@article{arxiv.2406.02094,
title = {Hybrid-Dynamic Ehrenfeucht-Fraisse Games},
author = {Guillermo Badia and Daniel Gaina and Alexander Knapp and Tomasz Kowalski and Martin Wirsing},
journal= {arXiv preprint arXiv:2406.02094},
year = {2025}
}