Omitting types theorem in hybrid dynamic first-order logic with rigid symbols
Omitting types theorem in hybrid dynamic first-order logic with rigid symbols
复制标题
刚性符号混合动态一阶逻辑中的省略类型定理
DOI：
10.1016/j.apal.2022.103212
复制
发表时间：
2023
影响因子：
0.8
通讯作者：
KOWALSKI Tomasz
中科院分区：
文献类型：
--
作者：
GAINA Daniel;BADIA Guillermo;KOWALSKI Tomasz
在本文中，我们证明了带有刚性符号(即具有固定解释的符号)的混合动态一阶逻辑的任意片段的省略类型定理(OTT)、闭包否定和检索。该逻辑框架可以被视为一个参数，并且它由文献中的一些著名的混合和/或动态逻辑来实例化。我们开发了一种强制技术，然后研究了基于局部可满足性的强制性质，从而得到了OTT的一个精细证明。对于不可数签名，结果要求紧致性，而对于可数签名，紧致性不是必要条件。我们应用OTT得到了我们的逻辑的向上和向下的L-温海姆-斯科勒姆定理，以及它的基于构造器的变量的完备性定理。
In the present contribution, we prove an Omitting Types Theorem (OTT) for an arbitrary fragment of hybrid dynamic first-order logic with rigid symbols (i.e. symbols with fixed interpretations across worlds) closed undernegationandretrieve. The logical framework can be regarded as a parameter and it is instantiated by some well-known hybrid and/or dynamic logics from the literature. We develop aforcingtechnique and then we study aforcing propertybased on local satisfiability, which lead to a refined proof of the OTT. For uncountable signatures, the result requires compactness, while for countable signatures, compactness is not necessary. We apply the OTT to obtain upwards and downwards Löwenheim-Skolem theorems for our logic, as well as a completeness theorem for itsconstructor-basedvariant.