Unified correspondence as a proof-theoretic tool

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

The present article aims at establishing formal connections between correspondence phenomena, well known from the area of modal logic, and the theory of display calculi, originated by Belnap. These connections have been seminally observed and exploited by Marcus Kracht, in the context of his characterization of the modal axioms (which he calls primitive formulas) which can be effectively transformed into 'analytic'structural rules of display calculi. In this context, a rule is 'analytic'if adding it to a display calculus preserves Belnap's cut-elimination theorem. In recent years, the state-of-the-art in correspondence theory has been uniformly extended from classical modal logic to diverse families of non-classical logics, ranging from (bi-)intuitionistic (modal) logics, linear, relevant and other substructural logics, to hybrid logics and mu-calculi. This generalization has given rise to a theory called unified correspondence, the most important technical tools of which are the algorithm ALBA, and the syntactic characterization of Sahlqvist-type classes of formulas and inequalities which is uniform in the setting of normal DLE-logics (logics the algebraic semantics of which is based on bounded distributive lattices). We apply unified correspondence theory, with its tools and insights, to extend Kracht's results and prove his claims in the setting of DLE-logics. The results of the present article characterize the space of properly displayable DLE-logics.

Original languageEnglish
Pages (from-to)1367-1442
Number of pages76
JournalJournal of Logic and Computation
Volume28
Issue number7
DOIs
Publication statusPublished - 1 Oct 2018

Funding

The research of the Giuseppe Greco, Alessandra Palmigiano, Apostolos Tzimoulis and Zhiguang Zhao has been made possible by the NWO Vidi grant 016.138.314, by the NWO Aspasia grant 015.008.054, and by a Delft Technology Fellowship awarded in 2013. The research of Minghui Ma is supported by the China national funding of social sciences (grant no.12CZ054). We would like to thank Agata Ciabattoni for inviting three of the authors to a research visit to her group in Vienna. The feedback and questions we received from her and Revantha Ramanayake during this visit significantly improved the paper.

FundersFunder number
Nederlandse Organisatie voor Wetenschappelijk Onderzoek015.008.054, 016.138.314
Chinese National Funding of Social Sciences12CZ054

    Keywords

    • Display calculi
    • distributive lattice expansions
    • properly displayable logics
    • unified correspondence

    Fingerprint

    Dive into the research topics of 'Unified correspondence as a proof-theoretic tool'. Together they form a unique fingerprint.

    Cite this