The True Concurrency of Herbrand's Theorem

Authors Aurore Alcolei, Pierre Clairambault, Martin Hyland, Glynn Winskel



PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.5.pdf
  • Filesize: 0.61 MB
  • 22 pages

Document Identifiers

Author Details

Aurore Alcolei
  • Univ Lyon, ENS de Lyon, CNRS, UCB Lyon 1, LIP, Lyon, France
Pierre Clairambault
  • Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, Lyon, France
Martin Hyland
  • DPMMS, University of Cambridge , Cambridge, United Kingdom
Glynn Winskel
  • Computer Laboratory, University of Cambridge, Cambridge, United Kingdom

Cite AsGet BibTex

Aurore Alcolei, Pierre Clairambault, Martin Hyland, and Glynn Winskel. The True Concurrency of Herbrand's Theorem. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CSL.2018.5

Abstract

Herbrand's theorem, widely regarded as a cornerstone of proof theory, exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula to that of a finite disjunction. In the general case, it reduces first-order validity to propositional validity, by understanding the structure of the assignment of first-order terms to existential quantifiers, and the causal dependency between quantifiers. In this paper, we show that Herbrand's theorem in its general form can be elegantly stated and proved as a theorem in the framework of concurrent games, a denotational semantics designed to faithfully represent causality and independence in concurrent systems, thereby exposing the concurrency underlying the computational content of classical proofs. The causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers implicit in proofs. Furthermore concurrent strategies can be composed, yielding a compositional proof of Herbrand's theorem, simply by interpreting classical sequent proofs in a well-chosen denotational model.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Denotational semantics
Keywords
  • Herbrand's theorem
  • Game semantics
  • True concurrency

Metrics

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

References

  1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409-470, 2000. Google Scholar
  2. 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, International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings, volume 789 of Lecture Notes in Computer Science, pages 495-515. Springer, 1994. URL: http://dx.doi.org/10.1007/3-540-57887-0_112.
  3. Michael Barr. *-autonomous categories and linear logic. Mathematical Structures in Computer Science, 1(2):159-178, 1991. Google Scholar
  4. Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures. Logical Methods in Computer Science, 13(3), 2017. Google Scholar
  5. Pierre Clairambault, Julian Gutierrez, and Glynn Winskel. The winning ways of concurrent games. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pages 235-244. IEEE, 2012. Google Scholar
  6. J.R.B. Cockett and R.A.G. Seely. Weakly distributive categories. Journal of Pure and Applied Algebra, 114(2):133-173, 1997. Google Scholar
  7. Thierry Coquand. A semantics of evidence for classical arithmetic. J. Symb. Log., 60(1):325-337, 1995. Google Scholar
  8. Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. A new deconstructive logic: Linear logic. J. Symb. Log., 62(3):755-807, 1997. Google Scholar
  9. Carsten Führmann and David J. Pym. On categorical models of classical logic and the geometry of interaction. Mathematical Structures in Computer Science, 17(5):957-1027, 2007. Google Scholar
  10. Gerhard Gentzen. Untersuchungen über das logische schließen. i. Mathematische zeitschrift, 39(1):176-210, 1935. Google Scholar
  11. Philipp Gerhardy and Ulrich Kohlenbach. Extracting herbrand disjunctions by functional interpretation. Arch. Math. Log., 44(5):633-644, 2005. Google Scholar
  12. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. Google Scholar
  13. Jean-Yves Girard. A new constructive logic: Classical logic. Mathematical Structures in Computer Science, 1(3):255-296, 1991. Google Scholar
  14. Kurt Gödel. Über eine bisher noch nicht benützte erweiterung des finiten standpunktes. dialectica, 12(3-4):280-287, 1958. Google Scholar
  15. Willem Heijltjes. Classical proof forestry. Ann. Pure Appl. Logic, 161(11):1346-1366, 2010. Google Scholar
  16. Stefan Hetzl and Daniel Weller. Expansion trees with cut. CoRR, abs/1308.0428, 2013. Google Scholar
  17. Ulrich Kohlenbach. On the no-counterexample interpretation. J. Symb. Log., 64(4):1491-1511, 1999. Google Scholar
  18. Jean-Louis Krivine. Realizability in classical logic. Panoramas et synthèses, 27:197-229, 2009. Google Scholar
  19. Olivier Laurent. Game semantics for first-order logic. Logical Methods in Computer Science, 6(4), 2010. Google Scholar
  20. F William Lawvere. Adjointness in foundations. Dialectica, 23(3-4):281-296, 1969. Google Scholar
  21. Richard McKinley. Proof nets for Herbrand’s theorem. ACM Trans. Comput. Log., 14(1):5, 2013. Google Scholar
  22. Paul-André Mellies. Categorical semantics of linear logic. Panoramas et syntheses, 27:15-215, 2009. Google Scholar
  23. Paul-André Melliès and Samuel Mimram. Asynchronous games: Innocence without alternation. In Luís Caires and Vasco Thudichum Vasconcelos, editors, CONCUR, volume 4703 of LNCS, pages 395-411. Springer, 2007. Google Scholar
  24. Dale A Miller. A compact representation of proofs. Studia Logica, 46(4):347-370, 1987. Google Scholar
  25. Samuel Mimram. The structure of first-order causality. Mathematical Structures in Computer Science, 21(1):65-110, 2011. Google Scholar
  26. Michel Parigot. Lambda-my-calculus: An algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, volume 624 of Lecture Notes in Computer Science, pages 190-201. Springer, 1992. URL: http://dx.doi.org/10.1007/BFb0013061.
  27. Silvain Rideau and Glynn Winskel. Concurrent strategies. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, pages 409-418, 2011. Google Scholar
  28. Robert A. G. Seely. Hyperdoctrines, natural deduction and the Beck condition. Math. Log. Q., 29(10):505-542, 1983. Google Scholar
  29. Robert AG Seely. Linear logic,*-autonomous categories and cofree coalgebras. Ste. Anne de Bellevue, Quebec: CEGEP John Abbott College, 1987. Google Scholar
  30. J.R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967. Google Scholar
  31. Glynn Winskel. Event structures. In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Advances in Petri Nets, volume 255 of LNCS, pages 325-392. Springer, 1986. Google Scholar
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