Authors: Barteld Kooi and Allard Tamminga

Within the context of Gentzen-calculi for classical propositional logic we present an algorithm that constructs a left rule from a right rule (and vice versa). First, we show that the algorithm is correct. Second, we use our algorithm to analyse the relation between proof-theoretical semantics (the meaning of an operator is given by its inference rules) and model-theoretical semantic (the meaning of an operator is given by its truth- and falsity-conditions). Third, we use our algorithm to study the concept of harmony and show what is wrong with Prior’s pair of rules for tonk.

In Gentzen-calculi for classical logic every operator has a left rule and a right rule. Bearing Prior’s challenge in mind, it has often been noted (first by Gentzen himself) that left rules and right rules are dependent, but as yet it is still under debate how this relation must be understood. In the context of natural deduction systems, Prawitz proposes his “Inversion Principle” to make this relation more precise. Crudely speaking, his principle says that an introduction rule followed by an elimination rule can never lead to anything beyond the original premises.

Using our correspondence analysis for proof systems and truth- and falsity-conditions, we note that left rules correspond to falsity-conditions and that right rules correspond to truth-conditions. This observation lies at the basis of our algorithm that constructs left rules from right rules (and vice versa). Accordingly, we offer a novel perspective on harmony, the balance between left rules and right rules (or within the context of natural deduction systems, between introduction and elimination rules). We say that a left rule \(L\) and a right rule \(R\) are harmonious if and only if our algorithm applied to \(L\) constructs a right rule \(R'\) that is inferentially equivalent to \(R\) (and vice versa).