LIPIcs.TYPES.2022.2.pdf
- Filesize: 0.76 MB
- 27 pages
Document
Classical Natural Deduction from Truth Tables
Authors
Herman Geuvers 
,
-
Part of:
Volume:
28th International Conference on Types for Proofs and Programs (TYPES 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-28
File
Document Identifiers
Author Details
Acknowledgements
We want to thank the reviewers for their valuable comments.
Cite As Get 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)
0PDF Downloads
References
- 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.
-
Z. Ariola and H. Herbelin. Minimal classical logic and control operators. In ICALP, volume 2719 of LNCS, pages 871-885. Springer, 2003.
-
T. Crolard. A formulae-as-types interpretation of subtractive logic. J. Log. Comput., 14(4):529-570, 2004.
-
P.-L. Curien and H. Herbelin. The duality of computation. In ICFP, pages 233-243, 2000.
- 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.
- 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.
- 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.
-
H. Geuvers, I. van der Giessen, and T. Hurkens. Strong normalization for truth table natural deduction. Fundam. Inform., 170(1-3):139-176, 2019.
- 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.
- 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.
-
S. Negri and J. von Plato. Structural Proof Theory. Cambridge University Press, 2001.
- 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.
-
M. Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In LPAR, volume 624 of LNCS, pages 190-201. Springer, 1992.
-
D. Prawitz. Natural deduction: a proof-theoretical study. Almqvist & Wiksell, 1965.
- 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.
- 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.
-
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.
- 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.
-
J. von Plato. Natural deduction with general elimination rules. Arch. Math. Log., 40(7):541-567, 2001.