Deep Inference in Bi-intuitionistic Logic

Abstract

Bi-intuitionistic logic is the extension of intuitionistic logic with exclusion, a connective dual to implication. Cut-elimination in bi-intuitionistic logic is complicated due to the interaction between these two connectives, and various extended sequent calculi, including a display calculus, have been proposed to address this problem.

In this paper, we present a new extended sequent calculus DBiInt for bi-intuitionistic logic which uses nested sequents and “deep inference”, i.e., inference rules can be applied at any level in the nested sequent. We show that DBiInt can simulate our previous “shallow” sequent calculus LBiInt. In particular, we show that deep inference can simulate the residuation rules in the display-like shallow calculus LBiInt. We also consider proof search and give a simple restriction of DBiInt which allows terminating proof search. Thus our work is another step towards addressing the broader problem of proof search in display logic.