Algebraic proofs of cut elimination

Jeremy Avigad
Carnegie Mellon University
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.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 45,662
Through your library

References found in this work BETA

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.
The Correspondence Between Cut-Elimination and Normalization.J. Zucker - 1974 - Annals of Mathematical Logic 7 (1):1-112.
Two Applications of Boolean Models.Thierry Coquand - 1998 - Archive for Mathematical Logic 37 (3):143-147.

Add more references

Citations of this work BETA

Forcing in Proof Theory.Jeremy Avigad - 2004 - Bulletin of Symbolic Logic 10 (3):305-333.
Saturated Models of Universal Theories.Jeremy Avigad - 2002 - Annals of Pure and Applied Logic 118 (3):219-234.
Kripke Models for Classical Logic.Danko Ilik, Gyesik Lee & Hugo Herbelin - 2010 - Annals of Pure and Applied Logic 161 (11):1367-1378.

View all 6 citations / Add more citations

Similar books and articles


Added to PP index

Total views
48 ( #182,497 of 2,280,776 )

Recent downloads (6 months)
2 ( #573,575 of 2,280,776 )

How can I increase my downloads?


My notes

Sign in to use this feature