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 proofterms, thereby extending the CurryHoward 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 proofterms. It is shown how the wellknown rules for natural deduction (Gentzen, Prawitz) and general elimination rules (SchroederHeister, 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 proofterms. The properties of these are studied as proofterm 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:13:39},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770712},
ISSN = {18688969},
year = {2018},
volume = {104},
editor = {Andreas Abel and Fredrik Nordvall Forsberg and Ambrus Kaposi},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/10051},
URN = {urn:nbn:de:0030drops100519},
doi = {10.4230/LIPIcs.TYPES.2017.3},
annote = {Keywords: constructive logic, natural deduction, detour conversion, permutation conversion, normalization CurryHoward isomorphism}
}
Keywords: 

constructive logic, natural deduction, detour conversion, permutation conversion, normalization CurryHoward isomorphism 
Collection: 

23rd International Conference on Types for Proofs and Programs (TYPES 2017) 
Issue Date: 

2018 
Date of publication: 

08.01.2019 