Harmony via Reductions and Expansions

The notion of harmony arises by considerations about the notion of assertion in the theory of meaning. When applied to rules in the format of natural deduction, harmony can be explained by making reference to certain transformations on derivations, called reductions and expansions. Reductions are a key ingredient of the proof of normalization for the calculus of natural deduction for intuitionistic logic. In this calculus, normal derivations that are closed (i.e. such that their conclusions depend on no assumption) end with an introduction rule, a fact which is referred to as the canonicity of closed normal derivations. The condition for the canonicity of normal derivations in a more general setting are discussed. The chapter ends with a brief discussion of other accounts of harmony.