Deriving natural deduction rules from truth tables

Herman Geuvers, Tonny Hurkens

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

Abstract

We develop a general method for deriving natural deduction rules from the truth table for a connective. The method applies to both constructive and classical logic. This implies we can derive “constructively valid” rules for any classical connective. We show this constructive validity by giving a general Kripke semantics, that is shown to be sound and complete for the constructive rules. For the well-known connectives (˅, ˄, →, ¬) the constructive rules we derive are equivalent to the natural deduction rules we know from Gentzen and Prawitz. However, they have a different shape, because we want all our rules to have a standard “format”, to make it easier to define the notions of cut and to study proof reductions. In style they are close to the “general elimination rules” studied by Von Plato [13] and others. The rules also shed some new light on the classical connectives: e.g. the classical rules we derive for → allow to prove Peirce’s law. Our method also allows to derive rules for connectives that are usually not treated in natural deduction textbooks, like the “if- then-else”, whose truth table is clear but whose constructive deduction rules are not. We prove that “if-then-else”, in combination with ┴ and ┬, is functionally complete (all other constructive connectives can be defined from it). We define the notion of cut, generally for any constructive connective and we describe the process of “cut-elimination”.

Original languageEnglish
Title of host publicationLogic and Its Applications - 7th Indian Conference, ICLA 2017, Proceedings
EditorsSujata Ghosh, Sanjiva Prasad
Place of PublicationBerlin
PublisherSpringer
Pages123-138
Number of pages16
ISBN (Electronic)978-3-662-54069-5
ISBN (Print)978-3-662-54068-8
DOIs
Publication statusPublished - 1 Jan 2017
Event7th Indian Conference on Logic and Its Applications, ICLA 2017 - Kanpur, India
Duration: 5 Jan 20177 Jan 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10119 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th Indian Conference on Logic and Its Applications, ICLA 2017
CountryIndia
CityKanpur
Period5/01/177/01/17

Fingerprint Dive into the research topics of 'Deriving natural deduction rules from truth tables'. Together they form a unique fingerprint.

  • Cite this

    Geuvers, H., & Hurkens, T. (2017). Deriving natural deduction rules from truth tables. In S. Ghosh, & S. Prasad (Eds.), Logic and Its Applications - 7th Indian Conference, ICLA 2017, Proceedings (pp. 123-138). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10119 LNCS). Springer. https://doi.org/10.1007/978-3-662-54069-5_10