Admissible rules for six intuitionistic modal logics

Iris van der Giessen*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

33 Downloads (Pure)


This paper characterizes the admissible rules for six interesting intuitionistic modal logics: iCK4, iCS4 ≡ IPC, strong Löb logic iSL, modalized Heyting calculus mHC, Kuznetsov-Muravitsky logic KM, and propositional lax logic PPL. Admissible rules are rules that can be added to a logic without changing the set of theorems of the logic. We provide a Gentzen-style proof theory for admissibility that combines methods known for intuitionistic propositional logic and classical modal logic. From this proof theory, we extract bases for the admissible rules, i.e., sets of admissible rules that derive all other admissible rules. In addition, we show that admissibility is decidable for these logics.
Original languageEnglish
Article number103233
Number of pages34
JournalAnnals of Pure and Applied Logic
Issue number4
Early online date21 Dec 2022
Publication statusPublished - 1 Apr 2023


  • Admissible rules
  • Proof theory
  • Intuitionistic modal logic
  • Provability logic
  • Lax logic

Cite this