file.pdf (274.74 kB)

Focus-preserving Embeddings of Substructural Logics in Intuitionistic Logic

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

History

Date

01/10/2005

Exports

Exports