Modal languages for topology: expressivity and definability

Characterising Modal Definability of Team-Based Logics via the Universal Modality

We study model and frame definability of various modal logics. Let ML(A+) denote the fragment of modal logic extended with the universal modality in which the universal modality occurs only positively. We show that a class of Kripke models is definable in ML(A+) if and only if the class is elementary and closed under disjoint unions and surjective bisimulations. We also characterise the definability of ML(A+) in the spirit of the well-known Goldblatt--Thomason theorem. We show that an elementary class F of Kripke frames is definable in ML(A+) if and only if F is closed under taking generated s…

Characterization and definability in modal first-order fragments

Model theoretic results such as Characterization and Definability give important information about different logics. It is well known that the proofs of those results for several modal logics have, somehow, the same 'taste'. A general proof for most modal logics below first order is still too ambitious. In this thesis we plan to isolate sufficient conditions for the characterization and definability theorems to hold in a wide range of logics. Along with these conditions we will prove that, whichever logic that meets them, satisfies both theorems. Therefore, one could give an unifying proof for…

二阶算术中的框架可定义性

Frame definability in second-order arithmetic

该文研究模态逻辑框架可定义性的反数学强度，证明估值扩张引理等相关原则与二阶算术子系统$\text{ACA}^{+}_0}$等价，还考察了CTL、LTL对应原则的强度。

关于直觉主义模态逻辑的有穷变量片段的算法表达力

On algorithmic expressivity of finite-variable fragments of intuitionistic modal logics

本文证明了直觉主义模态逻辑FS和MIPC可多项式时间嵌入其正单变量片段，揭示了其算法表达力。

Recursive enumerability and elementary frame definability in predicate modal logic

We investigate the relationship between recursive enumerability and elementary frame definability in first-order predicate modal logic. On the one hand, it is well-known that every first-order predicate modal logic complete with respect to an elementary class of Kripke frames, i.e., a class of frames definable by a classical first-order formula, is recursively enumerable. On the other, numerous examples are known of predicate modal logics, based on `natural' propositional modal logics with essentially second-order Kripke semantics, that are either not recursively enumerable or Kripke incomplet…

有序框架上基本模态-时态语言中功能性质的可定义性

Definability of Functional Properties in the Basic Modal-Temporal Language over Ordered Frames

研究基本模态-时态语言在有序框架上对九种功能性质的可定义性，发现原始多流设置表达能力弱，限制为最小功能框架后表达能力增强，但非线序中仍有不可定义性质。

Derivational modal logics with the difference modality

In this chapter we study modal logics of topological spaces in the combined language with the derivational modality and the difference modality. We give axiomatizations and prove completeness for the following classes: all spaces, $T_1$-spaces, dense-in-themselves spaces, a zero-dimensional dense-in-itself separable metric space, $R^n$ $(n\ge 2)$. We also discuss the correlation between languages with different combinations of the topological, the derivational, the universal and the difference modality in terms of definability.

Taming the `elsewhere': On expressivity of topological languages

In topological modal logic, it is well known that the Cantor derivative is more expressive than the topological closure, and the `elsewhere,' or `difference,' operator is more expressive than the `somewhere' operator. In 2014, Kudinov and Shehtman asked whether the combination of closure and elsewhere becomes strictly more expressive when adding the Cantor derivative. In this paper we give an affirmative answer: in fact, the Cantor derivative alone can define properties of topological spaces not expressible with closure and elsewhere. To prove this, we develop a novel theory of morphisms which…

An extension of Kracht's theorem to generalized Sahlqvist formulas

Sahlqvist formulas are a syntactically specified class of modal formulas proposed by Hendrik Sahlqvist in 1975. They are important because of their first-order definability and canonicity, and hence axiomatize complete modal logics. The first-order properties definable by Sahlqvist formulas were syntactically characterized by Marcus Kracht in 1993. The present paper extends Kracht's theorem to the class of `generalized Sahlqvist formulas' introduced by Goranko and Vakarelov and describes an appropriate generalization of Kracht formulas.

模态逻辑中的可靠性与完全性导入

Importing soundness and completeness in modal logics

提出从表达能力更强的模态语言向较弱语言传递可靠性与完全性的通用策略，统一了多种算子可定义性概念，并通过语义不敏感性和保真翻译实现。

Logics for Epistemic Actions: Completeness, Decidability, Expressivity

We consider dynamic versions of epistemic logic as formulated in Baltag and Moss "Logics for epistemic programs" (2004). That paper proposed a logical language (actually families of languages parameterized by action signatures) for dynamic epistemic logic. It had been shown that validity in the language is Pi-1-1-complete, so there are no recursively axiomatized complete logical systems for it. In contrast, this paper proves a weak completeness result for the fragment without action iteration, and a strong completeness result for the fragment without action iteration and common knowledge. Our …

凸团队逻辑

Convex Team Logics

本文证明凸命题和模态团队逻辑的表达完备性，引入多种完备逻辑，并回答经典命题逻辑加非空原子NE的开放问题，推广统一定义性概念。

discernment 是你所需要的

Discernment is all you need

本文探讨了 HOL 的表达能力及其作为统一逻辑框架的潜力，强调 discernment 在赋予 HOL 实用表达能力方面的重要性。