首页/论文/2003.08070

arXiv 2003.080702020-03math.LOcs.LO

Sahlqvist Correspondence Theory for Sabotage Modal Logic

Zhiguang Zhao

英文摘要：

Sabotage modal logic (SML) is a kind of dynamic logics. It extends static modal logic with a dynamic modality which is interpreted as "after deleting an arrow in the frame, the formula is true". In the present paper, we are aiming at solving an open problem, namely giving a Sahlqvist-type correspondence theorem for sabotage modal logic. In this paper, we define sabotage Sahlqvist formulas and give an algorithm to compute the first-order correspondents of sabotage Sahlqvist formulas. We give some remarks and future directions at the end of the paper.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

无分布模态逻辑：Sahlqvist—Van Benthem 对应关系

Distribution-Free Modal Logics: Sahlqvist -- Van Benthem Correspondence

本文提出无分布模态逻辑中Sahlqvist—Van Benthem对应关系的扩展，通过还原主义策略和格扩展与框架的对偶性实现可扩展的对应关系方法。

2025-03-16cs.LOmath.LO

Algebraic modal correspondence: Sahlqvist and beyond

The present paper proposes a new introductory treatment of the very well known Sahlqvist correspondence theory for classical modal logic. The first motivation for the present treatment is {\em pedagogical}: classical Sahlqvist correspondence is presented in a uniform and modular way, and, unlike the existing textbook accounts, extends itself to a class of formulas laying outside the Sahlqvist class proper. The second motivation is {\em methodological}: the present treatment aims at highlighting the {\em algebraic} and {\em order-theoretic} nature of the correspondence mechanism. The exposition…

2016-06-22math.LO

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.

2010-03-12math.LO

Sahlqvist theory for impossible worlds

We extend unified correspondence theory to Kripke frames with impossible worlds and their associated regular modal logics. These are logics the modal connectives of which are not required to be normal: only the weaker properties of additivity and multiplicativity are required. Conceptually, it has been argued that their lacking necessitation makes regular modal logics better suited than normal modal logics at the formalization of epistemic and deontic settings. From a technical viewpoint, regularity proves to be very natural and adequate for the treatment of algebraic canonicity Jónsson-style.…

2016-03-27math.LO

Non-finitely axiomatisable modal product logics with infinite canonical axiomatisations

Our concern is the axiomatisation problem for modal and algebraic logics that correspond to various fragments of two-variable first-order logic with counting quantifiers. In particular, we consider modal products with Diff, the propositional unimodal logic of the difference operator. We show that the two-dimensional product logic Diff x Diff is non-finitely axiomatisable, but can be axiomatised by infinitely many Sahlqvist axioms. We also show that its `square' version (the modal counterpart of the substitution and equality free fragment of two-variable first-order logic with counting to two) …

2020-01-28cs.LOmath.LO

多值模态逻辑的对应理论

Correspondence Theory for Many-valued Modal Logic

本文将 Sahlqvist 对应理论推广到以完备 Heyting 代数为真值空间的 Fitting 多值模态语义，定义参数化框架对应并改造 ALBA 算法，证明多值 Sahlqvist 与归纳公式的对应性及经典情形的句法一致性。

2025-06-10math.LO

更多相关论文收起更多论文

构造模态逻辑的对偶性：从萨尔奎维斯特到戈德布拉特-托马森

Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason

Mathematical Institute, University of Bern（伯尔尼大学数学研究所）；School of Computer Science, University of Birimingham（伯明翰大学计算机学院）；School of Computing, The Australian National University（澳大利亚国立大学计算学院）

本文研究了构造模态逻辑CK的语义学，建立代数与双关系语义的对偶性，并由此证明了萨尔奎维斯特类型的对应性和完备性结果，以及戈德布拉特-托马森类型的框架类可定义性定理。

2026-04-13cs.LOmath.LO

带破坏行为的完全博弈逻辑

Complete Game Logic with Sabotage

本文提出带破坏行为的博弈逻辑 GLs，通过增加设置陷阱的原语扩展 Parikh 博弈逻辑，证明其表达力与模态 μ-演算相当，并给出 Hilbert 风格证明演算的完全性。

2024-06-04cs.GTcs.LOmath.LO

超越分配性的正模态逻辑

Positive Modal Logic Beyond Distributivity

本文通过建立非分配（模态）格的对偶理论，提出弱正模态逻辑，证明其$Π_1$-持续性，并给出新的关系语义及Sahlqvist对应定理的类比结果。

2023-06-22cs.LOmath.LO

A dichotomy for some elementarily generated modal logics

In this paper we consider the normal modal logics of elementary classes defined by first-order formulas of the form $\forall x_0 \exists x_1 \dots \exists x_n \bigwedge x_i R_λx_j$. We prove that many properties of these logics, such as finite axiomatisability, elementarity, axiomatisability by a set of canonical formulas or by a single generalised Sahlqvist formula, together with modal definability of the initial formula, either simultaneously hold or simultaneously do not hold.

2015-02-27math.LO

Algorithmic Correspondence and Canonicity for Possibility Semantics

The present paper develops a unified correspondence treatment of the Sahlqvist theory for possibility semantics, extending the results in \cite{Ya16} from Sahlqvist formulas to the strictly larger class of inductive formulas, and from the full possibility frames to filter-descriptive possibility frames. Specifically, we define the possibility semantics version of the algorithm ALBA, and an adapted interpretation of the expanded modal language used in the algorithm. We prove the soundness of the algorithm with respect to both (the dual algebras of) full possibility frames and (the dual algebras…

2016-12-15math.LO

命题量化模态逻辑的若干一般性完全性结果

Some General Completeness Results for Propositionally Quantified Modal Logics

本文研究命题量化模态逻辑的完全性问题，证明含Barcan模式的正规逻辑在可量化一般框架下强完全，给出公式真值在框架过渡中保持的充分条件，并基于有限多样性得到一类Kripke完全的逻辑及欧几里得框架逻辑的有限公理化。

2024-06-23cs.LOmath.LO

Unified Correspondence as a Proof-Theoretic Tool

The present paper aims at establishing formal connections between correspondence phenomena, well known from the area of modal logic, and the theory of display calculi, originated by Belnap. These connections have been seminally observed and exploited by Marcus Kracht, in the context of his characterization of the modal axioms (which he calls primitive formulas) which can be effectively transformed into `analytic' structural rules of display calculi. In this context, a rule is `analytic' if adding it to a display calculus preserves Belnap's cut-elimination theorem. In recent years, the state-of…

2016-03-27cs.LOmath.LO

Crisp bi-Gödel 模态逻辑及其亚相容扩张

Crisp bi-Gödel modal logic and its paraconsistent expansion

本文为 crisp bi-Gödel 模态逻辑及其亚相容扩张提供希尔伯特式公理化，证明完备性、PSPACE-完全性，并研究语义性质及框架类对应。

2023-09-04math.LO

Atom-canonicity in algebraic logic in connection to omitting types in modal fragments of L_{ω, ω}

Fix 2<n<ω. Let L_n denote first order logic restricted to the first n variables. CA_n denotes the class of cylindric algebras of dimension n and for m>n, Nr_n\CA_m(\subseteq CA_n) denotes the class of n-neat reducts of CA_m's. The existence of certain finite relation algebras and finite CA_n's lacking relativized complete representations is shown to imply that the omitting types theorem (OTT) fails for L_n with respect to clique guarded semantics (which is an equivalent formalism of its packed fragments), and for the multi-dimensional modal logic S5^n. Several such relation and cylindric algeb…

2016-08-10math.LO