Intuitionistic BV (Extended version)

TL;DR

This paper introduces the intuitionistic logic IBV, providing a deep inference proof system with cut elimination, and explores its variants related to NML, including a sequent calculus for INML.

Contribution

It presents a new intuitionistic logic IBV with a deep inference proof system and cut elimination, and extends to variants related to NML with sequent calculus.

Findings

Deep inference proof system for IBV with cut elimination

IBV reduces to IMLL on MLL connectives

Sequent calculus developed for INML variant

Abstract

We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non-commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus.