Algebraic proofs of cut elimination


Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be viewed as special cases of the cut-elimination theorems for intuitionistic logic.



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

External links

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

Through your library

  • Only published works are available at libraries.

Similar books and articles

Classical logic, intuitionistic logic, and the Peirce rule.Henry Africk - 1992 - Notre Dame Journal of Formal Logic 33 (2):229-235.
Proof normalization modulo.Gilles Dowek & Benjamin Werner - 2003 - Journal of Symbolic Logic 68 (4):1289-1316.
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.
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
Complete infinitary type logics.J. W. Degen - 1999 - Studia Logica 63 (1):85-119.


Added to PP

71 (#232,342)

6 months
18 (#144,337)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Jeremy Avigad
Carnegie Mellon University

References found in this work

The correspondence between cut-elimination and normalization.J. Zucker - 1974 - Annals of Mathematical Logic 7 (1):1-112.
Saturated models of universal theories.Jeremy Avigad - 2002 - Annals of Pure and Applied Logic 118 (3):219-234.
Constructive Sheaf Semantics.Erik Palmgren - 1997 - Mathematical Logic Quarterly 43 (3):321-327.
Two applications of Boolean models.Thierry Coquand - 1998 - Archive for Mathematical Logic 37 (3):143-147.
Ein Ausgezeichnetes Modell Für Die Intuitionistische Typenlogik.Wilfried Buchholz - 1975 - Archive for Mathematical Logic 17 (1-2):55-60.

Add more references