Proof Terms for Generalized Natural Deduction
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
Theory of computation~Proof theory
Theory of computation~Type theory
Theory of computation~Constructive mathematics
Theory of computation~Functional constructs
3:1-3:39
Regular Paper
Herman
Geuvers
Herman Geuvers
Radboud University Nijmegen & Technical University Eindhoven, The Netherlands
Tonny
Hurkens
Tonny Hurkens
Radboud University Nijmegen & Technical University Eindhoven, The Netherlands
10.4230/LIPIcs.TYPES.2017.3
Z. Ariola and H. Herbelin. Minimal Classical Logic and Control Operators. In ICALP, volume 2719 of LNCS, pages 871-885. Springer, 2003.
P.-L. Curien and H. Herbelin. The duality of computation. In ICFP, pages 233-243, 2000.
R. Dyckhoff. Some Remarks on Proof-Theoretic Semantics. In Advances in Proof-Theoretic Semantics, pages 79-93. Springer, 2016.
N. Francez and R. Dyckhoff. A Note on Harmony. Journal of Philosophical Logic, 41(3):613-628, 2012. URL: http://dx.doi.org/10.1007/s10992-011-9208-0.
http://dx.doi.org/10.1007/s10992-011-9208-0
R.O. Gandy. An early proof of normalization by A.M. Turing. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, page 453–455. Academic Press Limited, 1980.
G. Gentzen. Untersuchungen über das logische Schliessen. Mathematische Zeitschrift, pages 176–210, 405–431, 1935. English translation in [19].
H. Geuvers and T. Hurkens. Deriving Natural Deduction Rules from Truth Tables. In ICLA, volume 10119 of Lecture Notes in Computer Science, pages 123-138. Springer, 2017.
J.-Y. Girard et al. Proofs and types, volume 7 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge, 1989.
F. Joachimski and R. Matthes. Short proofs of normalization for the simply- typed lambda-calculus, permutative conversions and Gödel’s T. Arch. Math. Log., 42(1):59-87, 2003.
E.G.K López-Escobar. Standardizing the N systems of Gentzen. In Models, Algebras and Proofs, volume 203 of Lecture Notes in Pure and Applied Mathematics, page 411–434. Marcel Dekker Inc., New York, 1999.
P. Milne. Inversion Principles and Introduction Rules. In Dag Prawitz on Proofs and Meaning, volume 7 of Outstanding Contributions to Logic, pages 189-224. Springer, 2015.
S. Negri and J. von Plato. Structural Proof Theory. Cambridge University Press, 2001.
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.
D. Prawitz. Ideas and Results in Proof Theory. In J. Fenstad, editor, 2nd Scandinavian Logic Symposium, pages 237-309. North-Holland, 1971.
S. Read. Harmony and Autonomy in Classical Logic. J. Philosophical Logic, 29(2):123-154, 2000. URL: http://dx.doi.org/10.1023/A:1004787622057.
http://dx.doi.org/10.1023/A:1004787622057
P. Schroeder-Heister. A Natural Extension of Natural Deduction. J. Symb. Log., 49(4):1284-1300, 1984.
Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics). Elsevier Science Inc., New York, NY, USA, 2006.
M.E. Szabo. The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969.
W.W. Tait. Intensional Interpretations of Functionals of Finite Type I. J. Symb. Log., 32(2):198-212, 1967. URL: http://dx.doi.org/10.2307/2271658.
http://dx.doi.org/10.2307/2271658
N. Tennant. Ultimate Normal Forms for Parallelized Natural Deductions. Logic Journal of the IGPL, 10(3):299-337, 2002.
D. van Dalen. Logic and structure (3. ed.). Universitext. Springer, 1994.
J. von Plato. Natural deduction with general elimination rules. Arch. Math. Log., 40(7):541-567, 2001.
Herman Geuvers and Tonny Hurkens
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode