file.pdf (274.74 kB)
Download file

Focus-preserving Embeddings of Substructural Logics in Intuitionistic Logic

Download (274.74 kB)
journal contribution
posted on 01.10.2005, 00:00 authored 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.




Usage metrics