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 cut-free 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 proof-terms, 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 pre-model for a theory entails strong normalization of its
proof-terms 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
pre-model 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 proof-terms (and therefore the cut
elimination property). Then  we build, from some model valued on the
pre-Heyting 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.