Intuitionistic Sahlqvist theory for deductive systems
arXiv:2208.00691 · doi:10.1017/jsl.2023.7
Abstract
Sahlqvist theory is extended to the fragments of the intuitionistic propositional calculus that include the conjunction connective. This allows us to introduce a Sahlqvist theory of intuitionistic character amenable to arbitrary protoalgebraic deductive systems. As an application, we obtain a Sahlqvist theorem for the fragments of the intuitionistic propositional calculus that include the implication connective and for the extensions of the intuitionistic linear logic.
arXiv comment50 pages