Abstract
Lax logic is obtained from intuitionistic logic by adding a single modality o which captures properties of necessity and possibility. This modality was considered by Curry in two papers from 1952 and 1957 and rediscovered recently in different contexts like verification of circuits and the computational λ-calculus. We show that lax logic can be faithfully embedded into the underlying intuitionistic logic and discuss (computational) properties of the embedding. Using the proposed polynomial-time computable embedding, PSPACE-completeness of the provability problem of propositional lax logic is shown.
The author would like to thank R. Dyckhoff, T. Eiter, D. Galmiche, D. Larchey-Wendling, and S. Woltran for discussions and the anonymous referees for questions and comments.
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
P. N. Benton, G. M. Bierman, and V. C. V. de Paiva. Computational types from a logical perspective. Journal of Functional Programming, 8(2):177–193, 1998.
H. B. Curry. The elimination theorem when modality is present. Journal of Symbolic Logic, 17:249–265, 1952.
H. B. Curry. A Theory of Formal Deducibility, volume 6 of Notre Dame Mathematical Lectures. Notre Dame, Indiana, second edition, 1957.
R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57(3):795–807, 1992.
Uwe Egly. Embedding lax logic into intuitionistic logic. Technical report, Abteilung Wissensbasierte Systeme, TU Wien, 2002.
M. Fairtlough and M. Mendler. Propositional lax logic. Information and Computation, 137(1):1–33, 1997.
M. Fairtlough, M. Mendler, and M. Walton. First-order lax logic as a framework for constraint logic programming. Technical Report MIPS-9714, University of Passau, 1997.
M. Fairtlough and M. Walton. Quantified lax logic. Technical Report CS-97-11, University of Sheffield, Department of Computer Science, 1997.
D. Galmiche and D. Larchey-Wendling. Structural sharing and efficient proof-search in propositional intuitionistic logic. In Asian Computing Science Conference, ASIAN’99, volume 1742 of Lecture Notes in Computer Science, pages 101–112. Springer Verlag, 1999.
J. M. Howe. Proof Search Issues in Some Non-Classical Logics. PhD thesis, University of St Andrews, December 1998. Available as University of St Andrews Research Report CS/99/1.
J. M. Howe. Proof search in lax logic. Mathematical Structures in Computer Science, 11(4):573–588, August 2001.
J. Hudelmaier. An O(nlogn)-space decision procedure for intuitionistic propositional logic. Journal of Logic and Computation, 3(1):63–75, 1993.
M. Mendler. A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Edinburgh University, Department of Computer Science, ECS-LFCS-93-255, 1993.
E. Moggi. Notion of computation and monads. Information and Computation, 93:55–92, 1991.
F. Pfenning and R. Davis. A judgemental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511–540, August 2001.
R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9:67–72, 1979.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Egly, U. (2002). Embedding Lax Logic into Intuitionistic Logic. In: Voronkov, A. (eds) Automated Deduction—CADE-18. CADE 2002. Lecture Notes in Computer Science(), vol 2392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45620-1_6
Download citation
DOI: https://doi.org/10.1007/3-540-45620-1_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43931-8
Online ISBN: 978-3-540-45620-9
eBook Packages: Springer Book Archive