A Simple Proof That Super-Consistency Implies Cut Elimination

Gilles Dowek, Olivier Hermant

We give a simple and direct proof that super-consistency implies the cut elimination property in deduction modulo. This proof can be seen as a simplification of the proof that supe…