Unified correspondence and proof theory for strict implication

DOI10.1093/LOGCOM/EXW012MaRDI QIDQ2983401zbMATH OpenOpenAlexFDO

Authors Minghui Ma, Zhiguang Zhao

Publication date 17 May 2017

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

Full work available at URL https://arxiv.org/abs/1604.08822

zbMATH Keywords

proof theoryregular modal logicssequent calculusstrict implicationunified correspondence

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05)

Abstract: The unified correspondence theory for distributive lattice expansion logics (DLE-logics) is specialized to strict implication logics. As a consequence of a general semantic consevativity result, a wide range of strict implication logics can be conservatively extended to Lambek Calculi over the bounded distributive full non-associative Lambek calculus (BDFNL). Many strict implication sequents can be transformed into analytic rules employing one of the main tools of unified correspondence theory, namely (a suitably modified version of) the Ackermann lemma based algorithm $msfALBA$. Gentzen-style cut-free sequent calculi for BDFNL and its extensions with analytic rules which are transformed from strict implication sequents, are developed.

Recommendations

• Unified correspondence as a proof-theoretic tool
• Sequent Calculi for Some Strict Implication Logics
• Algorithmic correspondence and canonicity for non-distributive logics
• Dual-context sequent calculus and strict implication
• Unified correspondence

Cited in

(9)

• Algorithmic correspondence and canonicity for non-distributive logics
• Residuated expansions of lattice-ordered structures
• THE LOGIC OF RESOURCES AND CAPABILITIES
• Unified correspondence as a proof-theoretic tool
• Sahlqvist via translation
• scientific article; zbMATH DE number 2170850 (Why is no real title available?)
• Constructive canonicity of inductive inequalities
• Unified correspondence
• A System for Strict Implication

Describes a project that uses

Uses Software

• SQEMA

This page was built for publication: Unified correspondence and proof theory for strict implication

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