Sequent Calculus for Intuitionistic Epistemic Logic IEL | SpringerLink
Skip to main content
Springer Nature Link
Log in

Sequent Calculus for Intuitionistic Epistemic Logic IEL

  • Conference paper
  • First Online:
Logical Foundations of Computer Science (LFCS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9537))

Included in the following conference series:

  • 694 Accesses

Abstract

The formal system of intuitionistic epistemic logic IEL was proposed by S. Artemov and T. Protopopescu. It provides the formal foundation for the study of knowledge from an intuitionistic point of view based on Brouwer-Hayting-Kolmogorov semantics of intuitionism. We construct a cut-free sequent calculus for IEL and establish that polynomial space is sufficient for the proof search in it. We prove that IEL is PSPACE-complete.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    For example, it can be some trusted database that stores true facts without proofs or some zero-knowledge proof.

  2. 2.

    Sequents in [4] are classical (multiconclusion) and contain special labels denoting worlds of a Kripke structure, so this formalization can be considered as a classical formulation of the theory of forcing relation in a Kripke structure that corresponds to the intuitionistic bimodal epistemic logic.

  3. 3.

    This method was introduced by Kleene in the construction of his G3 systems, see [6].

References

  1. Artemov, S., Protopopescu, T.: Intuitionistic Epistemic Logic (2014). arXiv:1406.1582v2

  2. Williamson, T.: On intuitionistic modal epistemic logic. J. Philos. Log. 21(1), 63–89 (1992)

    MathSciNet  MATH  Google Scholar 

  3. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. The MIT Press, Cambridge (1995)

    MATH  Google Scholar 

  4. Maffezioli, V., Naibo, A., Negri, S.: The Church-Fitch knowability paradox in the light of structural proof theory. Synthese 190, 2677–2716 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  5. Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (1996)

    MATH  Google Scholar 

  6. Kleene, S.C.: Introduction to Metamathematics. North-Holland Publ. Co., Amsterdam (1952)

    MATH  Google Scholar 

  7. Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. Assoc. Comput. Mach. 28, 114–133 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  8. Statman, R.: Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci. 9, 67–72 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  9. Krupski, V.N.: Introduction to Computational Complexity. Factorial Press, Moscow (2006). (In Russian)

    Google Scholar 

  10. Kitaev, A., Shen, A., Vyalyi, M.: Classical and Quantum Computations. MCCME-CheRo, Moscow (1999). (In Russian)

    MATH  Google Scholar 

  11. Krupski, N.: Typing in reflective combinatory logic. Ann. Pure Appl. Log. 141, 243–256 (2006)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

We are grateful to Sergey Artemov for inspiring discussions of intuitionistic epistemic logic. We thank the anonymous referees for their comments.

The research described in this paper was partially supported by Russian Foundation for Basic Research (grant 14-01-00127).

Author information

Authors and Affiliations

  1. Faculty of Mechanics and Mathematics, Lomonosov Moscow State University, Moscow, 119992, Russia

    Vladimir N. Krupski & Alexey Yatmanov

Authors
  1. Vladimir N. Krupski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexey Yatmanov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vladimir N. Krupski .

Editor information

Editors and Affiliations

  1. City University of New York , New York, New York, USA

    Sergei Artemov

  2. Cornell University , Ithaca, New York, USA

    Anil Nerode

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Krupski, V.N., Yatmanov, A. (2016). Sequent Calculus for Intuitionistic Epistemic Logic IEL. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2016. Lecture Notes in Computer Science(), vol 9537. Springer, Cham. https://doi.org/10.1007/978-3-319-27683-0_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-27683-0_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-27682-3

  • Online ISBN: 978-3-319-27683-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics