A Simple Proof That Super-Consistency Implies Cut Elimination

Abstract. We give a simple and direct proof that super-consistency implies cut elimination in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes ideas from the semantic proofs of cut elimination that proceed by proving the completeness of the cut free calculus. In particular, it gives a generalization, to all super-consistent theories, of the notion of V-complex, introduced in the semantic cut elimination proofs for simple type theory.

• Type: Conference
• Year: 2007
• Where: RTA
• Authors: Gilles Dowek, Olivier Hermant
• Keywords: Cut Elimination, Cut Elimination Proofs, RTA 2007, Super-consistency Implies Proof, Theoretical Computer Science