A note on the complexity of S4.2. Issue 2 (3rd April 2021)

• Record Type: Journal Article
• Authors: Chalki, Aggeliki; Koutras, Costas D.; Zikos, Yorgos
• Is Part Of: Journal of applied non-classical logics. Volume 31:Issue 2(2021)
• Page Start: 108
• Page End: 129
• Publication Date: 2021-04-03
• Subjects: Modal logic -- complexity of multimodal logics -- S4.2 logic -- tableaux proof procedures; Nonclassical mathematical logic -- Periodicals; Wiskundige logica; Logic; Periodicals; 511.3105
• DOI: 10.1080/11663081.2021.1901560
• Languages: English
• ISSNs: 1166-3081

Abstract

Abstract : S 4.2 is the modal logic of directed partial pre-orders and/or the modal logic of reflexive and transitive relational frames with a final cluster . It holds a distinguished position in philosophical logic, where it has been advocated as the 'correct' logic of knowledge; it has also found interesting applications in the temporal logic of relativistic spacetime and the metamathematics of forcing in set theory. The satisfiability problem for S 4.2 is P S P A C E -complete: this is a result established in an AiML 2004 paper of Shapirovsky [(2004). On PSPACE-decidability in transitive modal logic. In R. A. Schmidt, I. Pratt-Hartmann, M. Reynolds, & H. Wansing (Eds.), Advances in modal logic 5 (pp. 269–287). King's College Publications] where the complexity classification of S 4.2 emerges as a consequence of a very general method for constructing P S P A C E decision procedures for transitive modal logics. We provide here a 'classical' proof in the standard Halpern-Moses style of Halpern and Moses [(1992). A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54 (2), 319–379]. With little extra work, it is shown that the P S P A C E -completeness result extends to S 4.2 n, the multimodal version of S 4.2 . We prove that the P S P A C E -completeness characterisation of monomodal S 4.2 persists even if we restrict ourselves to fragments with bounded modal depth, but the problem is N P -complete when it is restricted to formulae with modal depth at most one. The complexity of S 4.2 satisfiability for the fragment of the language with a finite number of propositional variables (but unbounded modal depth) remains P S P A C E -hard. For a finite language and bounded modal depth, S 4.2 -satisfiability can be checked in linear time.