Algorithmic Correspondence and Canonicity for Non-Classical Logics WillemConradie University of Johannesburg
South Africa
Order Quantifier Elimination and Related Topics
December 6-8 2017 Dresden Germany
Algorithmic Correspondence and Canonicity for Non-Classical Logics 83F2B028707A42C02165AF9B3C4807D6 GROBID - A machine learning software for extracting information from scholarly documents

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 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öb 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].

Modal frame correspondences and fixed-points JVan Benthem Studia Logica 83 1-3 2006 Sahlqvist correspondence for modal mu-calculus JVan Benthem NBezhanishvili IHodkinson Studia Logica 100 1-2 2012 Correspondence theory in many-valued modal logics CBritz 2016 University of Johannesburg, South Africa Master's thesis Hybrid logics with Sahlqvist axioms BTen Cate MMarx JPViana Logic Journal of the IGPL 3 2006 On the strength and scope of DLS WConradie Journal of Applied Non-Classical Logics 16 3-4 2006 Canonicity results for mu-calculi: an algorithmic approach WConradie ACraig Journal of Logic and Computation 27 3 2017 Algorithmic correspondence for intuitionistic modal mu-calculus WConradie YFomatati APalmigiano SSourabh Theoretical Computer Science 564 2015 Unified correspondence WConradie SGhilardi APalmigiano Johan van Benthem on Logic and Information Dynamics, Outstanding Contributions to Logic ABaltag SSmets Springer International Publishing 2014 5 Algorithmic correspondence and completeness in modal logic IV: Semantic extensions of SQEMA WConradie VGoranko Journal of Applied Non-Classical Logics 18 2-3 2008 Algorithmic correspondence and completeness in modal logic. v. recursive extensions of sqema WConradie VGoranko DVakarelov Journal of Applied Logic 8 4 2010 Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA WConradie VGoranko DVakarelov Logical Methods in Computer Science 2006 Algorithmic correspondence and completeness in modal logic. II. Polyadic and hybrid extensions of the algorithm SQEMA WConradie VGoranko DVakarelov Journal of Logic and Computation 16 5 2006 Algorithmic correspondence and completeness in modal logic. III. extensions of the algorithm SQEMA with substitutions WConradie VGoranko DVakarelov Fundamenta Informaticae 92 4 2009 Algorithmic correspondence and canonicity for distributive modal logic WConradie APalmigiano Annals of Pure and Applied Logic 163 3 2012 Algorithmic correspondence and canonicity for nondistributive logics WConradie APalmigiano Submitted ArXiv preprint 160308515 On Sahlqvist theory for hybrid logic WConradie CRobinson Journal of Logic and Computation 27 3 2017 Computing circumscription revisited: A reduction algorithm PDoherty WLukaszewicz ASzalas Journal of Automated Reasoning 18 3 1997 Canonical extensions and relational completeness of some substructural logics MDunn MGehrke APalmigiano Journal of Symbolic Logic 70 3 2005 Dual characterizations for finite lattices via correspondence theory for monotone modal logic SFrittella APalmigiano LSantocanale Journal of Logic and Computation 27 3 2017 Quantifier elimination in second-order predicate logic DMGabbay HJOhlbach South African Computer Journal 7 1992 Generalized Kripke frames MGehrke Studia Logica 84 2 2006 A Sahlqvist theorem for distributive modal logic MGehrke HNagahashi YVenema Annals of Pure and Applied Logic 131 1-3 2005 SCAN is complete for all Sahlqvist formulae VGoranko UHustadt RASchmidt DVakarelov Revised Selected Papers of the 7th International Seminar on Relational Methods in Computer Science and the 2nd International Workshop on Applications of Kleene Algebra RBerghammer BMöller GStruth
Bad Malente, Germany
 Springer May 12-17, 2003. 2004 Elementary canonical formulae: Extending Sahlqvist's theorem VGoranko DVakarelov Annals of Pure and Applied Logic 141 1-2 2006 Unified correspondence as a proof-theoretic tool GGreco MMa APalmigiano ATzimoulis ZZhao doi: 101093/logcom/exw022 Journal of Logic and Computation 2016 ArXiv preprint 160308204 Categorical inference and modal logic NKurtonina Journal of Logic, Language, and Information 7 1998 Unified correspondence and proof theory for strict implication MMa ZZhao Journal of Logic and Computation 27 3 2017 Functional translation and second-order frame properties of modal logics HJOhlbach RASchmidt Journal of Logic and Computation 7 5 1997 Sahlqvist theory for impossible worlds APalmigiano SSourabh ZZhao Journal of Logic and Computation 27 3 2017 Sahlqvist's theorem for Boolean algebras with operators with an application to cylindric algebras MDe Rijke YVenema Studia Logica 54 1 1995 Completeness and correspondence in the first and second order semantics for modal logic HSahlqvist Studies in Logic and the Foundations of Mathematics SKanger
Amsterdam
 North-Holland 1975 82 A new proof of Sahlqvist's theorem on modal definability and completeness GSambin VVaccaro Journal of Symbolic Logic 54 3 1989 The Ackermann approach for modal logic, correspondence theory and second-order reduction RASchmidt Journal of Applied Logic 10 1 2012 Modal definability in languages with a finite number of propositional variables, and a new extention of the Sahlqvist class DVakarelov Advances in Modal Logic King's College Publications 2003 4