A completeness theorem for strong normalization in minimal deduction modulo
Denis Cousineau · 2009
Abstract. Deduction modulo is an extension of first-order predicate logic where axioms are replaced by rewrite rules and where many the-ories, such as arithmetic, simple type theory and some variants of set theory, can be expressed. An important question in deduction modulo is to find a condition of the theories that have the strong normalization property. Dowek and Werner have given a semantic sufficient condition for a theory to have the strong normalization property: they have proved a ”soundness ” theorem of the form: if a theory has a model (of a particu-lar form) then it has the strong normalization property. In this paper, we refine their notion of model in a way allowing not only to prove sound-ness, but also completeness: if a theory has the strong normalization property, then it has a model of this form. The key idea of our model construction is a refinement of Girard’s notion of reducibility candidates. By providing a sound and complete semantics for theories having the strong normalization property, this paper contributes to explore the idea