file.pdf (207.46 kB)
Download file

Algebraic Proofs of Cut Elimination

Download (207.46 kB)
journal contribution
posted on 01.01.2001, 00:00 by Jeremy AvigadJeremy Avigad
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 phi is provable classically, then ¬(¬phi)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.


Publisher Statement

All Rights Reserved



Usage metrics