Embedding Modal Logics into Logics of Bunched Implications
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2608.07203
curl -X POST /api/v1/records/arxiv/2608.07203/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2608.07203/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'