file.pdf (274.74 kB)
Focus-preserving Embeddings of Substructural Logics in Intuitionistic Logic
journal contribution
posted on 2005-10-01, 00:00 authored by Jason Reed, Frank PfenningWe 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.