Skip to main content
SpringerLink
Log in

Constructive Modalities with Provability Smack

  • Chapter
  • First Online:
Leo Esakia on Duality in Modal and Intuitionistic Logics

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 4))

Abstract

I overview the work of the Tbilisi school on intuitionistic modal logics of well-founded/scattered structures and its connections with contemporary Theoretical Computer Science. Fixed-point theorems and their consequences are of particular interest.

To the memory of Leo Esakia and Dito Pataraia

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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

Notes

  1. 1.

    The reader has to be warned that the notation in this section differs somewhat from that in references like [81–83].

  2. 2.

    Speaking of [57], footnote 4 provides an argument that the plural form intended by Grothendieck was toposes rather than topoi. I stick to the same convention, also because—as a quick Google search shows—the form toposes is used mostly by mathematicians, whereas topoi seems prevalent for unrelated notions in the humanities. Besides, this was the form used by Leo, Mamuka and Dito.

  3. 3.

    Note that toposes very rarely happen to mimic sets in having enough global elements to determine all subobjects; such special toposes are called well-pointed.

  4. 4.

    Reader should be warned that in most of categorical literature, presheaves are assumed to be contravariant, but see, e.g., [39] for an example of the covariant convention.

  5. 5.

    The corresponding theorem in [30] contained also an additional statement about density of the support of the fixed-point subobject, but this does not seem essential for us here.

References

  1. Abadi M (2007) Access control in a core calculus of dependency. Electr. Notes Theor. Comput. Sci. 172:5–31

    Article  Google Scholar 

  2. Aczel P (2001) The Russell-Prawitz modality. Math Struct Comput Sci 11(4):541–554

    Article  Google Scholar 

  3. Adámek J, Milius S, Moss L, Sousa L (2012) Well-pointed coalgebras (extended abstract). In: Proceedings of 15th international conference on foundations of software science and computation structures (FoSSaCS’12). Lecture notes in computer science (ARCoSS), vol 7213, pp 89–103

    Google Scholar 

  4. Alberucci L, Facchini A (2009) On modal \(\mu \)-calculus and Gödel-Löb logic. Studia Logica 91(2):145–169

    Google Scholar 

  5. Alechina N, Mendler M, de Paiva V, Ritter E (2001) Categorical and Kripke semantics for constructive S4 modal logic. In: Fribourg L (ed) CSL. Lecture notes in computer science, vol 2142. Springer, Berlin, pp 292–307

    Google Scholar 

  6. Amerbauer M (1996) Cut-free tableau calculi for some propositional normal modal logics. Studia Logica 57(2/3): 359–372

    Google Scholar 

  7. Appel A, Melliès P, Richards C, Vouillon J (2007) A very modal model of a modern, major, general type system. In: Hofmann M, Felleisen M (eds) POPL. ACM, pp 109–122

    Google Scholar 

  8. Atkey R, McBride C (2013) Productive coprogramming with guarded recursion. In: ICFP 2013 Proceedings, pp 197–208

    Google Scholar 

  9. Bellin G, de Paiva V, Ritter E (2001) Extended Curry-Howard correspondence for a basic constructive modal logic. In: Proceedings of methods for modalities

    Google Scholar 

  10. Benton P, Bierman G, de Paiva V (1998) Computational types from a logical perspective. J Funct Program 8(2):177–193

    Google Scholar 

  11. Benton N, Tabareau N (2009) Compiling functional types to relational specifications for low level imperative code. In: Kennedy A, Ahmed A (eds) TLDI. ACM, pp 3–14

    Google Scholar 

  12. Bezhanishvili G, Jansana R (2013) Esakia style duality for implicative semilattices. Appl Categorical Struct 21:181–208

    Google Scholar 

  13. Bierman G, de Paiva V (2000) On an intuitionistic modal logic. Studia Logica 65(3):383–416

    Google Scholar 

  14. Birkedal L, Møgelberg R, Schwinghammer J, Støvring K (2012) First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Meth Comput Sci 8:1–45

    Google Scholar 

  15. Birkedal L, Møgelberg R (2013) Intensional type theory with guarded recursive types qua fixed points on universes. In: Proceedings of LICS (2013)

    Google Scholar 

  16. Blackburn P, de Rijke M, Venema Y (2001) Modal logic. Cambridge University Press, Cambridge

    Google Scholar 

  17. Blok W, Pigozzi D (1989) Algebraizable logics. Memoirs AMS 77:396

    Google Scholar 

  18. Boolos G (1993) The logic of provability. Cambridge University Press, Cambridge

    Google Scholar 

  19. Boolos G, Sambin G (1991) Provability: the emergence of a mathematical modality. Studia Logica 50:1–23

    Google Scholar 

  20. Boz̆ić M, Dos̆en K (1984) Models for normal intuitionistic modal logics. Studia Logica 43(3):217–245

    Google Scholar 

  21. Burris S, Sankappanavar H (1981) A course in universal algebra. Graduate texts in mathematics. Springer, New York

    Book  Google Scholar 

  22. Celani S, Jansana R (1999) Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic. Logic J IGPL 7(6):683–715

    Google Scholar 

  23. Chagrov A, Zakharyaschev M (1997) Modal logic. No. 35 in Oxford logic guides. Clarendon Press, Oxford

    Google Scholar 

  24. Crole R (1993) Categories for types. Cambridge mathematical textbooks. Cambridge University Press, Cambridge

    Google Scholar 

  25. Curry H (1952) The elimination theorem when modality is present. J Symbolic Logic 17(4):249–265

    Google Scholar 

  26. de Jongh D, Visser A (1996) Embeddings of Heyting algebras. In: Logic: from foundations to applications (Staffordshire, 1993), 187–213, Oxford Sci Publ, Oxford University Press, New York

    Google Scholar 

  27. de Paiva V, Ritter E (2011) Basic constructive modality. In: Beziau J, Coniglio M (eds) Logic without frontiers—Festschrift for Walter Alexandre Carnielli on the occasion of his 60th birthday. College Publications, pp 411–428

    Google Scholar 

  28. Di Gianantonio P, Miculan M (2004) Unifying recursive and co-recursive definitions in sheaf categories. In: Walukiewicz I (ed) Foundations of software science and computation structures. Lecture notes in computer science, vol 2987. Springer, Berlin/Heidelberg, pp 136–150

    Google Scholar 

  29. Došen K (1985) Models for stronger normal intuitionistic modal logics. Studia Logica 44(1):39–70

    Google Scholar 

  30. Esakia L, Jibladze M, Pataraia D (2000) Scattered toposes. Ann Pure Appl Logic 103(1–3):97–107

    Article  Google Scholar 

  31. Esakia L (2006) The modalized Heyting calculus: a conservative modal extension of the intuitionistic logic. J Appl Non-Class Logics 16(3–4):349–366

    Article  Google Scholar 

  32. Fairtlough M, Mendler M (1997) Propositional lax logic. Inf Comput 137(1):1–33

    Google Scholar 

  33. Fine K (1985) Logics containing K4. part II. J Symbolic Logic 50(3):619–651

    Google Scholar 

  34. Font J (2006) Beyond Rasiowa’s algebraic approach to non-classical logics. Studia Logica 82(2):179–209

    Google Scholar 

  35. Font J, Jansana R, Pigozzi D (2003) A survey of abstract algebraic logic. Studia Logica 74(1–2):13–97

    Google Scholar 

  36. Font J, Jansana R, Pigozzi D (2009) Update to “A survey of abstract algebraic logic”. Studia Logica 91(1):125–130

    Google Scholar 

  37. Garg D, Abadi M (2008) A modal deconstruction of access control logics. In: Amadio R (ed) FoSSaCS. Lecture notes in computer science, vol 4962. Springer, Berlin, pp 216–230

    Google Scholar 

  38. Garg D, Pfenning F (2006) Non-interference in constructive authorization logic. In: IEEE computer society CSFW, pp 283–296

    Google Scholar 

  39. Ghilardi S (1989) Presheaf semantics and independence results for some non-classical first-order logics. Arch Math Logic 29:125–136

    Google Scholar 

  40. Goldblatt R (2003) Mathematical modal logic: a view of its evolution. J Appl Logic 1(5–6):309–392

    Google Scholar 

  41. Goldblatt R (2006) Topoi: the categorial analysis of logic. In: Dover books on mathematics. Dover Publications, New York

    Google Scholar 

  42. Goldblatt R (1981) Grothendieck topology as geometric modality. Math Logic Q 27(31–35):495–529

    Google Scholar 

  43. Goldblatt R (2010) Cover semantics for quantified lax logic. J Logic Comput 1035–1063

    Google Scholar 

  44. Horn A (1962) The separation theorem of intuitionist propositional calculus. J Symbolic Logic 27(4):391–399

    Google Scholar 

  45. Iemhoff R (2001) Provability logic and admissible rules. PhD thesis, University of Amsterdam

    Google Scholar 

  46. Jaber G, Tabareau N, Sozeau M (2012) Extending type theory with forcing. In: Proceedings of LICS’12, Dubrovnik, Croatia, pp. 395–404

    Google Scholar 

  47. Johnstone P (2002) Sketches of an elephant: a topos theory compendium. In: Oxford logic guides. Clarendon Press, Oxford

    Google Scholar 

  48. Köhler P (1981) Brouwerian semilattices. Trans Am Math Soc 268(1):103–126

    Google Scholar 

  49. Krishnaswami N, Benton N (2011) A semantic model for graphical user interfaces. In: Chakravarty M, Hu Z, Danvy O (eds) ICFP. ACM, pp 45–57

    Google Scholar 

  50. Krishnaswami N, Benton N (2011) Ultrametric semantics of reactive programs. In: LICS. IEEE Computer Society, pp 257–266

    Google Scholar 

  51. Kuznetsov A, Muravitsky A (1986) On superintuitionistic logics as fragments of proof logic extensions. Studia Logica 45(1):77–99

    Google Scholar 

  52. Kuznetsov A (1979) On algebras of open sets. In: The 4th Tiraspol symposium on general topology and its applications, Kishinev. Abstracts, Kishinev (Russian), pp 72–75

    Google Scholar 

  53. Lambek J, Scott P (1986) Introduction to higher order categorical logic. No. 7 in Cambridge studies in advanced mathematics. Cambridge University Press, Cambridge

    Google Scholar 

  54. Litak T (2007) The non-reflexive counterpart of Grz. Bull Sect Logic 36:195–208

    Google Scholar 

  55. MacLane S, Moerdijk I (1992) Sheaves in geometry and logic: a first introduction to topos theory, corrected edn. Springer, Berlin

    Google Scholar 

  56. McBride C, Paterson R (2008) Applicative programming with effects. J Funct Program 18(1):1–13

    Article  Google Scholar 

  57. McLarty C (1990) The uses and abuses of the history of topos theory. Br J Philos Sci 41(3):351–375

    Article  Google Scholar 

  58. Milne P (2010) Subformula and separation properties in natural deduction via small Kripke models. Rev Symbolic Logic 3(02):175–227

    Google Scholar 

  59. Moss L (2007) Finite models constructed from canonical formulas. J Philos Logic 36:605–640

    Google Scholar 

  60. Muravitsky A (1981) Finite approximability of the calculus \({{I}}^{\Delta }\) and the nonmodelability of some of its extensions. Mat Zametki 29(6):907–916

    Google Scholar 

  61. Muravitsky A (2014) Logic KM: a biography (this volume)

    Google Scholar 

  62. Nagaoka K, Isoda E (1997) Incompleteness results in Kripke bundle semantics. Math Logic Q 43(4):485–498

    Google Scholar 

  63. Nakano H (2000) A modality for recursion. In: LICS. IEEE Computer Society, pp 255–266

    Google Scholar 

  64. Nakano H (2001) Fixed-point logic with the approximation modality and its Kripke completeness. In: Kobayashi N, Pierce B (eds) TACS. Lecture notes in computer science, vol 2215. Springer, Berlin, pp 165–182

    Google Scholar 

  65. Pfenning F, Davies R (2001) A judgmental reconstruction of modal logic. Math Struct Comput Sci 11(4):511–540

    Article  Google Scholar 

  66. Prawitz D (1965) Natural deduction: a proof-theoretical study. PhD thesis, Almqvist & Wiksell

    Google Scholar 

  67. Rasiowa H (1974) An algebraic approach to non-classical logics. North Holland

    Google Scholar 

  68. Sambin G (1976) An effective fixed-point theorem in intuitionistic diagonalizable algebras (The algebraization of the theories which express Theor, IX). Studia Logica 35(4):345–361

    Google Scholar 

  69. Simmons H (1982) An algebraic version of Cantor-Bendixson analysis. In: Banaschewski B (ed) Categorical aspects of topology and analysis. Lecture notes in mathematics, vol 915. Springer, Berlin / Heidelberg, pp 310–323

    Google Scholar 

  70. Simmons H (2014) Cantor-Bendixson properties of the assembly of a frame (this volume)

    Google Scholar 

  71. Simpson A (1994) The proof theory and semantics of intuitionistic modal logic. PhD thesis, University of Edinburgh

    Google Scholar 

  72. Skvortsov D (2012) Kripke sheaf completeness of some superintuitionistic predicate logics with a weakened constant domains principle. Studia Logica 100:361–383

    Google Scholar 

  73. Smorynski C (1979) Calculating self-referential statements, I: explicit calculations. Studia Logica 38(1):17–36

    Google Scholar 

  74. Solovay R (1976) Provability interpretations of modal logic. Israel J Math 25:287–304

    Google Scholar 

  75. Sotirov V (1984) Modal theories with intuitionistic logic. In: Mathematical logic, proc. conf. math. logic dedicated to the memory of A. A. Markov (1903–1979), Sofia, 22–23 Sept 1980, pp 139–171

    Google Scholar 

  76. ten Cate B, Fontaine G, Litak T (2010) Some modal aspects of XPath. J Appl Non-Class Logics 20(3):139–171

    Google Scholar 

  77. Ursini A (1979) A modal calculus analogous to K4W, based on intuitionistic propositional logic, I-. Studia Logica: Int J Symbolic Logic 38(3):297–311

    Google Scholar 

  78. van Benthem J (1991) Reflections on epistemic logic. Logique et Anal 34:5–14

    Google Scholar 

  79. van Benthem J (2006) Modal frame correspondences and fixed-points. Studia Logica 83(1–3):133–155

    Google Scholar 

  80. Visser A (2005) Löb’s logic meets the \(\mu \)-calculus. In: Middeldorp A, van Oostrom V, van Raamsdonk F, de Vrijer R (eds) Processes, terms and cycles. Lecture notes in computer science, vol 3838. Springer, Berlin, pp 14–25

    Google Scholar 

  81. Wolter F, Zakharyaschev M (1997) On the relation between intuitionistic and classical modal logics. Algebra and Logic 36:121–125

    Google Scholar 

  82. Wolter F, Zakharyaschev M (1998) Intuitionistic modal logics as fragments of classical modal logics. In: Orlowska E (ed) Logic at work, essays in honour of Helena Rasiowa. Springer, Berlin, pp 168–186

    Google Scholar 

  83. Wolter F, Zakharyaschev M (2014) On the Blok-Esakia theorem (this volume)

    Google Scholar 

Download references

Acknowledgments

Special thanks are due to: the anonymous referee for careful reading and many helpful comments; Guram Bezhanishvili, for an invitation to write this chapter, but also his tolerance, understanding and patience during the whole process; Alexander Kurz for his support, interest and numerous discussions; Mamuka Jibladze and the late Dito Pataraia, particularly for all the discussions we had in Kutaisi. Apart from this, the list of people who provided feedback and/or suggestions include (in no particular order) Lars Birkedal, Rasmus Møgelberg, Stefan Milius, Thomas Streicher, Sam Staton, Alex Simpson, Gordon Plotkin, Johan van Benthem, Ramon Jansana, Achim Jung, Andrew Pitts, Conor McBride, Nick Benton, Guilhem Jaber, Dirk Pattinson, Drew Moshier, Nick Bezhanishvili, Alexei Muravitsky, Fredrik Nordvall Forsberg, Ben Kavanagh, Oliver Fasching, participants of Domains X, TYPES 2011, MGS 2012 and seminars at the University of Leicester. During most of the write-up, I was supported by the EPSRC grant EP/G041296/1.

Author information

Authors and Affiliations

  1. Friedrich-Alexander-Universität, Martensstraße 3, 91058, Erlangen, Germany

    Tadeusz Litak

Authors
  1. Tadeusz Litak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tadeusz Litak .

Editor information

Editors and Affiliations

  1. New Mexico State University, Las Cruces, New Mexico, USA

    Guram Bezhanishvili

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Litak, T. (2014). Constructive Modalities with Provability Smack. In: Bezhanishvili, G. (eds) Leo Esakia on Duality in Modal and Intuitionistic Logics. Outstanding Contributions to Logic, vol 4. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-8860-1_8

Download citation

Publish with us

Policies and ethics

Search

Navigation