Cut Elimination in the Intuitionistic Theory of Types with Axioms and Rewriting Cuts, Constructively

Abstract : We give a fully constructive semantic proof of cut elimination for intuitionistic type theory with axioms. The problem here, as with the original Takeuti conjecture, is that the impredicativity of the formal system involved makes it impossible to define a semantics along conventional lines, in the absence, a priori, of cut, or to prove completeness by induction on subformula structure. In addition, unlike semantic proofs by Tait, Takahashi, and Andrews of variants of the Takeuti conjecture, our arguments are constructive. Our techniques offer also an easier approach than Girard's strong normalization techniques to the problem of extending the cut-elimination result in the presence of axioms. We need only to relativize the Heyting algebras involved in a straightforward way.
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-00912791
Contributeur : Claire Medrala <>
Soumis le : lundi 2 décembre 2013 - 16:18:06
Dernière modification le : vendredi 29 septembre 2017 - 14:36:04
Document(s) archivé(s) le : lundi 3 mars 2014 - 10:06:36

Fichier

FESTSCHRIFT-Hermant-2008.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00912791, version 1

Collections

Citation

Olivier Hermant, James Lipton. Cut Elimination in the Intuitionistic Theory of Types with Axioms and Rewriting Cuts, Constructively. Studies in Logic and te Foundations of Mathematics, 2008, pp 101-134. ⟨hal-00912791⟩

Partager

Métriques

Consultations de la notice

221

Téléchargements de fichiers

87