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.