Sahlqvist Correspondence Theory for Second-Order Propositional Modal Logic

2021/10/16 by Zhiguang Zhao, Zhao, Zhiguang
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Multi-Agent Systems and Negotiation

paper · pdf · doi:10.48550/arxiv.2110.08561

openalex publication_date 2021/10/16 · openalex created_date 2021/10/25 · openalex updated_date 2026/07/28

Abstract

Modal logic with propositional quantifiers (i.e. second-order propositional modal logic (SOPML)) has been considered since the early time of modal logic. Its expressive power and complexity are high, and its van-Benthem-Rosen theorem and Goldblatt-Thomason theorem have been proved by ten Cate (2006). However, the Sahlqvist theory of SOPML has not been considered in the literature. In the present paper, we fill in this gap. We develop the Sahlqvist correspondence theory for SOPML, which covers and properly extends existing Sahlqvist formulas in basic modal logic. We define the class of Sahlqvist formulas for SOMPL step by step in a hierarchical way, each formula of which is shown to have a first-order correspondent over Kripke frames effectively computable by an algorithm ALBA^SOMPL. In addition, we show that certain Π₂-rules correspond to Π₂-Sahlqvist formulas in SOMPL, which further correspond to first-order conditions, and that even for very simple SOMPL Sahlqvist formulas, they could already be non-canonical.

Related

• Algebraic modal correspondence: Sahlqvist and beyond
• Sahlqvist Correspondence Theory for Sabotage Modal Logic
• Correspondence Theory for Many-valued Modal Logic
• A Sahlqvist-style Correspondence Theorem for Linear-time Temporal Logic
• Minimal modal logics, constructive modal logics and their relations