文章基本信息

标题：Proof Terms for Generalized Natural Deduction
本地全文：下载
作者：Herman Geuvers ; Tonny Hurkens
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：104
页码：1-39
DOI：10.4230/LIPIcs.TYPES.2017.3
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：constructive logic; natural deduction; detour conversion; permutation conversion; normalization Curry-Howard isomorphism