Sahlqvist correspondence theory for second-order propositional modal logic

被引:0
|
作者
Zhao, Zhiguang [1 ]
机构
[1] Taishan Univ, Sch Math & Stat, Tai An, Shandong, Peoples R China
关键词
correspondence theory; second-order propositional modal logic; ALBA algorithm; Pi(2)-rules; canonicity; S5;
D O I
10.1093/logcom/exac036
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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, J Philos. Logic, 35, 209-223). 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 SO PM L, 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 Pi(2)-rules correspond to Pi(2)-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.
引用
收藏
页码:577 / 598
页数:22
相关论文
共 50 条
  • [21] Expressive power of monadic second-order logic and modal μ-calculus
    Rohde, P
    AUTOMATA, LOGICS, AND INFINITE GAMES: A GUIDE TO CURRENT RESEARCH, 2002, 2500 : 239 - 257
  • [22] A Sahlqvist theorem for distributive modal logic
    Gehrke, M
    Nagahashi, H
    Venema, Y
    ANNALS OF PURE AND APPLIED LOGIC, 2005, 131 (1-3) : 65 - 102
  • [23] Pedagogical second-order propositional calculi
    Colson, Loic
    Michel, David
    JOURNAL OF LOGIC AND COMPUTATION, 2008, 18 (04) : 669 - 695
  • [24] Sahlqvist Correspondence for Modal mu-calculus
    Johan van Benthem
    Nick Bezhanishvili
    Ian Hodkinson
    Studia Logica, 2012, 100 : 31 - 60
  • [25] Quantified propositional calculus and a second-order theory for NC1
    Stephen Cook
    Tsuyoshi Morioka
    Archive for Mathematical Logic, 2005, 44 : 711 - 749
  • [26] Quantified propositional calculus and a second-order theory for NC1
    Cook, S
    Morioka, T
    ARCHIVE FOR MATHEMATICAL LOGIC, 2005, 44 (06) : 711 - 749
  • [27] Sahlqvist Correspondence for Modal mu-calculus
    van Benthem, Johan
    Bezhanishvili, Nick
    Hodkinson, Ian
    STUDIA LOGICA, 2012, 100 (1-2) : 31 - 60
  • [28] Pure Second-Order Logic with Second-Order Identity
    Paseau, Alexander
    NOTRE DAME JOURNAL OF FORMAL LOGIC, 2010, 51 (03) : 351 - 360
  • [29] On the existence of a modal-logical basis for monadic second-order logic
    Hella, Lauri
    Tulenheimo, Tero
    JOURNAL OF LOGIC AND COMPUTATION, 2013, 23 (01) : 157 - 180
  • [30] Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
    Strassburger, Lutz
    TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2009, 5608 : 309 - 324