Algorithmic Correspondence and Canonicity for Non-Classical Logics (Abstract of Invited Talk)

Abstract

In this talk I give an overview of the work on algorithmic approaches to correspondence and canonicity for non-classical logics in which I have been involved over the past decade, and which has evolved into the research programme now being called 'unified correspondence'. In the first part I will discuss work that was a collaboration with Valentin Goranko and Dimiter Vakarelov, while the second part details work with Alessandra Palmigiano and a number of other collaborators. Sahlqvist Theory. As is well known, every modal formula defines a secondorder property of Kripke frames. Sahlqvist's famous theorem [31] gives a syntactic definition of a class of modal formulas, the Sahlqvist formulas, each of which defines an first-order class of frames and is canonical. Over the years, many extensions, variations and analogues of this result have appeared, including alternative proofs in e.g. [32], generalizations to arbitrary modal signatures [30], variations of the correspondence language [28, 1], Sahlqvist-type results for hybrid logics [4], various substructural logics [26, 18, 21], mu-calculus [2], and enlargements of the Sahlqvist class to e.g. the inductive formulas of [24], to mention but a few. Another natural approach to the modal correspondence problem is to apply second-order quantifier elimination algorithms to the frame-translations of modal formulas. It has been shown, for example, that the algorithms SCAN [20] and DLS [17] both succeed in computing first-order equivalents for all Sahqvist formulas [23, 5]. SQEMA. SQEMA is an acronym for Second-Order Quantifier elimination in Modal logic using Ackernann's Lemma. As this would suggest, SQEMA is related to DLS in its use of the Ackermann lemma as the engine for eliminating predicate variables and of equivalence preserving rewrite-rules to prepare formulas for the application of the former. A major difference, however, is that SQEMA is specifically targeted at propositional modal logics which it does not translate into second-order logic, but manipulates directly. However, modal logic itself cannot express the required equivalences, formulated as rewrite rules, so an enriched hybrid language with inverse (temporal) modalities is required. SQEMA is strong enough to compute first-order correspondents for at least all inductive formulas. Perhaps more surprisingly, it is possible to extract a proof of canonicity (in Copyright c 2017 by the paper's authors In: P. Koopmann, S. Rudolph, R. Schmidt, C. Wernhard (eds.): SOQE 2017 { Proceedings of the Workshop on Second-Order Quanti er Elimination and Related Topics, Dresden, Germany, December 6{8, 2017, published at http://ceur-ws.org.

-

the form of d-persistence) for every formula on which SQEMA succeeds [ 11 ]. Schmidt has introduced another algorithm based on Ackermann’s Lemma which is optimized for implementation purposes [ 33 ].

Extensions of SQEMA. SQEMA extends in an unproblematic way to polyadic (purely) modal languages and hybrid languages [ 12 ]. Extensions using a recursive version of the Ackermann lemma enable SQEMA to find correspondents in first-order logic with least fixed points for some non-elementary modal formulas like the L¨ob formula [ 10 ]. Relaxing the syntactic requirement of positivity in the Ackermann rule to monotonicity, yields a more general ‘semantic’ algorithm [ 9 ]. Including various substitution rules results in an extension of SQEMA [ 13 ] that can handle all Vakaralov’s complex formulas [ 34 ].

ALBA. SQEMA and its variations are applicable to (extensions of) modal logics based on classical propositional logic. The distributive modal logic of Gehrke, Nagahashi and Venema [ 22 ] is similar to intuitionistic modal logic but lacks the implication, and has four unary modalities, which can be though of as ‘possibly’, ‘necessarily’, ‘possibly not’ and ‘necessarily not’. Distributive lattices with operators provide the algebraic semantics for this logic which a discrete duality links to Kripke frames enriched with partial ordering relations. The ALBA algorithm [ 14 ] (an acronym for Ackermann Lemma Based Algorithm) is a successor of SQEMA which is adapted to this setting. The loss of classical negation has far reaching consequences requiring major changes and making ALBA a distinctively different algorithm from SQEMA. Simultaneously, the move to this more general environment helps to clarify the essentially order-theoretic and algebraic nature of the properties underlying Salhqvist’s theorem and algorithms like SQEMA and ALBA.

Unified Correspondence. These insights are explored and developed in [ 8 ] as a framework for unifying disparate correspondence and canonicity results in the literature and as a methodology for formulating and proving new ones in a wide range of logics. One of the most general instances of this is a Sahlqvist-style result for logics with algebraic semantics based on possibly non-distributive lattices with operators exhibiting a wide range of order-theoretic behaviours [ 15 ]. Giving up distributivity results in the original ALAB algorithm’s strategy becoming unsound in significant aspects. This calls for a new approach where formulas are no longer decomposed connective-by-connective, but where their order-theoretic properties (as term functions on algebras) determine the applicability of rules which extract subformulas directly. This framework covers many well known logics including the Full Lambek and Lambek calculus, (co- and bi-) intuitionistic multi-modal logic, Prior’s MIPC and Dunn’s Positive Modal Logic. Furthermore, normality of modal operators is by no means a prerequisite for the unified correspondence approach to work, as is shown in [ 29 ]. Extensions of ALBA. Although the results for possibly non-distributive logics outlined in the previous paragraph are very general, the particular features of many logics require special treatment and therefore customised versions of ALBA and bespoke realizations of the unified correspondence paradigm. These include mu-calculi, already studied from a Sahlqvist-theoretic perspective in [ 2 ], where the presence of fixed-point binders significantly complicates the order theoretic considerations and requires special rules [ 6, 7 ]. Hybrid logics pose no problem as far as correspondence is concerned, since nominals and the other typical syntactic machinery do not introduce second-order quantification, but canonicity and completeness results require innovative treatment [ 16 ]. Correspondence for many-valued modal logic is easy to obtain once ALBA is seen to be applicable via an appropriate algebraic duality [ 3 ].

Other Applications of Unified Correspondence. Although the original purpose of SQEMA and ALBA is to eliminate second-order quantifiers, the fact that they both also guarantee canonicity already indicates that their usefulness goes beyond this. Other such applications include the dual characterizations of classes of finite lattices [ 19 ], the identification of the syntactic shape of axioms which can be translated into structural rules of a proper display calculus [ 25 ] and of internal Gentzen calculi for the logics of strict implication [ 27 ].

References

1. van Benthem, J. : Modal frame correspondences and fixed-points . Studia Logica 83 ( 1-3 ), 133 - 155 ( 2006 )

2. van Benthem, J. , Bezhanishvili , N. , Hodkinson , I. : Sahlqvist correspondence for modal mu-calculus . Studia Logica 100 ( 1-2 ), 31 - 60 ( 2012 )

3. Britz , C. : Correspondence theory in many-valued modal logics . Master's thesis , University of Johannesburg, South Africa ( 2016 )

4. ten Cate, B. , Marx , M. , Viana , J.P. : Hybrid logics with Sahlqvist axioms . Logic Journal of the IGPL (3) , 293 - 300 ( 2006 )

5. Conradie , W.: On the strength and scope of DLS . Journal of Applied Non-Classical Logics 16 ( 3-4 ), 279 - 296 ( 2006 )

6. Conradie , W. , Craig , A. : Canonicity results for mu-calculi: an algorithmic approach . Journal of Logic and Computation 27 ( 3 ), 705 - 748 ( 2017 )

7. Conradie , W. , Fomatati , Y. , Palmigiano , A. , Sourabh , S. : Algorithmic correspondence for intuitionistic modal mu-calculus . Theoretical Computer Science 564 , 30 - 62 ( 2015 ), http://www.sciencedirect.com/science/article/pii/S0304397514008196

8. Conradie , W. , Ghilardi , S. , Palmigiano , A. : Unified correspondence . In: Baltag, A. , Smets , S. (eds.) Johan van Benthem on Logic and Information Dynamics , Outstanding Contributions to Logic, vol. 5 , pp. 933 - 975 . Springer International Publishing ( 2014 )

9. Conradie , W. , Goranko , V. : Algorithmic correspondence and completeness in modal logic IV: Semantic extensions of SQEMA . Journal of Applied Non-Classical Logics 18 ( 2-3 ), 175 - 211 ( 2008 )

10. Conradie , W. , Goranko , V. , Vakarelov , D. : Algorithmic correspondence and completeness in modal logic. v. recursive extensions of sqema . Journal of Applied Logic 8 ( 4 ), 319 - 333 ( 2010 )

11. Conradie , W. , Goranko , V. , Vakarelov , D. : Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA. Logical Methods in Computer Science ( 2006 )

12. Conradie , W. , Goranko , V. , Vakarelov , D. : Algorithmic correspondence and completeness in modal logic. II. Polyadic and hybrid extensions of the algorithm SQEMA . Journal of Logic and Computation 16 ( 5 ), 579 - 612 ( 2006 )

13. Conradie , W. , Goranko , V. , Vakarelov , D. : Algorithmic correspondence and completeness in modal logic. III. extensions of the algorithm SQEMA with substitutions . Fundamenta Informaticae 92 ( 4 ), 307 - 343 ( 2009 )

14. Conradie , W. , Palmigiano , A. : Algorithmic correspondence and canonicity for distributive modal logic . Annals of Pure and Applied Logic 163 ( 3 ), 338 - 376 ( 2012 )

15. Conradie , W. , Palmigiano , A. : Algorithmic correspondence and canonicity for nondistributive logics (Submitted ArXiv preprint 160308515 )

16. Conradie , W. , Robinson , C. : On Sahlqvist theory for hybrid logic . Journal of Logic and Computation 27 ( 3 ), 867 - 900 ( 2017 )

17. Doherty , P. , Lukaszewicz , W. , Szalas , A. : Computing circumscription revisited: A reduction algorithm . Journal of Automated Reasoning 18 ( 3 ), 297 - 336 ( 1997 )

18. Dunn , M. , Gehrke , M. , Palmigiano , A. : Canonical extensions and relational completeness of some substructural logics . Journal of Symbolic Logic 70 ( 3 ), 713 - 740 ( 2005 )

19. Frittella , S. , Palmigiano , A. , Santocanale , L. : Dual characterizations for finite lattices via correspondence theory for monotone modal logic . Journal of Logic and Computation 27 ( 3 ), 639 - 678 ( 2017 )

20. Gabbay , D.M. , Ohlbach , H.J.: Quantifier elimination in second-order predicate logic . South African Computer Journal 7 , 35 - 43 ( 1992 )

21. Gehrke , M. : Generalized Kripke frames . Studia Logica 84 ( 2 ), 241 - 275 ( 2006 )

22. Gehrke , M. , Nagahashi , H. , Venema , Y. : A Sahlqvist theorem for distributive modal logic . Annals of Pure and Applied Logic 131 ( 1-3 ), 65 - 102 ( 2005 )

23. Goranko , V. , Hustadt , U. , Schmidt , R.A. , Vakarelov , D. : SCAN is complete for all Sahlqvist formulae . In: Berghammer, R. , M¨oller, B. , Struth , G . (eds.) Revised Selected Papers of the 7th International Seminar on Relational Methods in Computer Science and the 2nd International Workshop on Applications of Kleene Algebra , Bad Malente, Germany, May 12-17, 2003 . pp. 149 - 162 . Springer ( 2004 )

24. Goranko , V. , Vakarelov , D. : Elementary canonical formulae: Extending Sahlqvist's theorem . Annals of Pure and Applied Logic 141 ( 1-2 ), 180 - 217 ( 2006 )

25. Greco , G. , Ma, M. , Palmigiano , A. , Tzimoulis , A. , Zhao , Z. : Unified correspondence as a proof-theoretic tool . Journal of Logic and Computation ( 2016 , doi: 101093/logcom/exw022 ArXiv preprint 160308204)

26. Kurtonina , N.: Categorical inference and modal logic . Journal of Logic, Language, and Information 7 ( 1998 )

27. Ma , M. , Zhao , Z. : Unified correspondence and proof theory for strict implication . Journal of Logic and Computation 27 ( 3 ), 921 - 960 ( 2017 )

28. Ohlbach , H.J. , Schmidt , R.A. : Functional translation and second-order frame properties of modal logics . Journal of Logic and Computation 7 ( 5 ), 581 - 603 ( 1997 )

29. Palmigiano , A. , Sourabh , S. , Zhao , Z. : Sahlqvist theory for impossible worlds . Journal of Logic and Computation 27 ( 3 ), 775 - 816 ( 2017 )

30. de Rijke, M. , Venema , Y. : Sahlqvist's theorem for Boolean algebras with operators with an application to cylindric algebras . Studia Logica 54 ( 1 ), 61 - 78 ( 1995 )

31. Sahlqvist , H.: Completeness and correspondence in the first and second order semantics for modal logic . In: Kanger, S . (ed.) Studies in Logic and the Foundations of Mathematics , vol. 82 , pp. 110 - 143 . North-Holland, Amsterdam ( 1975 )

32. Sambin , G. , Vaccaro , V.: A new proof of Sahlqvist's theorem on modal definability and completeness . Journal of Symbolic Logic 54 ( 3 ), 992 - 999 ( 1989 )

33. Schmidt , R.A. : The Ackermann approach for modal logic, correspondence theory and second-order reduction . Journal of Applied Logic 10 ( 1 ), 52 - 74 ( 2012 )

34. Vakarelov , D. : Modal definability in languages with a finite number of propositional variables, and a new extention of the Sahlqvist class . In: Advances in Modal Logic , vol. 4 , pp. 495 - 518 . King's College Publications ( 2003 )