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 metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal-mines-paristech.archives-ouvertes.fr/hal-00793008
Contributor : Claire Medrala <>
Submitted on : Thursday, February 21, 2013 - 2:29:24 PM
Last modification on : Thursday, September 24, 2020 - 4:36:01 PM
Long-term archiving on: : Sunday, April 2, 2017 - 3:34:13 AM

File

A-516.pdf
Publisher files allowed on an open archive

Identifiers

Citation

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⟩

Share

Metrics

Record views

570

Files downloads

332