General-elimination harmony and higher-level rules

Michael Dummett introduced the notion of harmony in response to Arthur Prior's tonkish attack on the idea of proof-theoretic justification of logical laws (or analytic validity). But Dummett vacillated between different conceptions of harmony, in an attempt to use the idea to underpin his anti-realism. Dag Prawitz had already articulated an idea of Gerhard Gentzen's into a procedure whereby elimination-rules are in some sense functions of the corresponding introduction-rules. The resulting conception of general-elimination harmony ensures that the rules are transparent in the meaning they confer, in that the elimination-rules match the meaning the introduction-rules confer. The general-elimination rules which result may be of higher level, in that the assumptions discharged by the rule may be of (the existence of) derivations rather than just of formulae. In many cases, such higher-level rules may be "flattened" to rules discharging only formulae. However, such flattening is often only possible in the richer context of so-called ''classical" or realist negation, or in a multiple-conclusion environment. In a constructivist context, the flattened rules are harmonious but not stable.