Semantic A-translation and Super-consistency entail Classical Cut EliminationReportar como inadecuado




Semantic A-translation and Super-consistency entail Classical Cut Elimination - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LIX - Laboratoire d-informatique de l-École polytechnique Palaiseau 2 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique Inria Paris-Rocquencourt 3 CRI - Centre de Recherche en Informatique

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.

Keywords : Deduction modulo cut elimination A-translation pseudo-Heyting algebra super-consistency





Autor: Lisa Allali - Olivier Hermant -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados