Provability in BI's Sequent Calculus is Decidable
Alexander V. Gheorghiu, Simon Docherty, David J. Pym · arXiv (Cornell University) · 2021
Warning: This paper contains a mistake, rendering the proof of the main theorem invalid. The logic of Bunched Implications (BI) combines both additive and multiplicative connectives, which include two primitive intuitionistic implications. As a consequence, contexts in the sequent presentation are not lists, nor multisets, but rather tree-like structures called bunches. This additional complexity notwithstanding, the logic has a well-behaved metatheory admitting all the familiar forms of semantics and proof systems. However, the presentation of an effective proof-search procedure has been elusive since the logic's debut. We show that one can reduce the proof-search space for any given sequent to a primitive recursive set, the argument generalizing Gentzen's decidability argument for classical propositional logic and combining key features of Dyckhoff's contraction-elimination argument for intuitionistic logic. An effective proof-search procedure, and hence decidability of provability, follows as a corollary.