Cousineau, Denis ;
Hermant, Olivier
A Semantic Proof that Reducibility Candidates entail Cut Elimination
Abstract
Two main lines have been adopted to prove the cut elimination theorem:
the syntactic one, that studies the process of reducing cuts, and the
semantic one, that consists in interpreting a sequent in some algebra
and extracting from this interpretation a cutfree proof of this very
sequent.
A link between those two methods was exhibited by studying in a
semantic way, syntactical tools that allow to prove (strong)
normalization of proofterms, namely reducibility candidates. In the
case of deduction modulo, a framework combining deduction and
rewriting rules in which theories like Zermelo set theory and higher
order logic can be expressed, this is obtained by constructing a
reducibility candidates valued model. The existence of such a premodel for a theory entails strong normalization of its
proofterms and, by the usual syntactic argument, the cut elimination
property.
In this paper, we strengthen this gate between syntactic and semantic
methods, by providing a full semantic proof that the existence of a
premodel entails the cut elimination property for the considered
theory in deduction modulo. We first define a new simplified variant
of reducibility candidates à la Girard, that is sufficient to
prove weak normalization of proofterms (and therefore the cut
elimination property). Then we build, from some model valued on the
preHeyting algebra of those WN reducibility candidates, a regular
model valued on a Heyting algebra on which we apply the usual
soundness/strong completeness argument.
Finally, we discuss further extensions of this new method towards
normalization by evaluation techniques that commonly use Kripke
semantics.
BibTeX  Entry
@InProceedings{cousineau_et_al:LIPIcs:2012:3489,
author = {Denis Cousineau and Olivier Hermant},
title = {{A Semantic Proof that Reducibility Candidates entail Cut Elimination}},
booktitle = {23rd International Conference on Rewriting Techniques and Applications (RTA'12) },
pages = {133148},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897385},
ISSN = {18688969},
year = {2012},
volume = {15},
editor = {Ashish Tiwari},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2012/3489},
URN = {urn:nbn:de:0030drops34899},
doi = {10.4230/LIPIcs.RTA.2012.133},
annote = {Keywords: cut elimination, reducibility candidates, (pre)Heyting algebras}
}
2012
Keywords: 

cut elimination, reducibility candidates, (pre)Heyting algebras 
Seminar: 

23rd International Conference on Rewriting Techniques and Applications (RTA'12)

Issue date: 

2012 
Date of publication: 

2012 