Abstract
Gentzen’s sequent calculi LK and LJ are landmark proof systems. They identify the structural rules of weakening and contraction as notable inference rules, and they allow for an elegant statement and proof of both cut elimination and consistency for classical and intuitionistic logics. Among the undesirable features of those sequent calculi is that their inferences rules are low-level and frequently permute over each other. As a result, large-scale structures within sequent calculus proofs are hard to identify. In this paper, we present a different approach to designing a sequent calculus for classical logic. Starting with Gentzen’s LK proof system, we examine the proof search meaning of his inference rules and classify those rules as involving either don’t care nondeterminism or don’t know nondeterminism. Based on that classification, we design the focused proof system LKF in which inference rules belong to one of two phases of proof construction depending on which flavor of nondeterminism they involve. We then prove that the cut rule and the general form of the initial rule are admissible in LKF. Finally, by showing that the inference rules for LK are all admissible in LKF, we can give a relative completeness proof for LKF provability with respect to LK provability. We shall also apply these properties of the LKF proof system to establish other meta-theoretic properties of classical logic, including Herbrand’s theorem.
Chapter PDF
Similar content being viewed by others
References
Andreoli, J. M. (1992). Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2, 297–347. doi: https://doi.org/10.1093/logcom/2.3.297.
Chaudhuri, K., S. Hetzl, and D. Miller (2016). A multi-focused proof system isomorphic to expansion proofs. Journal of Logic and Computation 26, 577–603. doi: https://doi.org/10.1093/logcom/exu030.
Chaudhuri, K., D. Miller, and A. Saurin (2008). Canonical sequent proofs via multifocusing. In: Fifth International Conference on Theoretical Computer Science. Ed. by G. Ausiello, J. Karhumäki, G. Mauri, and L. Ong. Vol. 273. IFIP. Springer, 383–396. doi: https://doi.org/10.1007/978-0-387-09680-3_26.
Chaudhuri, K., F. Pfenning, and G. Price (2008). A logical characterization of forward and backward chaining in the inverse method. Journal of Automated Reasoning 40, 133–177. doi: https://doi.org/10.1007/s10817-007-9091-0.
Chihani, Z., D. Miller, and F. Renaud (2017). Asemantic framework for proof evidence. Journal of Automated Reasoning 59, 297–330. doi: https://doi.org/10.1007/s10817-016-9380-6.
Curien, P.-L. and H. Herbelin (2000). The duality of computation. In: ICFP ’00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming. New York: ACM Press, 233–243. doi: https://doi.org/10.1145/357766.351262.
Danos, V., J. B. Joinet, and H. Schellinx (1995). LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In: Advances in Linear Logic. Ed. by J.-Y. Girard, Y. Lafont, and L. Regnier. Vol. 22. London Mathematical Society Lecture Note Series. Cambridge University Press, 211–224.
Danos, V., J.-B. Joinet, and H. Schellinx (1997). A new deconstructive logic: linear logic. Journal of Symbolic Logic 62, 755–807. doi: https://doi.org/10.2307/2275572.
Delande, O. and D. Miller (2008). A neutral approach to proof and refutation in MALL. In: 23th Symposium on Logic in Computer Science. Ed. by F. Pfenning. IEEE Computer Society Press, 498–508. doi: https://doi.org/10.1016/j.apal.2009.07.017.
Delande, O., D. Miller, and A. Saurin (2010). Proof and refutation in MALL as a game. Annals of Pure and Applied Logic 161, 654–672. doi: https://doi.org/10.1016/j.apal.2009.07.017.
Gentzen, G. (1935). Investigations into logical deduction. In: The Collected Papers of Gerhard Gentzen. Ed. by M. E. Szabo. Translation of articles that appeared in 1934-35. Collected papers appeared in 1969. Amsterdam: North-Holland, 68–131. doi: https://doi.org/10.1007/BF01201353.
Gérard, U. and D. Miller (2017). Separating functional computation from relations. In: 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Ed. by V. Goranko and M. Dam. Vol. 82. LIPIcs, 23:1–23:17. doi: https://doi.org/10.4230/LIPIcs. CSL.2017.23.
Girard, J. Y., P. Taylor, and Y. Lafont (1989). Proofs and Types. Cambridge University Press.
Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science 50, 1–102. doi: https://doi.org/10.1016/0304-3975(87)90045-4.
Girard, J.-Y. (1991). A new constructive logic: classical logic. Mathematical Structures in Computer Science 1, 255–296. doi: https://doi.org/10.1017/S0960129500001328.
Guglielmi, A. and T. Gunderson (2008). Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science 1.
Hallnäs, L. and P. Schroeder-Heister (1990). A proof-theoretic approach to logic programming. I. Clauses as rules. Journal of Logic and Computation 1, 261–283. doi: https://doi.org/10.1093/logcom/1.2.261.
Heath, Q. and D. Miller (2019). A proof theory for model checking. Journal of Automated Reasoning 63, 857–775. doi: https://doi.org/10.1007/s10817-018-9475-3.
Herbelin, H. (1995). A lambda-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Computer Science Logic, 8th International Workshop, CSL ’94. Vol. 933. Lecture Notes in Computer Science. Springer, 61–75. doi: https://doi.org/10.1007/BFb0022247.
Kleene, S. C. (1952). Permutability of inferences in Gentzen’s calculi LK and LJ. Memoirs of the American Mathematical Society 10, 1–26.
Laurent, O. (2004). A proof of the focalization property of linear logic. Unpublished note.
Laurent, O. (2011). Intuitionistic dual-intuitionistic nets. Journal of Logic and Computation 21, 561–587. doi: https://doi.org/10.1093/logcom/exp044.
Liang, C. and C. Miller (2011). A focused approach to combining logics. Annals of Pure and Applied Logic 10, 679–697. doi: https://doi.org/10.1016/j.apal.2011.01.012.
Liang, C. and D. Miller (2009). Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science 410, 4747–4768. doi: https://doi.org/10.1016/j.tcs.2009.07.041.
Miller, D. (1987). A compact representation of proofs. Studia Logica 46, 347–370. doi: https://doi.org/10.1007/BF00370646.
Liang, C. and D. Miller (1989). A logical analysis of modules in logic programming. Journal of Logic Programming 6, 79–108. doi: https://doi.org/10.1016/0743-1066(89)90031-9.
Miller, D., G. Nadathur, F. Pfenning, and A. Scedrov (1991). Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51, 125–157. doi: https://doi.org/10.1016/0168-0072(91)90068-W.
Negri, S. and J. von Plato (1998). Cut elimination in the presence of axioms. Bulletin of Symbolic Logic 4, 418–435. doi: https://doi.org/10.2307/420956.
Pimentel, E., V. Nigam, and J. Neto (2016). Multi-focused proofs with different polarity assignments. In: Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015). Vol. 323. ENTCS, 163–179. doi: https://doi.org/10.1016/j.entcs.2016.06.011.
Scherer, G. (2016). Which types have a unique inhabitant? Focusing on pure program equivalence. PhD thesis. Université Paris-Diderot.
Simmons, R. J. (2014). Structural focalization. ACM Transaction on Computational Logic 15. doi: https://doi.org/10.1145/2629678.
Simmons, R. J. and F. Pfenning (2011). Weak focusing for ordered linear logic. Technical Report. CMU-CS-10-147, Carnegie Mellon University.
von Plato, J. (2012). Gentzen’s proof systems: byproducts in a work of genius. Bulletin of Symbolic Logic 18, 313–367. doi: https://doi.org/10.2178/bsl/1344861886.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution-ShareAlike 4.0 International License (http://creativecommons.org/licenses/by-sa/4.0/), which permits use, sharing, adaptation, distribution, and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. If you remix, transform, or build upon this chapter or a part thereof, you must distribute your contributions under the same license as the original.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2024 The Author(s)
About this chapter
Cite this chapter
Liang, C., Miller, D. (2024). Focusing Gentzen’s LK Proof System. In: Piecha, T., Wehmeier, K.F. (eds) Peter Schroeder-Heister on Proof-Theoretic Semantics. Outstanding Contributions to Logic, vol 29. Springer, Cham. https://doi.org/10.1007/978-3-031-50981-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-031-50981-0_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-50980-3
Online ISBN: 978-3-031-50981-0
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)