Focus-preserving Embeddings of Substructural Logics in Intuitionistic Logic

2005-10-01T00:00:00Z (GMT) by Jason Reed Frank Pfenning
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.