Unified correspondence as a proof-theoretic tool

DOI10.1093/LOGCOM/EXW022MaRDI QIDQ4612445zbMATH OpenOpenAlexFDO

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

Publication date 31 January 2019

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.08204, https://dspace.library.uu.nl/handle/1874/385207

zbMATH Keywords

display calculidistributive lattice expansionsunified correspondenceproperly displayable logics

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05)

Abstract: The present paper 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 nonclassical 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 paper characterize the space of properly displayable DLE-logics.

Recommendations

• Unified correspondence
• Unified correspondence and proof theory for strict implication
• Algorithmic correspondence and canonicity for non-distributive logics
• Algebraic modal correspondence: Sahlqvist and beyond
• Sequent Calculi for Normal Modal Propositional Logics

Cited in

(24)

• Syntactic Completeness of Proper Display Calculi
• Bilattice logic properly displayed
• Intermediate logics admitting a structural hypersequent calculus
• Lambek-Grishin calculus: focusing, display and full polarization
• Proper multi-type display calculi for rough algebras
• Algebraic proof theory for LE-logics
• Modal reduction principles: a parametric shift to graphs
• Sahlqvist via translation
• Subordination algebras as semantic environment of input/output logic
• Disentangling structural connectives or life without display property
• Algebraic modal correspondence: Sahlqvist and beyond
• Unified correspondence and proof theory for strict implication
• Semi De Morgan logic properly displayed
• Non-distributive description logic
• Sequent systems for negative modalities
• Correspondences between classical, intuitionistic and uniform provability
• scientific article; zbMATH DE number 7243670 (Why is no real title available?)
• Labelled calculi for lattice-based modal logics
• Proof spaces for unbounded parallelism
• Abstractions of uniform proofs
• Non-normal modal logics and conditional logics: semantic analysis and proof theory
• Unified correspondence
• Linear Logic Properly Displayed
• Algorithmic correspondence and canonicity for non-distributive logics

This page was built for publication: Unified correspondence as a proof-theoretic tool

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4612445)