Intuitionistic Sahlqvist theory for deductive systems
Damiano Fornasiere, Tommaso Moraschini
TL;DR
This paper extends Sahlqvist theory to certain fragments of intuitionistic propositional calculus, enabling algebraic and logical analysis of these systems, including those with conjunction and implication connectives.
Contribution
It introduces a Sahlqvist theory for intuitionistic fragments with conjunction and implication, applicable to various protoalgebraic deductive systems and extensions like linear logic.
Findings
Sahlqvist theory extended to conjunction-inclusive intuitionistic fragments
A Sahlqvist theorem established for implication-inclusive fragments
Application to extensions of intuitionistic linear logic
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Algebra and Logic · Logic, Reasoning, and Knowledge · Logic, programming, and type systems