A note on the proof theory the λII-calculus

Studia Logica 54 (2):199 - 230 (1995)
  Copy   BIBTEX

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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,369

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Varieties of linear calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
On the logic of β -pregroups.Aleksandra Kiślak-Malinowska - 2007 - Studia Logica 87 (2-3):323 - 342.
Sequent calculus in natural deduction style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.

Analytics

Added to PP
2009-01-28

Downloads
86 (#198,289)

6 months
14 (#186,781)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

David Pym
University College London

Citations of this work

No citations found.

Add more citations

References found in this work

Natural deduction: a proof-theoretical study.Dag Prawitz - 1965 - Mineola, N.Y.: Dover Publications.
First-order logic.Raymond Merrill Smullyan - 1968 - New York [etc.]: Springer Verlag.
Mathematical logic.Stephen Cole Kleene - 1967 - Mineola, N.Y.: Dover Publications.
First-order Logic.William Craig - 1975 - Journal of Symbolic Logic 40 (2):237-238.
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