Skip to Main content Skip to Navigation
Journal articles

A simple proof that super consistency implies cut elimination

Abstract : 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 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. As an application, we compare our work with the cut elimination theorems in higher-order logic that involve V-complexes.
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Claire Medrala Connect in order to contact the contributor
Submitted on : Thursday, February 21, 2013 - 2:29:24 PM
Last modification on : Friday, January 21, 2022 - 3:14:57 AM
Long-term archiving on: : Sunday, April 2, 2017 - 3:34:13 AM


Publisher files allowed on an open archive



Gilles Dowek, Olivier Hermant. A simple proof that super consistency implies cut elimination. Notre Dame Journal of Formal Logic, University of Notre Dame, 2012, 53 (4), pp. 93-106. ⟨10.1215/00294527-1722692⟩. ⟨hal-00793008⟩



Record views


Files downloads