Document Open Access Logo

Negative Translations and Normal Modality

Authors Tadeusz Litak, Miriam Polzer, Ulrich Rabenstein

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.27.pdf
  • Filesize: 0.63 MB
  • 18 pages

Document Identifiers

Author Details

Tadeusz Litak
Miriam Polzer
Ulrich Rabenstein

Cite As Get BibTex

Tadeusz Litak, Miriam Polzer, and Ulrich Rabenstein. Negative Translations and Normal Modality. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.27

Abstract

We discuss the behaviour of variants of the standard negative translations - Kolmogorov, Gödel-Gentzen, Kuroda and Glivenko - in propositional logics with a unary normal modality. More specifically, we address the question whether negative translations as a rule embed faithfully a classical modal logic into its intuitionistic counterpart. As it turns out, even the Kolmogorov translation can go wrong with rather natural modal principles. Nevertheless, we isolate sufficient syntactic criteria   ensuring adequacy of well-behaved (or, in our terminology, regular) translations for logics axiomatized with formulas satisfying these criteria, which we call enveloped implications. Furthermore, a large class of computationally relevant modal logics - namely, logics of type inhabitation for applicative functors (a.k.a. idioms) - turns out to validate the modal counterpart of the Double Negation Shift, thus ensuring adequacy of even the Glivenko translation. All our positive results are proved purely syntactically, using the minimal natural deduction system of Bellin, de Paiva and Ritter extended with additional axioms/combinators and hence also allow a direct formalization in a proof assistant (in our case Coq).

Subject Classification

Keywords
  • negative translations
  • intuitionistic modal logic
  • normal modality
  • double negation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Peter Aczel. The Russell-Prawitz modality. MSCS, 11(4):541-554, 2001. Google Scholar
  2. H. Andréka, Á. Kurucz, I. Németi, I. Sain, and A. Simon. Causes and remedies for undecidability in arrow logics and in multi-modal logics. In Maarten Marx, László Pólos, and Michael Masuch, editors, Arrow Logic and Multi-Modal Logic, Stud. Logic Lang. Inform., pages 63-100. CSLI Publications, 1996. Google Scholar
  3. Zena M. Ariola and Hugo Herbelin. Minimal classical logic and control operators. In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, editors, Proceedings of ICALP, volume 2719 of LNCS, pages 871-885. Springer, 2003. URL: http://dx.doi.org/10.1007/3-540-45061-0_68.
  4. Sergei Artemov and Tudor Protopopescu. Intuitionistic epistemic logic. Rev. Symb. Logic, 9(2):266-298, 2016. URL: http://dx.doi.org/10.1017/S1755020315000374.
  5. Gianluigi Bellin. A system of natural deduction for GL. Theoria, 51(2):89-114, 1985. URL: http://dx.doi.org/10.1111/j.1755-2567.1985.tb00089.x.
  6. Gianluigi Bellin, Valeria de Paiva, and Eike Ritter. Extended Curry-Howard correspondence for a basic constructive modal logic. In Proceedings of Methods for Modalities, 2001. URL: http://profs.sci.univr.it/~bellin/m4m.ps.
  7. Guram Bezhanishvili. Glivenko type theorems for intuitionistic modal logics. Stud. Logica, 67(1):89-109, 2001. URL: http://dx.doi.org/10.1023/A:1010577628486.
  8. Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. First steps in synthetic guarded domain theory: Step-indexing in the topos of trees. LMCS, 8:1-45, 2012. Google Scholar
  9. George Boolos. The Logic of Provability. Cambridge University Press, 1993. Google Scholar
  10. Milan Božić and Kosta Došen. Axiomatizations of intuitionistic double negation. B. Sect. Logic, 12(2):99-102, 1983. Google Scholar
  11. Milan Božić and Kosta Došen. Models for normal intuitionistic modal logics. Stud. Logica, 43(3):217-245, 1984. URL: http://www.jstor.org/stable/20015164.
  12. James Brotherston and Max Kanovich. Undecidability of propositional separation logic and its neighbours. J. ACM, 61(2):14:1-14:43, 04 2014. URL: http://dx.doi.org/10.1145/2542667.
  13. Alexander Chagrov and Michael Zakharyaschev. Modal Logic. Number 35 in Oxford Logic Guides. Clarendon Press, 1997. Google Scholar
  14. Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. From axioms to analytic rules in nonclassical logics. In Proceedings of LiCS, pages 229-240. IEEE Computer Society, 2008. URL: http://dx.doi.org/10.1109/LICS.2008.39.
  15. Agata Ciabattoni, Lutz Straßburger, and Kazushige Terui. Expanding the realm of systematic proof theory. In Proceedings of CSL, pages 163-178, Berlin, Heidelberg, 2009. Springer-Verlag. Google Scholar
  16. Valeria de Paiva and Eike Ritter. Basic constructive modality. In Jean-Yves Beziau and Marcelo Esteban Coniglio, editors, Logic Without Frontiers- Festschrift for Walter Alexandre Carnielli on the occasion of his 60th birthday, pages 411-428. College Publications, 2011. Google Scholar
  17. Kosta Došen. Modal translations and intuitionistic double negation. Logique et Analyse, 29(113):81-94, 1986. URL: http://www.jstor.org/stable/44084152.
  18. Martín Escardó and Paulo Oliva. The Peirce translation and the Double Negation Shift. In Fernando Ferreira, Benedikt Löwe, Elvira Mayordomo, and Luís Mendes Gomes, editors, Proceedings of CiE, pages 151-161. Springer Berlin Heidelberg, 2010. URL: http://dx.doi.org/10.1007/978-3-642-13962-8_17.
  19. Matt Fairtlough and Michael Mendler. Propositional lax logic. Inform. and Comput., 137(1):1-33, 1997. Google Scholar
  20. Hadi Farahani and Hiroakira Ono. Glivenko theorems and negative translations in substructural predicate logics. Arch. Math. Log., 51(7-8):695-707, 2012. URL: http://dx.doi.org/10.1007/s00153-012-0293-8.
  21. Gilda Ferreira and Paulo Oliva. On the relation between various negative translations. In Ulrich Berger and Helmut Schwichtenberg, editors, Logic, Construction, Computation, volume 3 of Mathematical Logic Series, pages 227-258. Ontos-Verlag, 2012. Google Scholar
  22. Nikolaos Galatos and Peter Jipsen. Distributive residuated frames and generalized bunched implication algebras. Algebr. Univ., to appear. Google Scholar
  23. Nikolaos Galatos and Hiroakira Ono. Glivenko theorems for substructural logics over FL. J. Symb. Logic, 71(4):1353-1384, 2006. URL: http://www.jstor.org/stable/27588518.
  24. Didier Galmiche, Daniel Méry, and David J. Pym. The semantics of BI and resource tableaux. MSCS, 15(6):1033-1088, 2005. URL: http://dx.doi.org/10.1017/S0960129505004858.
  25. Jaime Gaspar. Negative translations not intuitionistically equivalent to the usual ones. Stud. Logica, 101(1):45-63, 2013. URL: http://dx.doi.org/10.1007/s11225-011-9367-6.
  26. Robert I. Goldblatt. Grothendieck topology as geometric modality. MLQ, 27(31-35):495-529, 1981. URL: http://dx.doi.org/10.1002/malq.19810273104.
  27. Timothy G. Griffin. A formulae-as-type notion of control. In Proceedings of POPL, Proceedings of POPL, pages 47-58, New York, NY, USA, 1990. ACM. URL: http://dx.doi.org/10.1145/96709.96714.
  28. Wesley Halcrow Holliday. Possibility frames and forcing for modal logic (June 2016), 2016. submitted eScholarship manuscript: URL: http://www.escholarship.org/uc/item/9v11r0dq.
  29. Rosalie Iemhoff. Provability logic and admissible rules. phdthesis, University of Amsterdam, 2001. Google Scholar
  30. Yoshihiko Kakutani. Call-by-name and call-by-value in normal modal logic. In Zhong Shao, editor, Proceedings of APLAS, volume 4807 of LNCS, pages 399-414. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-76637-7_27.
  31. Daisuke Kimura and Yoshihiko Kakutani. Classical natural deduction for S4 modal logic. New Generation Comput., 29(1):61-86, 2011. URL: http://dx.doi.org/10.1007/s00354-010-0099-3.
  32. Clemens Kupke, Alexander Kurz, and Yde Venema. Stone coalgebras. Theoret. Comput. Sci., 327(1):109-134, 2004. URL: http://dx.doi.org/10.1016/j.tcs.2004.07.023.
  33. Á. Kurucz, I. Németi, I. Sain, and A. Simon. Decidable and undecidable logics with a binary modality. JoLLI, 4(3):191-206, 1995. URL: http://www.jstor.org/stable/40180071.
  34. Charles H. Lambros. A shortened proof of Sobociński’s theorem concerning a restricted rule of substitution in the field of propositional calculi. Notre Dame J. Form. L., 20(1):112-114, 01 1979. URL: http://dx.doi.org/10.1305/ndjfl/1093882409.
  35. Dominique Larchey-Wendling and Didier Galmiche. Nondeterministic phase semantics and the undecidability of boolean BI. ACM Trans. Comput. Logic, 14(1):6:1-6:41, 02 2013. URL: http://dx.doi.org/10.1145/2422085.2422091.
  36. Tadeusz Litak. Constructive modalities with provability smack. In Guram Bezhanishvili, editor, Leo Esakia on duality in modal and intuitionistic logics, volume 4 of Outstanding Contributions to Logic, pages 179-208. Springer, 2014. Author’s Cut: https://www8.cs.fau.de/ext/litak/esakiaarxivfull.pdf. URL: http://dx.doi.org/10.1007/978-94-017-8860-1_8.
  37. Conor McBride and Ross Paterson. Applicative programming with effects. J. Funct. Programming, 18(1):1-13, 2008. URL: http://dx.doi.org/10.1017/S0956796807006326.
  38. Stefan Milius and Tadeusz Litak. Guard your daggers and traces: Properties of guarded (co-)recursion. Fundamenta Informaticae, 150:407-449, 2017. special issue FiCS'13. URL: http://arxiv.org/abs/1603.05214, URL: http://dx.doi.org/10.3233/FI-2017-1475.
  39. Chetan R. Murthy. An evaluation semantics for classical proofs. In Giles Kahn, editor, Proceedings of LiCS, pages 96-107. IEEE Computer Society Press, July 1991. Google Scholar
  40. Hiroshi Nakano. A modality for recursion. In Proceedings of LiCS, pages 255-266. IEEE, 2000. Google Scholar
  41. Hiroshi Nakano. Fixed-point logic with the approximation modality and its Kripke completeness. In Naoki Kobayashi and Benjamin C. Pierce, editors, Proceedings of TACS, volume 2215 of LNCS, pages 165-182. Springer, 2001. Google Scholar
  42. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. B. Symb. Log., 5(2):215-244, 1999. URL: http://www.jstor.org/stable/421090.
  43. Hiroakira Ono. Glivenko theorems revisited. Ann. Pure Appl. Logic, 161(2):246-250, 2009. URL: http://dx.doi.org/10.1016/j.apal.2009.05.006.
  44. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. MSCS, 11(4):511-540, 2001. Google Scholar
  45. David J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26 of Appl. Log. Ser. Kluwer Academic Publishers, 2002. Google Scholar
  46. Alex K. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. phdthesis, University of Edinburgh, 1994. URL: http://homepages.inf.ed.ac.uk/als/Research/thesis.ps.gz.
  47. Bolesław Sobociński. A theorem concerning a restricted rule of substitution in the field of propositional calculi. I and II. Notre Dame J. Form. L., 15(3 and 4):465-476 and 589-597, 1974. URL: http://dx.doi.org/10.1305/ndjfl/1093891408.
  48. Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Stud. Logic Found. Math. Elsevier Science Inc., 2006. Google Scholar
  49. Vladimir Sotirov. Modal theories with intuitionistic logic. In Mathematical Logic, Proc. Conf. Math. Logic Dedicated to the Memory of A. A. Markov (1903-1979), Sofia, September 22-23, 1980, pages 139-171, 1984. Google Scholar
  50. Anne S. Troelstra. Marginalia on sequent calculi. Stud. Logica, 62(2):291-303, 1999. URL: http://dx.doi.org/10.1023/A:1026413320413.
  51. Anne S. Troelstra and H. Schwichtenberg. Basic proof theory. Number 43 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2000. Google Scholar
  52. Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics: An Introduction, volume 121 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1988. Google Scholar
  53. Johan van Benthem, Nick Bezhanishvili, and Wesley Halcrow Holliday. A bimodal perspective on possibility semantics. J. Log. Comput., 2016. URL: http://www.escholarship.org/uc/item/2h5069pq.
  54. Albert Visser. On the completeness principle: A study of provability in Heyting’s arithmetic and extensions. Ann. Math. Logic, 22(3):263-295, 1982. Google Scholar
  55. Albert Visser. Closed fragments of provability logics of constructive theories. J. Symb. Logic, 73(3):1081-1096, 2008. Google Scholar
  56. Frank Wolter and Michael Zakharyaschev. On the relation between intuitionistic and classical modal logics. Algebra and Logic, 36:121-125, 1997. Google Scholar
  57. Frank Wolter and Michael Zakharyaschev. Intuitionistic modal logics as fragments of classical bimodal logics. In Ewa Orlowska, editor, Logic at Work, Essays in honour of Helena Rasiowa, pages 168-186. Springer-Verlag, 1998. Google Scholar
  58. Frank Wolter and Michael Zakharyaschev. Modal decision problems. Studies in Logic and Practical Reasoning, 3:427-489, 2007. URL: http://dx.doi.org/10.1016/S1570-2464(07)80010-3.
  59. Michael Zakharyaschev, Frank Wolter, and Alexander Chagrov. Advanced modal logic. In D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, pages 83-266. Springer Netherlands, 2001. URL: http://dx.doi.org/10.1007/978-94-017-0454-0_2.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact