What Is a Good Sequent Calculus?

  • Francesca PoggiolesiEmail author
Part of the Trends in Logic book series (TREN, volume 32)


In his doctoral thesis of 1935, the young and brilliant student Gerhard Gentzen introduced what is today known as the sequent calculus. Over the last eighty years the sequent calculus has been the central interest of several illustrious proof theorists. This has given rise to a broad literature and numerous results. Nevertheless, there still are problems and issues concerning the sequent calculus that need to be further developed and tackled. Amongst these, our attention has been attracted by one question that can be expressed as follows: what is a good sequent calculus? What, in other words, are the properties that a sequent calculus needs to satisfy to be considered good? The aim of this chapter is to attempt to find an answer to this question.


Intuitionistic Logic Logical Variant Logical Rule Structural Rule Sequent Calculus 
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.


  1. 6.
    A. Avron. The method of hypersequents in the proof theory of propositional non-classical logic. In W. Hodges, M. Hyland, C. Steinhorn, and J. Strauss, editors, Logic: from Foundations to Applications, pp. 1–32. Oxford University Press, Oxford, 1996.Google Scholar
  2. 8.
    N. D. Belnap. Display logic. Journal of Philosophical Logic, 11:375–417, 1982.Google Scholar
  3. 13.
    G. Boloos. Don’t eliminate cut. Journal of Philosophical Logic, 13:373–378, 1984.CrossRefGoogle Scholar
  4. 18.
    E. Casari. Introduzione alla Logica. UTET, Torino, 1997.Google Scholar
  5. 27.
    H. B. Curry. The elimination theorem when modality is present. Journal of Symbolic Logic, 17:249–265, 1952.CrossRefGoogle Scholar
  6. 29.
    M. D’agostino and M. Mondadori. The taming of the cut. Classical refutations with analytic cut. Journal of Logic and Computation, 4:285–319, 1994.CrossRefGoogle Scholar
  7. 31.
    K. Došen. Sequent-systems for modal logic. Journal of Symbolic Logic, 50:149–159, 1985.CrossRefGoogle Scholar
  8. 33.
    K. Došen. Logical constants as punctuation marks. Notre Dame Journal of Formal Logic, 30:362–381, 1989.CrossRefGoogle Scholar
  9. 34.
    A. G. Dragalin. Mathematical Intuitionism. Introduction to Proof Theory. American Mathematical Society, Providence, 1988.Google Scholar
  10. 35.
    M. Dummett. The logical basis of metaphysics. Harvard University Press, Cambridge, 1991.Google Scholar
  11. 39.
    N. Francez and R. Dyckhoff. Proof-theoretic semantics for natural language. In Proceedings of the 10th Meeting of the Association of Mathematics of Language (MOL), July 2007, pp. 1–7. Los Angeles, forthcoming.Google Scholar
  12. 40.
    D. Gabbay. Labelled Deductive Systems: Volume 1. Foundations. Oxford University Press, Oxford, 1996.Google Scholar
  13. 54.
    I. Hacking. What is logic? Journal of Philosophy, 76:285–319, 1979.CrossRefGoogle Scholar
  14. 57.
    R. Hein and C. Stewart. Purity through unravelling. In P. Bruscoli, F. Lamarche, and C. Stewart, editors, Structures and Deductions, pp. 126–143. Technische Universit, Dresden, 2005.Google Scholar
  15. 58.
    P. Hertz. Uber axiomensysteme beliebiger satzsysteme. Annalen der Philosophie und philosophischen Kritik, 8:178–204, 1929.Google Scholar
  16. 59.
    P. Hertz. Uber axiomensysteme für beliebige satzsysteme. Mathematische Annalen, 101:457–514, 1929.CrossRefGoogle Scholar
  17. 61.
    O. Hjortland. Proof-theoretic harmony and structural assumptions. http://olethhjortland., pp. 1–20, 2007.
  18. 63.
    A. Indrezejczak. Generalised sequent calculus for propositional modal logics. Logica Trianguli, 1:15–31, 1997.Google Scholar
  19. 71.
    M. Kremer. Logic and meaning: the philosophical significance of the sequent calculus. Mind, New Series, 97:50–72, 1988.CrossRefGoogle Scholar
  20. 76.
    S. Leśniewski. Gründzuge eines neuen systems der grundlagen der mathematik. Fundamenta Mathematicae, 14:1–81, 1929.Google Scholar
  21. 94.
    F. Paoli. Substructural Logics: a Primer. Kluwer Academic Publisher, Dordrecht-Boston-London, 2002.Google Scholar
  22. 95.
    F. Paoli. Quine and slater on paraconsistency and deviance. Journal of Philosophical Logic, 32:531–548, 2003.CrossRefGoogle Scholar
  23. 107.
    D. Prawitz. Meaning and proofs: on the conflict between classical and intuitionistic logic. Theoria, 43:2–40, 1977.CrossRefGoogle Scholar
  24. 108.
    A. N. Prior. A runabout inference ticket. Analysis, 21:38–39, 1960.CrossRefGoogle Scholar
  25. 109.
    W. V. O. Quine. Word and Object. MIT Press, Cambridge, 1960.Google Scholar
  26. 110.
    W. V. O. Quine. Philosophy of Logic. Prentice-Hall, Englewood Cliffs, 1970.Google Scholar
  27. 111.
    W. V. O. Quine. The Roots of Reference. Open Court, La Salle, 1973.Google Scholar
  28. 113.
    S. Read. Harmony and autonomy in classical logic. Journal of Philosophical Logic, 29:123–154, 2000.CrossRefGoogle Scholar
  29. 114.
    S. Read. Harmony and modality. In C. Dégremont, L. Kieff, and H. Rückert, editors, Dialogues, Logics and Other Strong Things: Essays in Honour of Shahid Rahman, pp. 285–303. College Publications, London, 2008.Google Scholar
  30. 125.
    P. Schroeder-Heister. A natural extension of natural deduction (abstract). Journal of Symbolic Logic, 49:1284–1300, 1984.CrossRefGoogle Scholar
  31. 126.
    P. Schroeder-Heister. Generalised definitional reflection and the inversion principle. Logica Universalis, 1:355–376, 2007.CrossRefGoogle Scholar
  32. 134.
    P. Stouppa. A deep inference system for the modal logic S5. Studia Logica, 85:199–214, 2007.CrossRefGoogle Scholar
  33. 136.
    N. Tennant. The taming of the true. Oxford University Press, Oxford, 1997.Google Scholar
  34. 137.
    N. Tennant. Inferentialism, logicism, harmony, and a counterpoint. In A. Miller, editor, Essays for Crispin Wright: Logic, language, and mathematics, Vol 2, pp. 105–132. Oxford University Press, London, 2007.Google Scholar
  35. 139.
    A. S. Troelestra and H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, Cambridge, 1996.Google Scholar
  36. 145.
    H. Wansing. Sequent systems for normal modal propositional logics. Journal of Logic and Computation, 4:125–142, 1994.CrossRefGoogle Scholar
  37. 147.
    H. Wansing. Displaying Modal Logic. Kluwer Academic Publisher, Dordrecht, 1998.Google Scholar
  38. 148.
    H. Wansing. The idea of a proof-theoretic semantics and the meaning of the logical operations. Studia Logica, 64:3–20, 2000.CrossRefGoogle Scholar
  39. 149.
    H. Wansing. Sequent systems for modal logics. In Handbook of Philosophical Logic, Vol 8, pp. 61–145. Kluwer, Dordrecht, 2002.Google Scholar
  40. 151.
    J. Zucker and R. Tragesser. The adequacy problem for inferential logic. Journal of Philosophical Logic, 7:501–516, 1978.Google Scholar
  41. 1.
    Aristotle. Posterior Analytics. Clarendon Press, Oxford, 1993.Google Scholar
  42. 120.
    G. Sambin, G. Battilotti, and C. Faggian. Basic logic: Reflection, symmetry, visibility. Journal of Symbolic Logic, 65:979–1013, 2000.CrossRefGoogle Scholar
  43. 30.
    R. Descartes. Rules for the Direction of the Mind, Discourse on the Method, Meditations on First Philosophy, Objections against the Meditations and Replies, The Geometry. William Benton, Chicago, London, Toronto, Geneva, Sydney, Tokyo, Manila, 1952.Google Scholar
  44. 32.
    K. Došen. Sequent systems and groupoid models I. Studia Logica, 47:353–389, 1988.CrossRefGoogle Scholar
  45. 41.
    Galileo. Dialogue Concerning the Two Chief World Systems, Ptolemaic and Copernican. University of California Press, Berkley, 1967.Google Scholar
  46. 42.
    G. Gentzen. Investigations into logical deductions. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam, 1969.Google Scholar
  47. 44.
    J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, Cambridge, 1989.Google Scholar
  48. 56.
    T. Heath. A history of Greek Mathematics, Vol.1. Courier Dover Publications, New York, 1981.Google Scholar
  49. 93.
    F. Paoli. Bolzano e le dimostrazioni matematiche. Rivista di Filosofia, LXXVIII:221–242, 1991.Google Scholar
  50. 96.
    Pappus. Book 7 of the Collections. Springer, New York-Berlin-Heidelberg-Tokyo, 1986.Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2010

Authors and Affiliations


Personalised recommendations