Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Intuitionistic Sahlqvist theory for deductive systems

Damiano Fornasiere, Tommaso Moraschini

TL;DR

This paper extends Sahlqvist theory from modal logic to fragments of the intuitionistic propositional calculus that include conjunction and to arbitrary protoalgebraic deductive systems. It develops a robust algebraic–semantic framework (including Up$(\A_*)$, partial p-morphisms, and spectrum-based methods) to transfer modal Sahlqvist ideas into the intuitionistic setting, establishing canonicity and correspondence results for IPC fragments and their extensions. It provides concrete theorems: a canonical canonicity result for IPC fragments with ${\\land}$ (and a general correspondence for protoalgebraic logics), a Sahlqvist theory for IPC fragments with implication, and a correspondence theorem for intuitionistic linear logic, with first-order frame conditions and explicit connections to BTWL, EML, and Gödel–Dummett-type axioms. The work yields a unified method to derive Sahlqvist-type metarules across a broad class of logics and demonstrates applicability to fragments with conjunction and implication as well as to linear-implication frameworks, broadening the reach of Sahlqvist theory in non-classical logics.

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.

Intuitionistic Sahlqvist theory for deductive systems

TL;DR

This paper extends Sahlqvist theory from modal logic to fragments of the intuitionistic propositional calculus that include conjunction and to arbitrary protoalgebraic deductive systems. It develops a robust algebraic–semantic framework (including Up, partial p-morphisms, and spectrum-based methods) to transfer modal Sahlqvist ideas into the intuitionistic setting, establishing canonicity and correspondence results for IPC fragments and their extensions. It provides concrete theorems: a canonical canonicity result for IPC fragments with (and a general correspondence for protoalgebraic logics), a Sahlqvist theory for IPC fragments with implication, and a correspondence theorem for intuitionistic linear logic, with first-order frame conditions and explicit connections to BTWL, EML, and Gödel–Dummett-type axioms. The work yields a unified method to derive Sahlqvist-type metarules across a broad class of logics and demonstrates applicability to fragments with conjunction and implication as well as to linear-implication frameworks, broadening the reach of Sahlqvist theory in non-classical logics.

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.
Paper Structure (11 sections, 51 theorems, 230 equations, 1 figure)

This paper contains 11 sections, 51 theorems, 230 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Pseudocomplemented and implicative semilattices
  3. Posets and partial functions
  4. Sahlqvist theory for $\mathsf{IPC}$
  5. Sahlqvist theory for fragments of $\mathsf{IPC}$ with conjunction
  6. Abstract algebraic logic
  7. Sahlqvist theory for protoalgebraic logics
  8. The excluded middle and the bounded top width laws
  9. Sahlqvist theory for fragments of $\mathsf{IPC}$ with implication
  10. A correspondence theorem for intuitionistic linear logic
  11. Acknowledgements.

Key Result

Theorem 1

The following conditions hold for a Sahlqvist quasiequation $\Phi$ in a language $\mathcal{L} \subseteq \{ \land, \lor, \to, \lnot, 0, 1 \}$ containing $\land$:

Figures (1)

  • Figure 1: A pseudocomplemented semilattice.

Theorems & Definitions (143)

  • Theorem 1
  • Theorem 2
  • Theorem 3
  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Remark 2.4
  • Proposition 2.5
  • proof
  • Remark 2.6
  • ...and 133 more