Temporal BI: Proof system, semantics and translations

The logic BI of bunched implications is a combination of intuitionistic logic and multiplicative intuitionistic linear logic. In this paper, a temporal extension tBI of BI is introduced and studied. A Gentzen-type sequent calculus GtBI for tBI is introduced, and the cut-elimination and decidability theorems for GtBI are proved using a theorem for syntactically embedding GtBI into a sequent calculus GBI for BI. A semantics for GtBI is introduced extending the Grothendieck topological semantics for BI, and the completeness theorem with respect to this semantics is proved using a theorem for semantically embedding tBI into BI. A semantics for GtBI without additive falsity constant is introduced extending the Kripke resource semantics for BI without additive falsity constant, and the completeness theorem with respect to this semantics is proved in a similar way. Moreover, an intuitionistic temporal linear logic, ITLL, is introduced as a Gentzen-type sequent calculus, and a theorem for embedding GtBI into ITLL is proved using a temporal extension of the Girard translation of intuitionistic logic into intuitionistic linear logic.