Abstract
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.
The text for the second edition has been updated by including some points that have been discussed at the UniLog meeting 2005 in Montreux.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Peter B. Andrews. Refutations by matings. IEEE Transactions on Computers, C-25:801–807, 1976.
Michael Barr. *-Autonomous Categories, volume 752 of Lecture Notes in Mathematics. Springer-Verlag, 1979.
Wolfgang Bibel. A deductive solution for plan generation. New Generation Computing, 4:115–132, 1986.
Richard Blute. Linear logic, coherence and dinaturality. Theoretical Computer Science, 115:3–41, 1993.
Kai Brünnler. Deep Inference and Symmetry for Classical Proofs. PhD thesis, Technische Universität Dresden, 2003.
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.
Samuel R. Buss. The undecidability of k-provability. Annals of Pure and Applied Logic, 53:72–102, 1991.
Carlos Caleiro and Ricardo Gonçalves. Equipollent logical systems. In Jean-Yves Beziau, editor, Logica Universalis, pages 99–111. Birkhäuser, 2005.
Kosta Došen and Zoran Petrić. Proof-Theoretical Coherence. KCL Publications, London, 2004.
Samuel Eilenberg and Gregory Maxwell Kelly. A generalization of the functorial calculus. Journal of Algebra, 3(3):366–375, 1966.
Carsten Führmann and David Pym. On the geometry of interaction for classical logic. preprint, 2004.
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.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
Jean-Yves Girard. A new constructive logic: Classical logic. Mathematical Structures in Computer Science, 1:255–296, 1991.
Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.
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.
Alessio Guglielmi. A system of interaction and structure. To appear in ACM Transactions on Computational Logic, 2002.
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.
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.
Gregory Maxwell Kelly and Saunders Mac Lane. Coherence in closed categories. Journal of Pure and Applied Algebra, 1:97–140, 1971.
Joachim Lambek. Deductive systems and categories. I: Syntactic calculus and residuated categories. Math. Systems Theory, 2:287–318, 1968.
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.
François Lamarche. Exploring the gap between linear and classical logic, 2006. Submitted.
Joachim Lambek and Phil J. Scott. Introduction to higher order categorical logic, volume 7 of Cambridge studies in advanced mathematics. Cambridge University Press, 1986.
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.
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.
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.
Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer-Verlag, 1971.
Dale Miller. A compact representation of proofs. Studia Logica, 46(4):347–370, 1987.
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.
R. Pöschel and L. A. Kalužnin. Funktionen-und Relationenalgebren, Ein Kapitel der Diskreten Mathematik. Deutscher Verlag der Wissenschaften, Berlin, 1979.
Stephen Pollard. Homeomorphism and the equivalence of logical systems. Notre Dame Journal of Formal Logic, 39:422–435, 1998.
E. L. Post. The Two-Valued Iterative Systems of Mathematical Logic. Princeton University Press, Princeton, 1941.
Dag Prawitz. Natural Deduction, A Proof-Theoretical Study. Almquist and Wiksell, 1965.
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.
Francis Jeffry Pelletier and Alasdair Urquhart. Synonymous logics. Journal of Philosophical Logic, 32:259–285, 2003.
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.
Finiki Stouppa. The design of modal proof theories: the case of S5. Master’s thesis, Technische Universität Dresden, 2004.
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.
Lutz Straßurger. On the axiomatisation of Boolean categories with and without medial, 2005. Preprint, available at http://arxiv.org/abs/cs.LO/0512086.
Lutz Straßurger. Proof nets and the identity of proofs, 2006. Lecture notes for ESSLLI’06. Available from https://hal.inria.fr/inria-00107260/en/ and http://arxiv.org/abs/cs.LO/0610123.
Rüdiger Thiele. Hilbert’s twenty-fourth problem. American Mathematical Monthly, 110:1–24, 2003.
Contest: How to define identity between logics? 1st World Congress and School on Universal Logic, 2005. On the web at http://www.uni-log.org/one2.html.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2007 Birkhäuser Verlag Basel/Switzerland
About this paper
Cite this paper
Straßurger, L. (2007). What is a Logic, and What is a Proof?. In: Beziau, JY. (eds) Logica Universalis. Birkhäuser Basel. https://doi.org/10.1007/978-3-7643-8354-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-7643-8354-1_8
Publisher Name: Birkhäuser Basel
Print ISBN: 978-3-7643-8353-4
Online ISBN: 978-3-7643-8354-1
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)