{"@context":"https:\/\/schema.org\/","@type":"ScholarlyArticle","@id":"#article7122","name":"A Semantic Proof that Reducibility Candidates entail Cut Elimination","abstract":"Two main lines have been adopted to prove the cut elimination theorem:\r\nthe syntactic one, that studies the process of reducing cuts, and the\r\nsemantic one, that consists in interpreting a sequent in some algebra\r\nand extracting from this interpretation a cut-free proof of this very\r\nsequent.\r\n\r\nA link between those two methods was exhibited by studying in a\r\nsemantic way, syntactical tools that allow to prove (strong)\r\nnormalization of proof-terms, namely reducibility candidates. In the\r\ncase of deduction modulo, a framework combining deduction and\r\nrewriting rules in which theories like Zermelo set theory and higher\r\norder logic can be expressed, this is obtained by constructing a\r\nreducibility candidates valued model. The existence of such a pre-model for a theory entails strong normalization of its\r\nproof-terms and, by the usual syntactic argument, the cut elimination\r\nproperty.\r\n\r\nIn this paper, we strengthen this gate between syntactic and semantic\r\nmethods, by providing a full semantic proof that the existence of a\r\npre-model entails the cut elimination property for the considered\r\ntheory in deduction modulo. We first define a new simplified variant\r\nof reducibility candidates \u00e0 la Girard, that is sufficient to\r\nprove weak normalization of proof-terms (and therefore the cut\r\nelimination property). Then we build, from some model valued on the\r\npre-Heyting algebra of those WN reducibility candidates, a regular\r\nmodel valued on a Heyting algebra on which we apply the usual\r\nsoundness\/strong completeness argument.\r\n\r\nFinally, we discuss further extensions of this new method towards\r\nnormalization by evaluation techniques that commonly use Kripke\r\nsemantics.","keywords":["cut elimination","reducibility candidates","(pre-)Heyting algebras"],"author":[{"@type":"Person","name":"Cousineau, Denis","givenName":"Denis","familyName":"Cousineau"},{"@type":"Person","name":"Hermant, Olivier","givenName":"Olivier","familyName":"Hermant"}],"position":12,"pageStart":133,"pageEnd":148,"dateCreated":"2012-05-29","datePublished":"2012-05-29","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"Cousineau, Denis","givenName":"Denis","familyName":"Cousineau"},{"@type":"Person","name":"Hermant, Olivier","givenName":"Olivier","familyName":"Hermant"}],"copyrightYear":"2012","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2012.133","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":{"@type":"PublicationVolume","@id":"#volume6218","volumeNumber":15,"name":"23rd International Conference on Rewriting Techniques and Applications (RTA'12)","dateCreated":"2012-05-29","datePublished":"2012-05-29","editor":{"@type":"Person","name":"Tiwari, Ashish","givenName":"Ashish","familyName":"Tiwari"},"isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#article7122","isPartOf":{"@type":"Periodical","@id":"#series116","name":"Leibniz International Proceedings in Informatics","issn":"1868-8969","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume6218"}}}