106 Algorithmic Correspondence and Canonicity for Possibility Semantics (Abstract) Zhiguang Zhao Delft University of Technology, Netherlands Unified Correspondence. Correspondence and completeness theory have a long history in modal logic, and they are referred to as the “three pillars of wisdom supporting the edifice of modal logic” [22, page 331] together with duality theory. Dating back to [20,21], the Sahlqvist theorem gives a syntactic definition of a class of modal formulas, the Sahlqvist class, each member of which defines an elementary (i.e. first-order definable) class of Kripke frames and is canonical. Since modal logic on the frame level is essentially second-order, computing the first-order correspondence of a modal formula is a kind of second-order quantifier elimination. Recently, a uniform and modular theory which subsumes the above results and extends them to logics with a non-classical propositional base has emerged, and has been dubbed unified correspondence [5]. It is built on duality-theoretic insights [9] and uniformly exports the state-of-the-art in Sahlqvist theory from normal modal logic to a wide range of logics which include, among others, intu- itionistic and distributive and general (non-distributive) lattice-based (modal) logics [6,8], non-normal (regular) modal logics based on distributive lattices of arbitrary modal signature [19], hybrid logics [12], many valued logics [16] and bi-intuitionistic and lattice-based modal mu-calculus [1,3,2]. Unified correspon- dence theory has two components: the first one is a very general syntactic defini- tion of Sahlqvist and inductive formulas, which applies uniformly to each logical signature and is given purely in terms of the order-theoretic properties of the algebraic interpretations of the logical connectives; the second one is the Acker- mann lemma based algorithm ALBA, which is a generalization of SQEMA based on order-theoretic and algebraic insights, which effectively computes first-order correspondents of input formulas/inequalities, and is guaranteed to succeed on the Sahlqvist and inductive classes of formulas/inequalities. The algorithm aims at eliminating all propositional variables, which are, on the relational seman- tics side, second-order variables, and rewrite the formula into a quasi-inequality which contains only nominals and co-nominals, which are, on the relational se- mantics side, essentially first-order. In this sense, unified correspondence theory is essentially second-order quantifier elimination on the algebraic side. The breadth of this work has stimulated many and varied applications. Some are closely related to the core concerns of the theory itself, such as understanding the relationship between different methodologies for obtaining canonicity results [18,7], the phenomenon of pseudocorrespondence [10], and the investigation of 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. 107 the extent to which the Sahlqvist theory of classes of normal distributive lattice expansions can be reduced to the Sahlqvist theory of normal Boolean algebra expansions, by means of Gödel-type translations [11]. Other, possibly surpris- ing applications include the dual characterizations of classes of finite lattices [13], the identification of the syntactic shape of axioms which can be translated into structural rules of a proper display calculus [14] and of internal Gentzen calculi for the logics of strict implication [17], and the epistemic interpretation of lattice-based modal logic in terms of categorization theory in management science [4]. These and other results (cf. [9]) form the body of a theory called uni- fied correspondence [5], a framework within which correspondence results can be formulated and proved abstracting away from specific logical signatures, us- ing only the order-theoretic properties of the algebraic interpretations of logical connectives. Possibility Semantics. Possibility semantics for modal logic is a generaliza- tion of standard Kripke semantics. In this semantics, a possibility frame has a refinement relation which is a partial order between states, in addition to the ac- cessibility relation for modalities. From an algebraic perspective, full possibility frames are dually equivalent to complete Boolean algebras with complete oper- ators which are not necessarily atomic, while filter-descriptive possibility frames are dually equivalent to Boolean algebras with operators. In recent years, the theoretic study of possibility semantics has received more attention. In [23], Yamamoto investigates the correspondence theory in possibil- ity semantics in a frame-theoretic way and prove a Sahlqvist-type correspon- dence theorem over full possibility frames, which are the possibility semantic counterpart of Kripke frames, using insights from the algebraic understanding of possibility semantics. In [15, Theorem 7.20], it is shown that all inductive formulas are filter-canonical and hence every normal modal logic axiomatized by inductive formulas is sound and complete with respect to its canonical full possibility frame. However, the correspondence result for inductive formulas is still missing, as well as the correspondence result over filter-descriptive possibil- ity frames (see [15, page 103]) and soundness and completeness with respect to the corresponding elementary class of full possibility frames. The present paper aims at giving a closer look at the aforementioned unsolved problems using the algebraic and order-theoretic insights from a current ongoing research project, namely unified correspondence. Methodology. Our contribution is methodological: we analyze the correspon- dence phenomenon in possibility semantics using the dual algebraic structures, namely complete (not necessarily atomic) Boolean algebras with complete op- erators, where the atoms are not always available. For the correspondence over full possibility frames, our strategy is to identify two different Boolean algebras with operators as the dual algebraic structures of the possibility frame, namely the Boolean algebra of regular open subsets BRO (when viewing the possibility frame as a possibility frame itself) and the Boolean algebra of arbitrary subsets 108 BFull (when viewing the possibility frame as a bimodal Kripke frame), where a canonical order-embedding map e : BRO → BFull can be defined. The embedding e preserves arbitrary meets, therefore a left adjoint c : BFull → BRO of e can be defined, which sends a subset X of the domain W of possibilities to the smallest regular open subset containing X. This left adjoint c plays an important role in the dual characterization of the interpretations of the expanded language, which form the ground of the regular open translation, i.e. the counterpart of standard translation in possibility semantics. When it comes to canonicity, we use the fact that filter-canonicity is equivalent to constructive canonicity [15, Theorem 5.46, 7.20], and prove a topological Ackermann lemma, which justifies the soundness of propositional variable elimination rules and forms the basis of the correspon- dence result with respect to the class of filter-descriptive frames as well as the canonicity and completeness result with respect to the corresponding class of full possibility frames. References 1. W. Conradie and A. Craig. Canonicity results for mu-calculi: an algorithmic approach. Journal of Logic and Computation, Forthcoming. ArXiv preprint arXiv:1408.6367. 2. W. Conradie, A. Craig, A. Palmigiano, and Z. Zhao. Constructive canonicity for lattice-based fixed point logics. Submitted. ArXiv preprint arXiv:1603.06547. 3. W. Conradie, Y. Fomatati, A. Palmigiano, and S. Sourabh. Algorithmic corre- spondence for intuitionistic modal mu-calculus. Theoretical Computer Science, 564:30–62, 2015. 4. W. Conradie, S. Frittella, A. Palmigiano, M. Piazzai, A. Tzimoulis, and N. Wijn- berg. Categories: How I learned to stop worrying and love two sorts. Proceedings of WoLLIC 2016, ArXiv preprint 1604.00777. 5. W. Conradie, S. Ghilardi, and A. Palmigiano. Unified correspondence. In A. Baltag and S. Smets, editors, Johan van Benthem on Logic and Information Dynamics, volume 5 of Outstanding Contributions to Logic, pages 933–975. Springer Interna- tional Publishing, 2014. 6. W. Conradie and A. Palmigiano. Algorithmic correspondence and canonicity for distributive modal logic. Annals of Pure and Applied Logic, 163(3):338 – 376, 2012. 7. W. Conradie and A. Palmigiano. Constructive canonicity of inductive inequalities. Submitted. ArXiv preprint 1603.08341. 8. W. Conradie and A. Palmigiano. Algorithmic correspondence and canonicity for non-distributive logics. Submitted. ArXiv preprint 1603.08515. 9. W. Conradie, A. Palmigiano, and S. Sourabh. Algebraic modal correspondence: Sahlqvist and beyond. Submitted. ArXiv preprint 1606.06881. 10. W. Conradie, A. Palmigiano, S. Sourabh, and Z. Zhao. Canonicity and relativized canonicity via pseudo-correspondence: an application of ALBA. Submitted. ArXiv preprint 1511.04271. 11. W. Conradie, A. Palmigiano, and Z. Zhao. Sahlqvist via translation. Submitted. ArXiv preprint 1603.08220. 12. W. Conradie and C. Robinson. On Sahlqvist theory for hybrid logic. Journal of Logic and Computation, 2015. doi: 10.1093/logcom/exv045. 109 13. S. Frittella, A. Palmigiano, and L. Santocanale. Dual characterizations for finite lattices via correspondence theory for monotone modal logic. Journal of Logic and Computation, 2016. doi:10.1093/logcom/exw011. 14. G. Greco, M. Ma, A. Palmigiano, A. Tzimoulis, and Z. Zhao. Unified correspon- dence as a proof-theoretic tool. Journal of Logic and Computation, 2016. doi: 10.1093/logcom/exw022. ArXiv preprint 1603.08204. 15. W. Holliday. Possibility frames and forcing for modal logic. UC Berkeley Working Paper in Logic and the Methodology of Science, June 2016. URL http://escholarship.org/uc/item/9v11r0dq. 16. C. le Roux. Correspondence theory in many-valued modal logics. Master’s thesis, University of Johannesburg, South Africa, 2016. 17. M. Ma and Z. Zhao. Unified correspondence and proof theory for strict implica- tion. Journal of Logic and Computation, 2016. doi: 10.1093/logcom/exw012. ArXiv preprint 1604.08822. 18. A. Palmigiano, S. Sourabh, and Z. Zhao. Jónsson-style canonicity for ALBA- inequalities. Journal of Logic and Computation, 2015. doi:10.1093/logcom/exv041. 19. A. Palmigiano, S. Sourabh, and Z. Zhao. Sahlqvist theory for impossible worlds. Journal of Logic and Computation, 2016. doi:10.1093/logcom/exw014. 20. H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logic. In Studies in Logic and the Foundations of Mathematics, volume 82, pages 110–143. 1975. 21. J. van Benthem. Modal logic and classical logic. Bibliopolis, 1983. 22. J. van Benthem. Correspondence theory. In D. M. Gabbay and F. Guenthner, editors, Handbook of philosophical logic, volume 3, pages 325–408. Kluwer Academic Publishers, 2001. 23. K. Yamamoto. Modal correspondence theory for possibility semantics. UC Berkeley Working Paper in Logic and the Methodology of Science, 2016. URL http://escholarship.org/uc/item/7t12914n.