Tags:Chu construction, negative translation and proof theory
Abstract:
Bellin translates multiplicative-additive linear logic to its intuitionistic fragment by relating the Chu construction to trips on a proof net, seemingly posing an alternative to negative translation. However, his translation is not sound in the sense that not all valid intuitionistic sequents in its image correspond to valid classical ones. By directly analyzing two-sided classical sequents, we develop a sound generalization thereof inspired by parametric negative translation that also handles the exponentials.