Semantic A-translation and Super-consistency entail Classical Cut Elimination

Abstract : We show that if a theory R defined by a rewrite system is super-consistent, the classical sequent calculus modulo R enjoys the cut elimination property, which was an open question. For such theories it was already known that proofs strongly normalize in natural deduction modulo R, and that cut elimination holds in the intuitionistic sequent calculus modulo R. We first define a syntactic and a semantic version of Friedman's A-translation, showing that it preserves the structure of pseudo-Heyting algebra, our semantic framework. Then we relate the interpretation of a theory in the A-translated algebra and its A-translation in the original algebra. This allows to show the stability of the super-consistency criterion and the cut elimination theorem.
Type de document :
Communication dans un congrès
Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR 19 - 19th Conference on Logic for Programming, Artificial Intelligence, and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.407-422, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-45221-5_28〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00923915
Contributeur : Olivier Hermant <>
Soumis le : dimanche 5 janvier 2014 - 22:17:33
Dernière modification le : lundi 12 novembre 2018 - 10:55:21
Document(s) archivé(s) le : jeudi 10 avril 2014 - 16:11:20

Fichiers

SemanticTranslation.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Lisa Allali, Olivier Hermant. Semantic A-translation and Super-consistency entail Classical Cut Elimination. Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR 19 - 19th Conference on Logic for Programming, Artificial Intelligence, and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.407-422, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-45221-5_28〉. 〈hal-00923915〉

Partager

Métriques

Consultations de la notice

679

Téléchargements de fichiers

241