论文标题
省略类型的杂种一阶逻辑中的定理与刚性符号
Omitting Types Theorem in hybrid-dynamic first-order logic with rigid symbols
论文作者
论文摘要
在目前的贡献中，我们证明了一种省略类型的定理（OTT），用于与刚性符号（即在否定和检索下封闭世界上具有固定解释的符号（即具有固定解释的符号）的任意片段。逻辑框架可以视为一个参数，它是由文献中一些众所周知的混合和/或动态逻辑实例化的。我们开发了一种强迫技术，然后根据局部满意度研究了强迫属性，这导致了OTT的精致证明。对于不可数的签名，结果需要紧凑，而对于可数签名，则无需紧凑。我们将OTT应用于我们的逻辑上的向上和向下löwenheim-skolems，以及其基于构造函数的变体的完整定理。本文的主要结果可以很容易地在机构模型理论框架中重塑，从而使其具有更高的一般性。
In the the present contribution, we prove an Omitting Types Theorem (OTT) for an arbitrary fragment of hybriddynamic first-order logic with rigid symbols (i.e. symbols with fixed interpretations across worlds) closed under negation and retrieve. 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 a forcing technique and then we study a forcing property based 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 its constructor-based variant. The main result of this paper can easily be recast in the institutional model theory framework, giving it a higher level of generality.
