Metraipolis › archive › dc_6de9019d2dfd

Embedding Modal Logics into Logics of Bunched Implications — arXiv:2608.07203

Source: arXiv (en)
Original: https://arxiv.org/abs/2608.07203
License (as archived): CC0-1.0
Archived: 2026-10-23T15:19:02.812Z
SHA-256 of the archived text: 20480a7fec575d20b5406abf328b46f31d20ca7182654db51c34bd2dd3205e42
Stable URL of this page: https://metraipolis.com/documento/dc_6de9019d2dfd

How to cite

Embedding Modal Logics into Logics of Bunched Implications — arXiv:2608.07203 — arXiv (en), https://arxiv.org/abs/2608.07203 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_6de9019d2dfd (Metraipolis archive dc_6de9019d2dfd, sha256 20480a7fec575d20b5406abf328b46f31d20ca7182654db51c34bd2dd3205e42)

BibTeX

@misc{dc6de9019d2dfd,
  title = {Embedding Modal Logics into Logics of Bunched Implications — arXiv:2608.07203},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2608.07203},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_6de9019d2dfd; sha256 20480a7fec575d20b5406abf328b46f31d20ca7182654db51c34bd2dd3205e42},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2608.07203. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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 entirely syntactical. It proceeds via Hilbert-style calculi, and is built by analogy with a recently discovered proof by Godel of the embedding of intuitionistic propositional logic into S4. We present the first full proofs of deduction theorems for BBI, which are used to show that the embedding is preserved by reasoning with assumptions, including where those assumptions are organised into bunches. Unlike the existing proof, our proof is stable under arbitrary axiomatic extensions of S4, and applies to all known axiomatic extensions of BBI in the literature. We observe how this embedding is related to semantical properties of both logics. Moreover, the proof extends gracefully to language extensions of BBI, as we show with hybrid BBI, classical BI, and sub-classical BBI.

Tema degli esploratori: matematica e informatica teorica (retro-catalogo arXiv: annunci del 2026-08-10 in cs.LO).
Categorie arXiv: Logic in Computer Science (cs.LO) ; Logic (math.LO).
Pagina del lavoro: https://arxiv.org/abs/2608.07203 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-23T15:09:24.946Z dalla pagina https://arxiv.org/catchup/cs.LO/2026-08-10?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).