Document Open Access Logo

Classical Natural Deduction from Truth Tables

Authors Herman Geuvers , Tonny Hurkens



PDF
Thumbnail PDF

File

LIPIcs.TYPES.2022.2.pdf
  • Filesize: 0.76 MB
  • 27 pages

Document Identifiers

Author Details

Herman Geuvers
  • Radboud University, Nijmegen, The Netherlands
  • Technical University Eindhoven, The Netherlands
Tonny Hurkens
  • Unaffiliated Researcher, Haps, The Netherlands

Acknowledgements

We want to thank the reviewers for their valuable comments.

Cite AsGet BibTex

Herman Geuvers and Tonny Hurkens. Classical Natural Deduction from Truth Tables. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 2:1-2:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TYPES.2022.2

Abstract

In earlier articles we have introduced truth table natural deduction which allows one to extract natural deduction rules for a propositional logic connective from its truth table definition. This works for both intuitionistic logic and classical logic. We have studied the proof theory of the intuitionistic rules in detail, giving rise to a general Kripke semantics and general proof term calculus with reduction rules that are strongly normalizing. In the present paper we study the classical rules and give a term interpretation to classical deductions with reduction rules. As a variation we define a multi-conclusion variant of the natural deduction rules as it simplifies the study of proof term reduction. We show that the reduction is normalizing and gives rise to the sub-formula property. We also compare the logical strength of the classical rules with the intuitionistic ones and we show that if one non-monotone connective is classical, then all connectives become classical.

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
  • Natural deduction
  • classical proposition logic
  • multiple conclusion natural deduction
  • proof terms
  • formulas-as-types
  • proof normalization
  • subformula property
  • Curry-Howard isomorphism

Metrics

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

References

  1. Andreas Abel. On model-theoretic strong normalization for truth-table natural deduction. In Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch, editors, 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy, volume 188 of LIPIcs, pages 1:1-1:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.TYPES.2020.1.
  2. Z. Ariola and H. Herbelin. Minimal classical logic and control operators. In ICALP, volume 2719 of LNCS, pages 871-885. Springer, 2003. Google Scholar
  3. T. Crolard. A formulae-as-types interpretation of subtractive logic. J. Log. Comput., 14(4):529-570, 2004. Google Scholar
  4. P.-L. Curien and H. Herbelin. The duality of computation. In ICFP, pages 233-243, 2000. Google Scholar
  5. N Francez and R Dyckhoff. A note on harmony. Journal of Philosophical Logic, 41(3):613-628, June 2012. URL: https://doi.org/10.1007/s10992-011-9208-0.
  6. H Geuvers and T Hurkens. Deriving natural deduction rules from truth tables. In Logic and Its Applications - 7th Indian Conference, ICLA 2017, Kanpur, India, January 5-7, 2017, Proceedings, volume 10119 of Lecture Notes in Computer Science, pages 123-138, 2017. URL: https://doi.org/10.1007/978-3-662-54069-5_10.
  7. H Geuvers and T Hurkens. Proof terms for generalized natural deduction. In Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi, editors, 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, volume 104 of LIPIcs, pages 3:1-3:39. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.TYPES.2017.3.
  8. H. Geuvers, I. van der Giessen, and T. Hurkens. Strong normalization for truth table natural deduction. Fundam. Inform., 170(1-3):139-176, 2019. Google Scholar
  9. Tomoaki Kawano, Naosuke Matsuda, and Kento Takagi. Effect of the choice of connectives on the relation between classical logic and intuitionistic logic. Notre Dame Journal of Formal Logic, 63(2), 2022. URL: https://doi.org/10.1215/00294527-2022-0016.
  10. Peter Milne. Inversion principles and introduction rules. In Heinrich Wansing, editor, Dag Prawitz on Proofs and Meaning, pages 189-224. Springer International Publishing, Cham, 2015. URL: https://doi.org/10.1007/978-3-319-11041-7_8.
  11. S. Negri and J. von Plato. Structural Proof Theory. Cambridge University Press, 2001. Google Scholar
  12. Grigory K. Olkhovikov and Peter Schroeder-Heister. On flattening elimination rules. Rev. Symb. Log., 7(1):60-72, 2014. URL: https://doi.org/10.1017/S1755020313000385.
  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. S Read. Harmony and autonomy in classical logic. Journal of Philosophical Logic, 29(2):123-154, 2000. URL: https://doi.org/10.1023/A:1004787622057.
  16. Peter Schroeder-Heister. The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony. Stud Logica, 102(6):1185-1216, 2014. URL: https://doi.org/10.1007/s11225-014-9562-3.
  17. A.S. Troelstra and D. van Dalen. Constructivism in Mathematics, volume I. Number volume 121 in Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1988. Google Scholar
  18. I. van der Giessen. Natural deduction derived from truth tables, Master Thesis Mathematics, Radboud University Nijmegen, July 2018. URL: http://www.cs.ru.nl/~herman/PUBS/Masterscriptie_IrisvanderGiessen.pdf.
  19. 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