Provability in BI's Sequent Calculus is Decidable

TL;DR

This paper claims to prove that provability in BI's sequent calculus is decidable by reducing proof search to a primitive recursive set, extending classical logic techniques, despite a noted mistake in the proof.

Contribution

It introduces a method to reduce proof search in BI's sequent calculus to a primitive recursive set, suggesting decidability of provability.

Findings

Proof search space for BI can be reduced to a primitive recursive set

Decidability of provability in BI is established under the proposed method

The approach generalizes classical logic decidability techniques

Abstract

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.