Unified correspondence as a proof-theoretic tool

Giuseppe Greco, Minghui Ma, Alessandra Palmigiano, Apostolos Tzimoulis, Zhiguang Zhao

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

Fingerprint

Correspondence
Modal Logic
Display devices
Logic
Display
Calculus
Substructural Logics
Syntactics
Non-classical Logics
Hybrid Logic
Algebraic Semantics
μ-calculus
Cut-elimination
Intuitionistic Logic
Classical Logic
Distributive Lattice
Semantics
Axioms
Calculi
Theorem

Keywords

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

Cite this

Greco, Giuseppe ; Ma, Minghui ; Palmigiano, Alessandra ; Tzimoulis, Apostolos ; Zhao, Zhiguang. / Unified correspondence as a proof-theoretic tool. In: Journal of Logic and Computation. 2018 ; Vol. 28, No. 7. pp. 1367-1442.
@article{0415fbb29b4049848650a58d4c4003bc,
title = "Unified correspondence as a proof-theoretic tool",
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.",
keywords = "Display calculi, distributive lattice expansions, properly displayable logics, unified correspondence",
author = "Giuseppe Greco and Minghui Ma and Alessandra Palmigiano and Apostolos Tzimoulis and Zhiguang Zhao",
year = "2018",
month = "10",
day = "1",
doi = "10.1093/logcom/exw022",
language = "English",
volume = "28",
pages = "1367--1442",
journal = "Journal of Logic and Computation",
issn = "0955-792X",
publisher = "Oxford University Press",
number = "7",

}

Unified correspondence as a proof-theoretic tool. / Greco, Giuseppe; Ma, Minghui; Palmigiano, Alessandra; Tzimoulis, Apostolos; Zhao, Zhiguang.

In: Journal of Logic and Computation, Vol. 28, No. 7, 01.10.2018, p. 1367-1442.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Unified correspondence as a proof-theoretic tool

AU - Greco, Giuseppe

AU - Ma, Minghui

AU - Palmigiano, Alessandra

AU - Tzimoulis, Apostolos

AU - Zhao, Zhiguang

PY - 2018/10/1

Y1 - 2018/10/1

N2 - 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.

AB - 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.

KW - Display calculi

KW - distributive lattice expansions

KW - properly displayable logics

KW - unified correspondence

UR - http://www.scopus.com/inward/record.url?scp=85026755602&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85026755602&partnerID=8YFLogxK

U2 - 10.1093/logcom/exw022

DO - 10.1093/logcom/exw022

M3 - Article

VL - 28

SP - 1367

EP - 1442

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

SN - 0955-792X

IS - 7

ER -