Approaches based on generalised eliminations or generalised introductions maintain that these generalised rules have a distinguished status, so that harmony can be defined with respect to them. An alternative way would be to explain what it means that given introductions cI and given eliminations cE are in harmony with each other, independent of any syntactical function that generates cE from cI or vice versa. This way of proceeding has the advantage that rule sets cI and cE can be said to be in harmony without starting either from the introductions or from the eliminations as primary meaning-giving rules. That for certain syntactical functions F and G the rule sets cI and F (cI ), or cE and G (cE ), are in harmony, is then a special result and not the definiens of harmony. The canonical functions generating harmonious rules operate on sets of introduction and elimination rules for which harmony is already defined independently. This symmetry of the notion of harmony follows naturally from an intuitive understanding of the concept.

Such an approach is described for propositional logic in Schroeder-Heister [66]. Its idea is to translate the meaning of a connective c according to given introduction rules cI into a formula cI of second-order intuitionistic propositional logic IPC2, and its meaning according to given elimination rules cE into an IPC2-formula cE . Introductions and eliminations are then said to be in harmony with each other, if cI and cE are equivalent (in IPC2). The introduction and elimination meanings cI and cE can be read off the proposed introduction and elimination rules. For example, consider the connective && with the introduction and elimination rules

[ p1]

p1 p2 p1&& p2 [ p1]

r1 [ p2]

r2 [r1, r2]

r

p1 && p2 r

Its introduction meaning is p1 ∧ ( p1 → p2), and its elimination meaning is

∀r1r2r ((( p1 → r1) ∧ ( p2 → r2) ∧ ((r1 ∧ r2) → r )) → r ). As these formulas

are equivalent in IPC2, the introduction and elimination rules for && are in harmony

with each other. Further examples are discussed in Schroeder-Heister [66].

The translation into IPC2 presupposes, of course, that the connectives inherent in IPC2 are already taken for granted. Therefore, this approach works properly only for generalised connectives different from the standard ones. As it reduces semantical content to what can be expressed by formulas of IPC2, it was called a 'reductive' rather than 'foundational' approach. As described in Schroeder-Heister [63] this can be carried over to a framework that employs higher-level rules, making the reference to IPC2 redundant. However, as the handling of quantified rules in this framework corresponds to what can be carried out in IPC2 for implications, this is not a presupposition-free approach either. The viability of both approaches hinges on the notion of equivalence, that is, the idea that meanings expressed by equivalent propositions (or rules in the foundational approach), one representing the content of introduction-premisses and the other one representing the content of eliminationconclusions, is sufficient to describe harmony.

Found a mistake? Please highlight the word and press Shift + Enter