Classical and Intuitionistic Subexponential Logics are Equally Expressive

TL;DR

This paper demonstrates that classical and intuitionistic subexponential logics are equally expressive by establishing a systematic encoding that preserves derivations, challenging the common view of their asymmetry in expressivity.

Contribution

It introduces a systematic encoding for subexponential logics that shows their expressive equivalence, including new and known adequacy results for substructural logics.

Findings

A bijection between focused derivations in classical and intuitionistic subexponential logics.

Encoding modifications can eliminate the asymmetry in expressivity.

New adequacy theorems for substructural logics derived from specific encodings.

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.