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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. of Logic and Computation 2(3), 297–347 (1992)
Barber, A., Plotkin, G.: Dual intuitionistic linear logic. Technical Report ECS-LFCS-96-347, University of Edinburgh (1996)
Chang, B.-Y.E., Chaudhuri, K., Pfenning, F.: A judgmental analysis of linear logic. Technical Report CMU-CS-03-131R, Carnegie Mellon University (December 2003)
Chaudhuri, K.: The Focused Inverse Method for Linear Logic. PhD thesis, Carnegie Mellon University, Technical report CMU-CS-06-162 (December 2006)
Chaudhuri, K.: Focusing strategies in the sequent calculus of synthetic connectives. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 467–481. Springer, Heidelberg (2008)
Chaudhuri, K.: Classical and intuitionistic subexponential logics are equally expressive. Technical report, INRIA (2010)
Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. J. of Automated Reasoning 40(2-3), 133–177 (2008)
Danos, V., Joinet, J.-B., Schellinx, H.: The structure of exponentials: Uncovering the dynamics of linear logic proofs. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol. 713, pp. 159–171. Springer, Heidelberg (1993)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Laurent, O.: Etude de la polarisation en logique. Thèse de doctorat, Université Aix-Marseille II (March 2002)
Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science 410(46), 4747–4768 (2009)
Liang, C., Miller, D.: A unified sequent calculus for focused proofs. In: LICS-24, pp. 355–364 (2009)
Miller, D.: Finding unity in computational logic. In: ACM-BCS-Visions (April 2010)
Nigam, V.: Exploiting non-canonicity in the sequent calculus. PhD thesis, Ecole Polytechnique (September 2009)
Nigam, V., Miller, D.: Algorithmic specifications in linear logic with subexponentials. In: PPDP, pp. 129–140 (2009)
Schellinx, H.: Some syntactical observations on linear logic. Journal of Logic and Computation 1(4), 537–559 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chaudhuri, K. (2010). Classical and Intuitionistic Subexponential Logics Are Equally Expressive. In: Dawar, A., Veith, H. (eds) Computer Science Logic. CSL 2010. Lecture Notes in Computer Science, vol 6247. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15205-4_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-15205-4_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15204-7
Online ISBN: 978-3-642-15205-4
eBook Packages: Computer ScienceComputer Science (R0)