Sciweavers

Share
RTA
2007
Springer

A Simple Proof That Super-Consistency Implies Cut Elimination

9 years 4 months ago
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 simpliļ¬cation 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.
Gilles Dowek, Olivier Hermant
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where RTA
Authors Gilles Dowek, Olivier Hermant
Comments (0)
books