A note on the proof theory the λII-calculus
Studia Logica 54 (2):199 - 230 (1995)
| Abstract | The II-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 II-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 | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,653 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesKai Brünnler (2006). Cut Elimination Inside a Deep Inference System for Classical Predicate Logic. Studia Logica 82 (1):51 - 71.
Sara Negri & Jan von Plato (2001). Sequent Calculus in Natural Deduction Style. Journal of Symbolic Logic 66 (4):1803-1816.
Branislav R. Boričić (1988). A Note on Sequent Calculi Intermediate Between LJ and LK. Studia Logica 47 (2):151 - 157.
Aleksandra Kiślak-Malinowska (2007). On the Logic of Β -Pregroups. Studia Logica 87 (2-3):323 - 342.
Sara Negri (2011). Proof Analysis: A Contribution to Hilbert's Last Problem. Cambridge University Press.
George Tourlakis (2010). On the Proof-Theory of Two Formalisations of Modal First-Order Logic. Studia Logica 96 (3):349-373.
Sara Negri (2002). Varieties of Linear Calculi. Journal of Philosophical Logic 31 (6):569-590.
Maria Luisa Bonet & Samuel R. Buss (1993). The Deduction Rule and Linear and Near-Linear Proof Simulations. Journal of Symbolic Logic 58 (2):688-709.
Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. Studia Logica 60 (1):107-118.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads8 ( #122,951 of 548,984 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
