Skip to Main content Skip to Navigation
Conference papers

Classical and Intuitionistic Subexponential Logics are Equally Expressive

Kaustuv Chaudhuri 1 
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : It is standard to regard the intuitionistic restriction of a classical logic as increasing the expressivity of the logic because the classical logic can be adequately represented in the intuitionistic logic by double-negation, while the other direction has no truth-preserving propositional encodings. We show here that subexponential logic, which is a family of substructural refinements of classical logic, each parametric over a preorder over the subexponential connectives, does not suffer from this asymmetry if the preorder is systematically modified as part of the encoding. Precisely, we show a bijection between synthetic (i.e., focused) partial sequent derivations modulo a given encoding. Particular instances of our encoding for particular subexponential preorders give rise to both known and novel adequacy theorems for substructural logics.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Kaustuv Chaudhuri Connect in order to contact the contributor
Submitted on : Wednesday, November 10, 2010 - 4:38:50 PM
Last modification on : Thursday, January 20, 2022 - 5:30:47 PM
Long-term archiving on: : Friday, February 11, 2011 - 3:15:38 AM


Files produced by the author(s)




Kaustuv Chaudhuri. Classical and Intuitionistic Subexponential Logics are Equally Expressive. Computer Science Logic, Aug 2010, Brno, Czech Republic. pp.185--199, ⟨10.1007/978-3-642-15205-4_17⟩. ⟨inria-00534865⟩



Record views


Files downloads