A simple proof that super consistency implies cut elimination - Archive ouverte HAL Accéder directement au contenu
Article Dans Une Revue Notre Dame Journal of Formal Logic Année : 2012

A simple proof that super consistency implies cut elimination

(1) , (2)
1
2

Résumé

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.
Fichier principal
Vignette du fichier
A-516.pdf (317.94 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...

Dates et versions

hal-00793008 , version 1 (21-02-2013)

Identifiants

Citer

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

Altmetric

Partager

Gmail Facebook Twitter LinkedIn More