Focus-preserving Embeddings of Substructural Logics in Intuitionistic Logic

We present a method of embedding substructural logics into ordinary first-order intuitionistic logic. This embedding is faithful in a very strong sense: not only does it preserve provability of sequents under translation, but it also preserves sets of proofs — and the focusing structure of those proofs — up to isomorphism. Examples are given for the cases of intuitionistic linear logic and ordered logic, and indeed we can use our method to derive a correct focusing system for ordered logic. Potential applications lie in logic programming, theorem proving, and logical frameworks for substructural logics where focusing is crucial for the underlying proof theory.