On completeness of reducibility candidates as a semantics of strong normalization

TL;DR

This paper introduces a sound and complete semantic criterion for strong normalization in minimal deduction modulo using reducibility candidates, simplifying previous approaches and covering all such theories.

Contribution

It presents a new, simplified semantic criterion based on reducibility candidates for strong normalization in minimal deduction modulo, applicable to all such theories.

Findings

The criterion is sound and complete for strong normalization.

Using Curry-style proof-terms simplifies the definition and proof.

The approach applies to all theories in minimal deduction modulo.

Abstract

This paper defines a sound and complete semantic criterion, based on reducibility candidates, for strong normalization of theories expressed in minimal deduction modulo \`a la Curry. The use of Curry-style proof-terms allows to build this criterion on the classic notion of pre-Heyting algebras and makes that criterion concern all theories expressed in minimal deduction modulo. Compared to using Church-style proof-terms, this method provides both a simpler definition of the criterion and a simpler proof of its completeness.