Relevant harmony
Nissim Francez · Journal of Logic and Computation · 2013
After reviewing the basic definitions of harmony and stability, two of the central concepts in Proof-Theoretic Semantics, the paper considers the implicational fragment of the relevant logic R (Anderson&Belnap), under a labelled natural deduction (ND) system, where the labels keep track of ‘use’ of assumptions. Thereby, no assumption is discharged that has not been used. It is shown that the ND is not closed under composition of derivations using its standard definition, thereby prohibiting Prawitz's detour removal reductions, hence failing harmony. A revised definition of derivation composition is proposed, under which the ND system *is* closed, allowing reductions and reenabling harmony (and stability).