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.
Type de document :
Article dans une revue
Notre Dame Journal of Formal Logic, University of Notre Dame, 2012, 53 (4), pp. 93-106. 〈10.1215/00294527-1722692〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal-mines-paristech.archives-ouvertes.fr/hal-00793008
Contributeur : Claire Medrala <>
Soumis le : jeudi 21 février 2013 - 14:29:24
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : dimanche 2 avril 2017 - 03:34:13

Fichier

A-516.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

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〉

Partager

Métriques

Consultations de la notice

338

Téléchargements de fichiers

111