Embedding Modal Logics into Logics of Bunched Implications

Daniele Sansoni, Ranald Clouston

We present a new proof of the embedding of the classical modal logic S4 into the logic of Boolean Bunched Implications (BBI). While the original proof is semantical, this proof is…