Classical Natural Deduction from Truth Tables

Geuvers, Herman; Hurkens, Tonny

doi:10.4230/LIPIcs.TYPES.2022.2

File

LIPIcs.TYPES.2022.2.pdf

Filesize: 0.76 MB
27 pages

Document Identifiers

DOI: 10.4230/LIPIcs.TYPES.2022.2
URN: urn:nbn:de:0030-drops-184450

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

0

Metadata Views

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.