The G4i analogue of a G3i calculus

TL;DR

This paper extends Dyckhoff's G4ip calculus to a broad class of intuitionistic modal logics, providing a systematic method to derive terminating analytic calculi that preserve equivalence and extend existing cut-free systems.

Contribution

It introduces a general method to obtain terminating analytic calculi for intuitionistic modal logics based on existing cut-free calculi, extending Dyckhoff's G4ip framework.

Findings

Provides a systematic construction method for analytic calculi

Ensures the resulting calculus is terminating and equivalent to the original

Extends Dyckhoff's G4ip to a large class of intuitionistic modal logics

Abstract

This paper provides a method to obtain terminating analytic calculi for a large class of intuitionistic modal logics. For a given logic L with a cut-free calculus G that is an extension of G3ip the method produces a terminating analytic calculus that is an extension of G4ip and equivalent to G. G4ip has been introduced by Dyckhoff in 1992 as a terminating analogue of the calculus G3ip for intuitionistic propositional logic. Thus this paper can be viewed as an extension of Dyckhoff's work to intuitionistic modal logic.