Inconsistency-Tolerant Bunched Implications

It is known that logical systems with the property of paraconsistency can deal with inconsistency-tolerant and uncertainty reasoning more appropriately than systems which are non-paraconsistent. It is also known that the logic BI of bunched implications is useful for formalizing resource-sensitive reasoning. In this paper, a paraconsistent extension PBI of BI is studied. The logic PBI is thus intended to formalize an appropriate combination of inconsistency-tolerant reasoning and resource-sensitive reasoning. A Gentzen-type sequent calculus SPBI for PBI is introduced, and the cut-elimination and decidability theorems for SPBI are proved. An extension of the Grothendieck topological semantics for BI is introduced for PBI, and the completeness theorem with respect to this semantics is proved.