Document Open Access Logo

Proof Terms for Generalized Natural Deduction

Authors Herman Geuvers, Tonny Hurkens

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2017.3.pdf
  • Filesize: 0.54 MB
  • 39 pages

Document Identifiers

Author Details

Herman Geuvers
  • Radboud University Nijmegen & Technical University Eindhoven, The Netherlands
Tonny Hurkens
  • Radboud University Nijmegen & Technical University Eindhoven, The Netherlands

Cite AsGet BibTex

Herman Geuvers and Tonny Hurkens. Proof Terms for Generalized Natural Deduction. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 3:1-3:39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TYPES.2017.3

Abstract

In previous work it has been shown how to generate natural deduction rules for propositional connectives from truth tables, both for classical and constructive logic. The present paper extends this for the constructive case with proof-terms, thereby extending the Curry-Howard isomorphism to these new connectives. A general notion of conversion of proofs is defined, both as a conversion of derivations and as a reduction of proof-terms. It is shown how the well-known rules for natural deduction (Gentzen, Prawitz) and general elimination rules (Schroeder-Heister, von Plato, and others), and their proof conversions can be found as instances. As an illustration of the power of the method, we give constructive rules for the nand logical operator (also called Sheffer stroke). As usual, conversions come in two flavours: either a detour conversion arising from a detour convertibility, where an introduction rule is immediately followed by an elimination rule, or a permutation conversion arising from an permutation convertibility, an elimination rule nested inside another elimination rule. In this paper, both are defined for the general setting, as conversions of derivations and as reductions of proof-terms. The properties of these are studied as proof-term reductions. As one of the main contributions it is proved that detour conversion is strongly normalizing and permutation conversion is strongly normalizing: no matter how one reduces, the process eventually terminates. Furthermore, the combination of the two conversions is shown to be weakly normalizing: one can always reduce away all convertibilities.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
  • Theory of computation → Functional constructs
Keywords
  • constructive logic
  • natural deduction
  • detour conversion
  • permutation conversion
  • normalization Curry-Howard isomorphism

Metrics

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

References

  1. Z. Ariola and H. Herbelin. Minimal Classical Logic and Control Operators. In ICALP, volume 2719 of LNCS, pages 871-885. Springer, 2003. Google Scholar
  2. P.-L. Curien and H. Herbelin. The duality of computation. In ICFP, pages 233-243, 2000. Google Scholar
  3. R. Dyckhoff. Some Remarks on Proof-Theoretic Semantics. In Advances in Proof-Theoretic Semantics, pages 79-93. Springer, 2016. Google Scholar
  4. N. Francez and R. Dyckhoff. A Note on Harmony. Journal of Philosophical Logic, 41(3):613-628, 2012. URL: http://dx.doi.org/10.1007/s10992-011-9208-0.
  5. R.O. Gandy. An early proof of normalization by A.M. Turing. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, page 453–455. Academic Press Limited, 1980. Google Scholar
  6. G. Gentzen. Untersuchungen über das logische Schliessen. Mathematische Zeitschrift, pages 176–210, 405–431, 1935. English translation in [19]. Google Scholar
  7. H. Geuvers and T. Hurkens. Deriving Natural Deduction Rules from Truth Tables. In ICLA, volume 10119 of Lecture Notes in Computer Science, pages 123-138. Springer, 2017. Google Scholar
  8. J.-Y. Girard et al. Proofs and types, volume 7 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge, 1989. Google Scholar
  9. F. Joachimski and R. Matthes. Short proofs of normalization for the simply- typed lambda-calculus, permutative conversions and Gödel’s T. Arch. Math. Log., 42(1):59-87, 2003. Google Scholar
  10. E.G.K López-Escobar. Standardizing the N systems of Gentzen. In Models, Algebras and Proofs, volume 203 of Lecture Notes in Pure and Applied Mathematics, page 411–434. Marcel Dekker Inc., New York, 1999. Google Scholar
  11. P. Milne. Inversion Principles and Introduction Rules. In Dag Prawitz on Proofs and Meaning, volume 7 of Outstanding Contributions to Logic, pages 189-224. Springer, 2015. Google Scholar
  12. S. Negri and J. von Plato. Structural Proof Theory. Cambridge University Press, 2001. Google Scholar
  13. M. Parigot. λμ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In LPAR, volume 624 of LNCS, pages 190-201. Springer, 1992. Google Scholar
  14. D. Prawitz. Natural deduction: a proof-theoretical study. Almqvist &Wiksell, 1965. Google Scholar
  15. D. Prawitz. Ideas and Results in Proof Theory. In J. Fenstad, editor, 2nd Scandinavian Logic Symposium, pages 237-309. North-Holland, 1971. Google Scholar
  16. S. Read. Harmony and Autonomy in Classical Logic. J. Philosophical Logic, 29(2):123-154, 2000. URL: http://dx.doi.org/10.1023/A:1004787622057.
  17. P. Schroeder-Heister. A Natural Extension of Natural Deduction. J. Symb. Log., 49(4):1284-1300, 1984. Google Scholar
  18. Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics). Elsevier Science Inc., New York, NY, USA, 2006. Google Scholar
  19. M.E. Szabo. The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969. Google Scholar
  20. W.W. Tait. Intensional Interpretations of Functionals of Finite Type I. J. Symb. Log., 32(2):198-212, 1967. URL: http://dx.doi.org/10.2307/2271658.
  21. N. Tennant. Ultimate Normal Forms for Parallelized Natural Deductions. Logic Journal of the IGPL, 10(3):299-337, 2002. Google Scholar
  22. D. van Dalen. Logic and structure (3. ed.). Universitext. Springer, 1994. Google Scholar
  23. J. von Plato. Natural deduction with general elimination rules. Arch. Math. Log., 40(7):541-567, 2001. 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact