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

Title:
Semantic A-translation and Super-consistency entail Classical Cut Elimination
Authors:
Allali, Lisa, Hermant, Olivier
Contributors:
Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X), Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre de Recherche en Informatique (CRI), Mines Paris - PSL (École nationale supérieure des mines de Paris), Université Paris Sciences et Lettres (PSL)-Université Paris Sciences et Lettres (PSL), Bernd Fischer, Geoff Sutcliffe, Ken McMillan and Aart Middeldorp and Andrei Voronkov
Source:
LPAR 19 - 19th Conference on Logic for Programming. :407-422
Publisher Information:
CCSD; Springer, 2013.
Publication Year:
2013
Collection:
collection:X
collection:ENSMP
collection:CNRS
collection:INRIA
collection:INRIA-ROCQ
collection:LIX
collection:X-LIX
collection:X-DEP
collection:X-DEP-INFO
collection:ENSMP_CRI
collection:PARISTECH
collection:INRIA_TEST
collection:TESTALAIN1
collection:INRIA2
collection:PSL
collection:ENSMP_DEP_MS
collection:INRIA-300009
collection:ENSMP_DR
collection:ENSMP-PSL
collection:DEPARTEMENT-DE-MATHEMATIQUES
Subject Terms:
Deduction modulo, cut elimination, A-translation, pseudo-Heyting algebra, super-consistency, ACM: F.: Theory of Computation, F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES, F.4.1: Mathematical Logic, F.4.1.7: Proof theory, [INFO.INFO-LO]Computer Science [cs], Logic in Computer Science [cs.LO], [MATH.MATH-LO]Mathematics [math], Logic [math.LO]
Subject Geographic:
Stellenbosch, South Africa
Original Identifier:
ARXIV: 1401.0998
HAL: hal-00923915
Document Type:
Konferenz conferenceObject<br />Conference papers
Language:
English
Relation:
info:eu-repo/semantics/altIdentifier/arxiv/1401.0998; info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-45221-5_28
DOI:
10.1007/978-3-642-45221-5_28
Access URL:
https://inria.hal.science/hal-00923915
https://inria.hal.science/hal-00923915v1/document
https://inria.hal.science/hal-00923915v1/file/SemanticTranslation.pdf
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edshal.hal.00923915v1
Database:
HAL

Weitere Informationen

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.