Document Open Access Logo

Proofs and Refutations for Intuitionistic and Second-Order Logic

Authors Pablo Barenbaum, Teodoro Freund

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.9.pdf
  • Filesize: 0.88 MB
  • 18 pages

Document Identifiers

Author Details

Pablo Barenbaum
  • University of Buenos Aires, Argentina
  • National University of Quilmes (CONICET), Bernal, Argentina
Teodoro Freund
  • University of Buenos Aires, Argentina

Funding

This work was partially supported by project grant PUNQ 2247/22.

Cite AsGet BibTex

Pablo Barenbaum and Teodoro Freund. Proofs and Refutations for Intuitionistic and Second-Order Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.9

Abstract

The λ^{PRK}-calculus is a typed λ-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical propositional logic. In this work, we extend λ^{PRK} to encompass classical second-order logic, by incorporating parametric polymorphism and existential types. The system is shown to enjoy good computational properties, such as type preservation, confluence, and strong normalization, which is established by means of a reducibility argument. We identify a syntactic restriction on proofs that characterizes exactly the intuitionistic fragment of second-order λ^{PRK}, and we study canonicity results.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Type theory
Keywords
  • lambda-calculus
  • propositions-as-types
  • classical logic
  • proof normalization

Metrics

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

Related Versions

References

  1. Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, and Alexis Saurin. Classical call-by-need sequent calculi: The unity of semantic artifacts. In Tom Schrijvers and Peter Thiemann, editors, Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings, volume 7294 of Lecture Notes in Computer Science, pages 32-46. Springer, 2012. Google Scholar
  2. Zena M Ariola, Hugo Herbelin, and Alexis Saurin. Classical call-by-need and duality. In International Conference on Typed Lambda Calculi and Applications, pages 27-44. Springer, 2011. Google Scholar
  3. Franco Barbanera and Stefano Berardi. A symmetric lambda calculus for "classical" program extraction. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, pages 495-515, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg. Google Scholar
  4. Pablo Barenbaum and Teodoro Freund. A constructive logic with classical proofs and refutations. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470649.
  5. Pablo Barenbaum and Teodoro Freund. Proofs and refutations for intuitionistic and second-order logic (extended version), 2022. URL: https://doi.org/10.48550/ARXIV.2210.07274.
  6. Gavin M. Bierman and Valeria CV de Paiva. On an intuitionistic modal logic. Studia Logica, 65(3):383-416, 2000. Google Scholar
  7. Corrado Böhm and Alessandro Berarducci. Automatic synthesis of typed lambda-programs on term algebras. Theor. Comput. Sci., 39:135-154, 1985. Google Scholar
  8. Thierry Coquand and Gérard P. Huet. The calculus of constructions. Inf. Comput., 76(2/3):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  9. Tristan Crolard. Subtractive logic. Theor. Comput. Sci., 254(1-2):151-185, 2001. URL: https://doi.org/10.1016/S0304-3975(99)00124-3.
  10. Pierre-Louis Curien and Hugo Herbelin. The duality of computation, 2000. Google Scholar
  11. Pierre-Louis Curien and Guillaume Munch-Maccagnoni. The duality of computation under focus. In Cristian S. Calude and Vladimiro Sassone, editors, Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010, Brisbane, Australia, September 20-23, 2010. Proceedings, volume 323 of IFIP Advances in Information and Communication Technology, pages 165-181. Springer, 2010. Google Scholar
  12. Brian A. Davey and Hilary A. Priestley. Introduction to lattices and order. Cambridge University Press, Cambridge, 1990. Google Scholar
  13. René David and Walter Py. λμ-calculus and böhm’s theorem. The Journal of Symbolic Logic, 66(1):407-413, 2001. Google Scholar
  14. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. J. ACM, 48(3):555-604, 2001. URL: https://doi.org/10.1145/382780.382785.
  15. Nicolaas Govert De Bruijn. The mathematical language automath, its usage, and some of its extensions. In Symposium on automatic demonstration, pages 29-61. Springer, 1970. Google Scholar
  16. Philippe de Groote. An environment machine for the lambda-mu-calculus. Math. Struct. Comput. Sci., 8(6):637-669, 1998. URL: http://journals.cambridge.org/action/displayAbstract?aid=44787.
  17. Daniel J. Dougherty, Silvia Ghilezan, and Pierre Lescanne. Characterizing strong normalization in the curien-herbelin symmetric lambda calculus: Extending the coppo-dezani heritage. Theor. Comput. Sci., 398(1-3):114-128, 2008. Google Scholar
  18. Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. Abstracting models of strong normalization for classical calculi. J. Log. Algebraic Methods Program., 111:100512, 2020. URL: https://doi.org/10.1016/j.jlamp.2019.100512.
  19. Matthias Felleisen, Daniel P. Friedman, Eugene E. Kohlbecker, and Bruce F. Duba. A syntactic theory of sequential control. Theor. Comput. Sci., 52:205-237, 1987. URL: https://doi.org/10.1016/0304-3975(87)90109-5.
  20. Gerhard Gentzen. Untersuchungen über das logische schließen. i. Mathematische zeitschrift, 39(1):176-210, 1935. Google Scholar
  21. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris 7, 1972. Google Scholar
  22. Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987. Google Scholar
  23. Timothy G Griffin. A formulae-as-type notion of control. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 47-58, 1989. Google Scholar
  24. Giulio Guerrieri and Alberto Naibo. Postponement of raa and Glivenko’s theorem, revisited. Stud Logica, 107(1):109-144, 2019. URL: https://doi.org/10.1007/s11225-017-9781-5.
  25. Hugo Herbelin and Silvia Ghilezan. An approach to call-by-name delimited continuations. SIGPLAN Not., 43(1):383-394, January 2008. URL: https://doi.org/10.1145/1328897.1328484.
  26. Delia Kesner, Eduardo Bonelli, and Andrés Viso. Strong bisimulation for control operators (invited talk). In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 4:1-4:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  27. Delia Kesner and Pierre Vial. Non-idempotent types for classical calculi in natural deduction style. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:3)2020.
  28. Jean-Louis Krivine. Realizability in classical logic. Panoramas et synthèses, 27, January 2009. Google Scholar
  29. Olivier Laurent. Polarized proof-nets and lambda-μ-calculus. Theor. Comput. Sci., 290(1):161-188, 2003. Google Scholar
  30. Per Martin-Löf. A theory of types, 1971. Google Scholar
  31. Nax Paul Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of pure and Applied logic, 51(1-2):159-172, 1991. Google Scholar
  32. Étienne Miquey. A classical sequent calculus with dependent types. ACM Trans. Program. Lang. Syst., 41(2):8:1-8:47, 2019. Google Scholar
  33. Guillaume Munch-Maccagnoni. Focalisation and classical realisability. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings, volume 5771 of Lecture Notes in Computer Science, pages 409-423. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04027-6_30.
  34. David Nelson. Constructible falsity. The Journal of Symbolic Logic, 14(1):16-26, 1949. Google Scholar
  35. Tobias Nipkow. Higher-order critical pairs. In Proceedings 1991 Sixth Annual IEEE Symposium on Logic in Computer Science, pages 342-343. IEEE Computer Society, 1991. Google Scholar
  36. Michel Parigot. Free deduction: An analysis of "computations" in classical logic. In Andrei Voronkov, editor, Logic Programming, First Russian Conference on Logic Programming, Irkutsk, Russia, September 14-18, 1990 - Second Russian Conference on Logic Programming, St. Petersburg, Russia, September 11-16, 1991, Proceedings, volume 592 of Lecture Notes in Computer Science, pages 361-380. Springer, 1991. URL: https://doi.org/10.1007/3-540-55460-2_27.
  37. Michel Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning, pages 190-201, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg. Google Scholar
  38. Pierre-Marie Pédrot and Alexis Saurin. Classical by-need. In European Symposium on Programming, pages 616-643. Springer, 2016. Google Scholar
  39. Andrew M. Pitts. Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci., 10(3):321-359, 2000. URL: http://journals.cambridge.org/action/displayAbstract?aid=44651.
  40. Emmanuel Polonovski. Strong normalization of λμμ-calculus with explicit substitutions. Lecture Notes in Computer Science, pages 423-437, 2004. Google Scholar
  41. Dag Prawitz. Natural deduction: a proof-theoretical study. PhD thesis, Almqvist & Wiksell, 1965. Google Scholar
  42. John C Reynolds. Towards a theory of type structure. In Programming Symposium, pages 408-425. Springer, 1974. Google Scholar
  43. Ian Rumfitt. "Yes" and "No". Mind, 109(436):781-823, 2000. Google Scholar
  44. Alexis Saurin. Separation with streams in the λμ-calculus. In 20th Annual IEEE Symposium on Logic in Computer Science (LICS'05), pages 356-365. IEEE, 2005. Google Scholar
  45. Alexis Saurin. On the relations between the syntactic theories of lambda-mu-calculi. In Michael Kaminski and Simone Martini, editors, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings, volume 5213 of Lecture Notes in Computer Science, pages 154-168. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-87531-4_13.
  46. Jonathan P. Seldin. On the proof theory of the intermediate logic MH. J. Symb. Log., 51(3):626-647, 1986. URL: https://doi.org/10.2307/2274019.
  47. Steffen van Bakel. Completeness and partial soundness results for intersection and union typing for ̅λμμ̃. Ann. Pure Appl. Log., 161(11):1400-1430, 2010. Google Scholar
  48. Yoriyuki Yamagata. Strong normalization of a symmetric lambda calculus for second-order classical logic. Arch. Math. Log., 41(1):91-99, 2002. Google Scholar
  49. Yoriyuki Yamagata. Strong normalization of the second-order symmetric lambda mu -calculus. Inf. Comput., 193(1):1-20, 2004. Google Scholar
  50. Noam Zeilberger. On the unity of duality. Ann. Pure Appl. Log., 153(1-3):66-96, 2008. URL: https://doi.org/10.1016/j.apal.2008.01.001.
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 Imprint Privacy Contact