Algebraic Proofs of Cut Elimination
journal contributionposted 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.