Taming Bounded Depth with Nested Sequents
Agata Ciabattoni, Lutz Straßburger, Matteo Tesi · HAL (Le Centre pour la Communication Scientifique Directe) · 2022
Bounded depth refers to a property of Kripke frames that serve as semantics for intuitionistic logic. We introduce nested sequent calculi for the intermediate logics of bounded depth. Our calculi are obtained in a modular way by adding suitable structural rules to a variant of Fitting’s calculus for intuitionistic propositional logic, for which we present the first syntactic cut elimination proof. This proof modularly extends to the new nested sequent calculi introduced in this paper.