License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2017.3
URN: urn:nbn:de:0030-drops-100519
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/10051/
Go to the corresponding LIPIcs Volume Portal

Geuvers, Herman ; Hurkens, Tonny

Proof Terms for Generalized Natural Deduction

pdf-format:
LIPIcs-TYPES-2017-3.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{geuvers_et_al:LIPIcs:2018:10051,
  author =	{Herman Geuvers and Tonny Hurkens},
  title =	{{Proof Terms for Generalized Natural Deduction}},
  booktitle =	{23rd International Conference on Types for Proofs and  Programs (TYPES 2017)},
  pages =	{3:1--3:39},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{104},
  editor =	{Andreas Abel and Fredrik Nordvall Forsberg and Ambrus Kaposi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/10051},
  URN =		{urn:nbn:de:0030-drops-100519},
  doi =		{10.4230/LIPIcs.TYPES.2017.3},
  annote =	{Keywords: constructive logic, natural deduction, detour conversion, permutation conversion, normalization Curry-Howard isomorphism}
}

Keywords: constructive logic, natural deduction, detour conversion, permutation conversion, normalization Curry-Howard isomorphism
Collection: 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
Issue Date: 2018
Date of publication: 08.01.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI