=Paper=
{{Paper
|id=Vol-2013/paper2
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2013/paper2.pdf
|volume=Vol-2013
}}
==None==
https://ceur-ws.org/Vol-2013/paper2.pdf
2
Algorithmic Correspondence and Canonicity for
Non-Classical Logics
(Abstract of Invited Talk)
Willem Conradie
University of Johannesburg, South Africa
In this talk I give an overview of the work on algorithmic approaches to corre-
spondence 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 second-
order property of Kripke frames. Sahlqvist’s famous theorem [31] gives a syn-
tactic 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, includ-
ing 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 en-
largements 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 – Pro-
ceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics,
Dresden, Germany, December 6–8, 2017, published at http://ceur-ws.org.
3
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 recur-
sive 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 log-
ics 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 ‘possi-
bly’, ‘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 algo-
rithm [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 dis-
tinctively different algorithm from SQEMA. Simultaneously, the move to this
more general environment helps to clarify the essentially order-theoretic and al-
gebraic 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 lat-
tices with operators exhibiting a wide range of order-theoretic behaviours [15].
Giving up distributivity results in the original ALAB algorithm’s strategy be-
coming 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 appli-
cability 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].
4
Extensions of ALBA. Although the results for possibly non-distributive log-
ics 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 syn-
tactic 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 ap-
proach. Journal of Logic and Computation 27(3), 705–748 (2017)
7. Conradie, W., Fomatati, Y., Palmigiano, A., Sourabh, S.: Algorithmic correspon-
dence 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 com-
pleteness in modal logic. v. recursive extensions of sqema. Journal of Applied Logic
8(4), 319–333 (2010)
5
11. Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and com-
pleteness in modal logic. I. The core algorithm SQEMA. Logical Methods in Com-
puter Science (2006)
12. Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and com-
pleteness 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 com-
pleteness in modal logic. III. extensions of the algorithm SQEMA with substitu-
tions. Fundamenta Informaticae 92(4), 307–343 (2009)
14. Conradie, W., Palmigiano, A.: Algorithmic correspondence and canonicity for dis-
tributive modal logic. Annals of Pure and Applied Logic 163(3), 338 – 376 (2012)
15. Conradie, W., Palmigiano, A.: Algorithmic correspondence and canonicity for non-
distributive 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 com-
pleteness of some substructural logics. Journal of Symbolic Logic 70(3), 713–740
(2005)
19. Frittella, S., Palmigiano, A., Santocanale, L.: Dual characterizations for finite lat-
tices 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öller, B., Struth, G. (eds.) Revised Se-
lected 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 correspon-
dence 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 prop-
erties 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 se-
mantics for modal logic. In: Kanger, S. (ed.) Studies in Logic and the Foundations
of Mathematics, vol. 82, pp. 110–143. North-Holland, Amsterdam (1975)
6
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)