Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation

摘要

Herbelin presented (at CSL'94) a simple sequent calculus for minimal implicational logic, extensible to full first-order intuitionistic logic, with a complete system of cut-reduction rules which is both confluent and strongly normalizing. Some of the cut rules may be regarded as rules to construct explicit substitutions. He observed that the addition of a cut permutation rule, for propagation of such substitutions, breaks the proof of strong normalization; the implicit conjecture is that the rule may be added without breaking strong normalization. We prove this conjecture, thus showing how to model beta-reduction in his calculus (extended with rules to allow cut permutations).