What is a Logic, and What is a Proof?

  • Lutz Straßurger


I will discuss the two problems of how to define identity between logics and how to define identity between proofs. For the identity of logics, I propose to simply use the notion of preorder equivalence. This might be considered to be folklore, but is exactly what is needed from the viewpoint of the problem of the identity of proofs: If the proofs are considered to be part of the logic, then preorder equivalence becomes equivalence of categories, whose arrows are the proofs. For identifying these, the concept of proof nets is discussed.


Modal Logic Classical Logic Category Theory Deductive System Intuitionistic Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [And76]
    Peter B. Andrews. Refutations by matings. IEEE Transactions on Computers, C-25:801–807, 1976.Google Scholar
  2. [Bar79]
    Michael Barr. *-Autonomous Categories, volume 752 of Lecture Notes in Mathematics. Springer-Verlag, 1979.Google Scholar
  3. [Bib86]
    Wolfgang Bibel. A deductive solution for plan generation. New Generation Computing, 4:115–132, 1986.MATHGoogle Scholar
  4. [Blu93]
    Richard Blute. Linear logic, coherence and dinaturality. Theoretical Computer Science, 115:3–41, 1993.MATHCrossRefMathSciNetGoogle Scholar
  5. [Brü03]
    Kai Brünnler. Deep Inference and Symmetry for Classical Proofs. PhD thesis, Technische Universität Dresden, 2003.Google Scholar
  6. [BT01]
    Kai Brünnler and Alwen Fernanto Tiu. A local system for classical logic. In R. Nieuwenhuis and A. Voronkov, editors, LPAR 2001, volume 2250 of Lecture Notes in Artificial Intelligence, pages 347–361. Springer-Verlag, 2001.Google Scholar
  7. [Bus91]
    Samuel R. Buss. The undecidability of k-provability. Annals of Pure and Applied Logic, 53:72–102, 1991.CrossRefMathSciNetGoogle Scholar
  8. [CG05]
    Carlos Caleiro and Ricardo Gonçalves. Equipollent logical systems. In Jean-Yves Beziau, editor, Logica Universalis, pages 99–111. Birkhäuser, 2005.Google Scholar
  9. [DP04]
    Kosta Došen and Zoran Petrić. Proof-Theoretical Coherence. KCL Publications, London, 2004.MATHGoogle Scholar
  10. [EK66]
    Samuel Eilenberg and Gregory Maxwell Kelly. A generalization of the functorial calculus. Journal of Algebra, 3(3):366–375, 1966.MATHCrossRefMathSciNetGoogle Scholar
  11. [FP04a]
    Carsten Führmann and David Pym. On the geometry of interaction for classical logic. preprint, 2004.Google Scholar
  12. [FP04b]
    Carsten Führmann and David Pym. On the geometry of interaction for classical logic (extended abstract). In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), pages 211–220, 2004.Google Scholar
  13. [Gir87]
    Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.MATHCrossRefMathSciNetGoogle Scholar
  14. [Gir91]
    Jean-Yves Girard. A new constructive logic: Classical logic. Mathematical Structures in Computer Science, 1:255–296, 1991.MATHCrossRefMathSciNetGoogle Scholar
  15. [GLT89]
    Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.Google Scholar
  16. [GS01]
    Alessio Guglielmi and Lutz Straßurger. Non-commutativity and MELL in the calculus of structures. In Laurent Fribourg, editor, Computer Science Logic, CSL 2001, volume 2142 of LNCS, pages 54–68. Springer-Verlag, 2001.Google Scholar
  17. [Gug02]
    Alessio Guglielmi. A system of interaction and structure. To appear in ACM Transactions on Computational Logic, 2002.Google Scholar
  18. [How80]
    W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, 1980.Google Scholar
  19. [Hyl04]
    J. Martin E. Hyland. Abstract interpretation of proofs: Classical propositional calculus. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, CSL 2004, volume 3210 of LNCS, pages 6–21. Springer-Verlag, 2004.Google Scholar
  20. [KM71]
    Gregory Maxwell Kelly and Saunders Mac Lane. Coherence in closed categories. Journal of Pure and Applied Algebra, 1:97–140, 1971.MATHCrossRefMathSciNetGoogle Scholar
  21. [Lam68]
    Joachim Lambek. Deductive systems and categories. I: Syntactic calculus and residuated categories. Math. Systems Theory, 2:287–318, 1968.MATHCrossRefMathSciNetGoogle Scholar
  22. [Lam69]
    Joachim Lambek. Deductive systems and categories. II. standard constructions and closed categories. In P. Hilton, editor, Category Theory, Homology Theory and Applications, volume 86 of Lecture Notes in Mathematics, pages 76–122. Springer, 1969.Google Scholar
  23. [Lam06]
    François Lamarche. Exploring the gap between linear and classical logic, 2006. Submitted.Google Scholar
  24. [LS86]
    Joachim Lambek and Phil J. Scott. Introduction to higher order categorical logic, volume 7 of Cambridge studies in advanced mathematics. Cambridge University Press, 1986.Google Scholar
  25. [LS05a]
    François Lamarche and Lutz Straßurger. Constructing free Boolean categories. In Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS’05), pages 209–218, 2005.Google Scholar
  26. [LS05b]
    François Lamarche and Lutz Straßurger. Naming proofs in classical propositional logic. In Paweł Urzyczyn, editor, Typed Lambda Calculi and Applications, TLCA 2005, volume 3461 of Lecture Notes in Computer Science, pages 246–261. Springer-Verlag, 2005.Google Scholar
  27. [LS06]
    François Lamarche and Lutz Straßurger. From proof nets to the free *-autonomous category. Logical Methods in Computer Science, 2(4:3):1–44, 2006.Google Scholar
  28. [Mac71]
    Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer-Verlag, 1971.Google Scholar
  29. [Mil87]
    Dale Miller. A compact representation of proofs. Studia Logica, 46(4):347–370, 1987.MATHCrossRefMathSciNetGoogle Scholar
  30. [ML75]
    Per Martin-Löf. About models for intuitionistic type theories and the notion of definitional equality. In S. Kangar, editor, Proceedings of the Third Scandinavian Logic Symposium, pages 81–109. North-Holland Publishing Co., 1975.Google Scholar
  31. [PK79]
    R. Pöschel and L. A. Kalužnin. Funktionen-und Relationenalgebren, Ein Kapitel der Diskreten Mathematik. Deutscher Verlag der Wissenschaften, Berlin, 1979.Google Scholar
  32. [Pol98]
    Stephen Pollard. Homeomorphism and the equivalence of logical systems. Notre Dame Journal of Formal Logic, 39:422–435, 1998.MATHCrossRefMathSciNetGoogle Scholar
  33. [Pos41]
    E. L. Post. The Two-Valued Iterative Systems of Mathematical Logic. Princeton University Press, Princeton, 1941.MATHGoogle Scholar
  34. [Pra65]
    Dag Prawitz. Natural Deduction, A Proof-Theoretical Study. Almquist and Wiksell, 1965.Google Scholar
  35. [Pra71]
    Dag Prawitz. Ideas and results in proof theory. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 235–307. North-Holland Publishing Co., 1971.Google Scholar
  36. [PU03]
    Francis Jeffry Pelletier and Alasdair Urquhart. Synonymous logics. Journal of Philosophical Logic, 32:259–285, 2003.MATHCrossRefMathSciNetGoogle Scholar
  37. [SL04]
    Lutz Straßurger and François Lamarche. On proof nets for multiplicative linear logic with units. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, CSL 2004, volume 3210 of LNCS, pages 145–159. Springer-Verlag, 2004.Google Scholar
  38. [Sto04]
    Finiki Stouppa. The design of modal proof theories: the case of S5. Master’s thesis, Technische Universität Dresden, 2004.Google Scholar
  39. [Str05a]
    Lutz Straßurger. From deep inference to proof nets. In Structures and Deduction — The Quest for the Essence of Proofs (Satellite Workshop of ICALP 2005), 2005.Google Scholar
  40. [Str05b]
    Lutz Straßurger. On the axiomatisation of Boolean categories with and without medial, 2005. Preprint, available at Scholar
  41. [Str06]
    Lutz Straßurger. Proof nets and the identity of proofs, 2006. Lecture notes for ESSLLI’06. Available from and Scholar
  42. [Thi03]
    Rüdiger Thiele. Hilbert’s twenty-fourth problem. American Mathematical Monthly, 110:1–24, 2003.MATHCrossRefMathSciNetGoogle Scholar
  43. [Uni05]
    Contest: How to define identity between logics? 1st World Congress and School on Universal Logic, 2005. On the web at Scholar

Copyright information

© Birkhäuser Verlag Basel/Switzerland 2007

Authors and Affiliations

  • Lutz Straßurger
    • 1
  1. 1.INRIA Futurs, Projet ParsifalÉcole Polytechnique — LIXPalaiseau CedexFrance

Personalised recommendations