Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Labelled calculi for lattice-based modal logics

Ineke van der Berg, Andrea De Domenico, Giuseppe Greco, Krishna Manoorkar, Alessandra Palmigiano, Mattia Panettiere

Abstract

We introduce labelled sequent calculi for the basic normal non-distributive modal logic L and 31 of its axiomatic extensions, where the labels are atomic formulas of a first order language which is interpreted on the canonical extensions of the algebras in the variety corresponding to the logic L. Modular proofs are presented that these calculi are all sound, complete and conservative w.r.t. L, and enjoy cut elimination and the subformula property. The introduction of these calculi showcases a general methodology for introducing labelled calculi for the class of LE-logics and their analytic axiomatic extensions in a principled and uniform way.

Labelled calculi for lattice-based modal logics

Abstract

We introduce labelled sequent calculi for the basic normal non-distributive modal logic L and 31 of its axiomatic extensions, where the labels are atomic formulas of a first order language which is interpreted on the canonical extensions of the algebras in the variety corresponding to the logic L. Modular proofs are presented that these calculi are all sound, complete and conservative w.r.t. L, and enjoy cut elimination and the subformula property. The introduction of these calculi showcases a general methodology for introducing labelled calculi for the class of LE-logics and their analytic axiomatic extensions in a principled and uniform way.
Paper Structure (15 sections, 6 theorems, 6 equations)

This paper contains 15 sections, 6 theorems, 6 equations.

Table of Contents

  1. Introduction
  2. Structure of the paper.
  3. Preliminaries
  4. Basic normal non-distributive modal logic, its associated ALBA-language, and some of its axiomatic extensions
  5. $\mathcal{L}$-algebras, their canonical extensions, and the algebraic interpretation of the extended language of ALBA
  6. The algorithm ALBA
  7. The labelled calculus A.L and some of its extensions
  8. Properties of the calculus $\mathbf{A.L}\Sigma$
  9. Soundness
  10. Syntactic completeness
  11. Conservativity
  12. Cut elimination and subformula property
  13. $\mathbf{A.L}\Sigma$ is a proper labelled calculus
  14. Conclusions
  15. Proper labelled calculi

Key Result

theorem thmcountertheorem

Any proper labelled calculus enjoys cut-elimination. If also the condition C$_1$ in Definition def:ProperLabelledCalculi is satisfied, then the proof system enjoys the subformula property.

Theorems & Definitions (20)

  • definition thmcounterdefinition: Analysis
  • definition thmcounterdefinition: Position
  • definition thmcounterdefinition
  • remark thmcounterremark: Analysis of switch rules
  • remark thmcounterremark
  • theorem thmcountertheorem
  • corollary thmcountercorollary
  • lemma thmcounterlemma
  • proof
  • definition thmcounterdefinition
  • ...and 10 more