Prawitz proved a theorem, formalising ‘harmony’ in Natural Deduction systems, which showed that, corresponding to any deduction
there is one to the same effect but in which no formula occurrence is both the consequence of an application of an introduction
rule and major premise of an application of the related elimination rule. As Gentzen ordered the rules, certain rules in Classical
Logic had to be excepted, but if we see the appropriate rules instead as rules for
Contradiction, then we can extend the theorem to the classical case. Properly arranged there is a thoroughgoing ‘harmony’, in the classical
rules. Indeed, as we shall see, they are, all together, far more ‘harmonious’ in the general sense than has been commonly
observed. As this paper will show, the appearance of disharmony has only arisen because of the illogical way in which natural
deduction rules for Classical Logic have been presented.
Keywords Natural deduction - Harmony - Relevance - Epsilon calculus