Studia Logica 54 (2):199 - 230 (1995)
Authors |
|
Abstract |
The lambdaPi-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the lambdaPi-calculus and prove the cut-elimination theorem. The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The type-theoretic setting considered here elegantly illustrates the distinction between the processes of normalization in a natural deduction system and cut-elimination in a Gentzen-style sequent calculus.
|
Keywords | No keywords specified (fix it) |
Categories | (categorize this paper) |
DOI | 10.1007/BF01063152 |
Options |
![]() ![]() ![]() ![]() |
Download options
References found in this work BETA
Natural Deduction: A Proof-Theoretical Study.Dag Prawitz - 1965 - Stockholm, Sweden: Dover Publications.
First-Order Logic.Raymond Merrill Smullyan - 1968 - Berlin, Germany: New York [Etc.]Springer-Verlag.
A Natural Extension of Natural Deduction.Peter Schroeder-Heister - 1984 - Journal of Symbolic Logic 49 (4):1284-1300.
View all 17 references / Add more references
Citations of this work BETA
No citations found.
Similar books and articles
Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 2008 - In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. CSLI Publications. pp. 43-66.
The Deduction Rule and Linear and Near-Linear Proof Simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
On the Logic of Β -Pregroups.Aleksandra Kiślak-Malinowska - 2007 - Studia Logica 87 (2-3):323 - 342.
A Note on Sequent Calculi Intermediate Between LJ and LK.Branislav R. Boričić - 1988 - Studia Logica 47 (2):151 - 157.
Sequent Calculus in Natural Deduction Style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.
Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
Analytics
Added to PP index
2009-01-28
Total views
68 ( #168,959 of 2,507,860 )
Recent downloads (6 months)
1 ( #416,715 of 2,507,860 )
2009-01-28
Total views
68 ( #168,959 of 2,507,860 )
Recent downloads (6 months)
1 ( #416,715 of 2,507,860 )
How can I increase my downloads?
Downloads