A simple proof that super consistency implies cut elimination

Gilles Dowek (1) , Olivier Hermant (2)

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
2 CRI - Centre de Recherche en Informatique

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.

Domaines: Logique en informatique [cs.LO]; Théorie et langage formel [cs.FL]

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⟩