Classical and Intuitionistic Subexponential Logics Are Equally Expressive

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.

• Type: Conference
• Year: 2010
• Where: CSL
• Authors: Kaustuv Chaudhuri
• Keywords: Automated Reasoning, Classical Logic, CSL 2010, Intuitionistic Logic, Truth-preserving Propositional Encodings