Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

The Problem of Harmony

In the proof-theoretic semantics of logical constants, harmony is a, or perhaps the, crucial concept. If we work in a natural-deduction framework, harmony is a property that introduction and elimination rules for a logical constant are expected to satisfy with respect to each other in order to be appropriate. Harmony guarantees that we do not gain anything when applying an introduction rule followed by an elimination rule, but also, conversely, that from the result of applying elimination rules we can, by applying introduction rules, recover what we started with. The notion of harmony or 'consonance' was introduced by Dummett ([13], pp. 396–397).3

However, it is not absolutely clear how to define harmony. Various competing understandings are to be found in the literature. We identify a particular path that has not yet been explored, and we call this path 'intensional' or 'strong' harmony. The need to consider such a notion on the background of the discussion, initiated by Prawitz [45], on the identity of proofs, in particular in the context of Kosta Došen's work (see Došen [6, 8, 9], Došen and Petric´ [12]), was raised by Luca Tranchini.4 As the background to this issue we first present two conceptions of harmony, which are not reliant on the notion of identity of proofs.

Harmony Based on Generalised Rules

According to Gentzen “the introductions represent so-to-speak the 'definitions' of the corresponding signs” whereas the eliminations are “consequences” thereof, which should be demonstrated to be “unique functions of the introduction inferences on the basis of certain requirements” (Gentzen [25], p. 189). If we take this as our characterisation of harmony, we must specify a function F which generates elimination rules from given introduction rules. If elimination rules are generated according to this function, then introduction and elimination rules are in harmony with each other.

There have been various proposals to formulate elimination rules in a uniform way with respect to given introduction rules, in particular those by von Kutschera [36], Prawitz [47] and Schroeder-Heister [53]. At least implicitly, they all intend to capture the notion of harmony. Read [51, 52] has proposed to speak of 'general-elimination harmony'. Formulated as a principle, we could say: Given a set cI of introduction rules for a logical constant c, the set of elimination rules harmonious with cI is the set of rules generated by F , namely F (cI ). In other words, cI and F (cI ) are by definition in harmony with each other. If alternative elimination rules cE are given for c, one would say that cE is in harmony with cI , if cE is equivalent to F (cI ) in the presence of cI . This means that, in the system based on cI and cE , we can derive the rules contained in F (cI ), and in the system based on cI and F (cI ), we can derive the rules contained in cE .

Consequently the generalised elimination rules F (cI ) are canonical harmonious elimination rules5 given introduction rules cI . The approaches mentioned above develop arguments that justify this distinguishing characteristic, for example by referring to an inversion principle. The canonical elimination rule ensures that everything that can be obtained from the premisses of each introduction rule can be obtained from their conclusion. For example, if the introduction rules for ϕ have the form

I) .6.1

ϕ .6.m


the canonical elimination rule takes the form

[.6.1] [.6.m ]

ϕ r ... r

E)can r

The exact specification of what the .6.i can mean, and what it means to use the .6.i as dischargeable assumptions, depends on the framework used (see Schroeder-Heister [63, 65]).6

While the standard approaches use introduction rules as their starting point, it is possible in principle, and in fact not difficult, to develop a corresponding approach based on elimination rules. Given a set of elimination rules cE of a connective c, we would define a function G that associates with cE a set of introduction rules G (cE ) as the set of introduction rules harmonious to cI . While the rules in G (cE ) are the canonical harmonious introduction rules, any other set cI of introduction rules for c would be in harmony with cE if cI is equivalent to G (cE ) in the presence of cE . This means that, in the system based on cE and cI , we can derive the rules contained in G (cE ), and in the system based on cE and G (cE ), we can derive the rules in cI . For example, if the elimination rules have the form

E) ϕ .6.

q1 ... ϕ .6.m


then the canonical introduction rule takes the form

[.6.1] [.6.m ]

I) q 1 ... q m can ϕ

Here the conclusions of the elimination rules become premisses of the canonical introduction rules. Again, the exact specification of .6.i depends on the framework

used. For example, if, for the four-place connective ∧ →, the set ∧→ E consists of

the three elimination rules

(∧→ E) ∧→ ( p1 , p2 , p3 , p4 ) ( p 1 , p 2 , p 3 , p 4 )


∧→ ( p1 , p2 , p3 , p4 ) p3


6In this section, we do not distinguish between schematic letters for formulas and propositional variables, as we are also considering propositional quantification. Therefore, in a rule schema such as E)can, the propositional variable r is used as a schematic letter.

we would define G (∧→ E ) as consisting of the single introduction rule

[ p3]

(∧→ I) can p1 p2 p4

∧→ ( p1, p2, p3, p4)

In Schroeder-Heister [63] functions F and G are defined in detail.

Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics