Embedding Lax Logic into Intuitionistic Logic

  • Uwe Egly
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    H. B. Curry. The elimination theorem when modality is present. Journal of Symbolic Logic, 17:249–265, 1952.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    H. B. Curry. A Theory of Formal Deducibility, volume 6 of Notre Dame Mathematical Lectures. Notre Dame, Indiana, second edition, 1957.Google Scholar
  4. 4.
    R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57(3):795–807, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Uwe Egly. Embedding lax logic into intuitionistic logic. Technical report, Abteilung Wissensbasierte Systeme, TU Wien, 2002.Google Scholar
  6. 6.
    M. Fairtlough and M. Mendler. Propositional lax logic. Information and Computation, 137(1):1–33, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    M. Fairtlough and M. Walton. Quantified lax logic. Technical Report CS-97-11, University of Sheffield, Department of Computer Science, 1997.Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    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.Google Scholar
  11. 11.
    J. M. Howe. Proof search in lax logic. Mathematical Structures in Computer Science, 11(4):573–588, August 2001.Google Scholar
  12. 12.
    J. Hudelmaier. An O(nlogn)-space decision procedure for intuitionistic propositional logic. Journal of Logic and Computation, 3(1):63–75, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    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.Google Scholar
  14. 14.
    E. Moggi. Notion of computation and monads. Information and Computation, 93:55–92, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    F. Pfenning and R. Davis. A judgemental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511–540, August 2001.Google Scholar
  16. 16.
    R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9:67–72, 1979.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Uwe Egly
    • 1
  1. 1.Institut für Informationssysteme E184.3TU WienWienAustria

Personalised recommendations