Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

Towards a Definition of Strong Harmony

For simplicity, take the notion of reductive harmony mentioned in Sect. 3.2. Given introduction rules cI and elimination rules cE of an operator c, it associates with c the introduction meaning cI and the elimination meaning cE , and identifies extensional harmony with the equivalence of cI and cE in IPC2. It then appears to be natural to define intensional harmony as the availability of an isomorphism between cI and cE in IPC2. However, this definition turns out to be unsuccessful, as the following observation shows.

What we would like to achieve, in any case, is that the canonical eliminations for given introductions are in strong harmony with the introductions, and similarly that the canonical introductions for given eliminations are in strong harmony with the eliminations. The second case is trivial, as the premisses of the canonical introduction are exactly the conclusions of the eliminations. For example, if for the connective

↔ the elimination rules

(↔ E) p 1 p 2 p 1

can p2 p 1 p 2 p 2

p1

are assumed to be given, then its canonical introduction rule has the form

(↔ I) [ p1]

p2 [ p2]

p1

can p1 ↔ p2

Both the elimination meaning ↔I and the introduction meaning ↔E have the form

( p1 → p2)( p2 → p1), so that the identity proof identifies them. However, in

the first case, where the canonical eliminations are given by the general elimination

rules, the situation is more problematic.

Consider disjunction with the rules

[ p1] [ p2]

p 1 p1 ∨ p2 p 2 p1 ∨ p2 p 1 p 2 q q

q

Here the introduction meaning of p1 ∨ p2 is p1 ∨ p2, viewed as a formula of IPC2, and its elimination meaning is ∀q((( p1 → q)( p2 → q))q). However, though p1 ∨ p2 and ∀q((( p1 → q)( p2 → q))q) are equivalent in IPC2,

they are not isomorphic. There are proofs

p1 ∨ p2

D1

q((( p1 → q)( p2 → q))q)q((( p1 → q)( p2 → q))q)

D2

p1 ∨ p2

of ∀q((( p1 → q)( p2 → q))q) from p1 ∨ p2 and of p1 ∨ p2 from

q((( p1 → q)( p2 → q))q), so that the composition D2 ◦ D1 yields

the identity proof p1 ∨ p2, but there are no such proofs so that D1 ◦ D2 yields the identity proof ∀q((( p1 → q)( p2 → q))q). One might object that, due to the definability of connectives in IPC2, p1 ∨ p2 should be understood as

q((( p1 → q)( p2 → q))q), so that the isomorphism between p1 ∨ p2 and

q((( p1 → q)( p2 → q))q) becomes trivial (and similarly, if conjunction

is also eliminated due to its definability in IPC2). To accommodate this objection, we consider the example of the trivial connective + with the introduction and elimination

rules

p

+ p [ p]

+ p q

q

Here the elimination rule is the canonical one according to the general-elimination schema. In order to demonstrate strong harmony, we would have to establish the

isomorphism of p and ∀q(( pq)q) in IPC2, but this fails. This failure may

be related to the fact that for the second-order translations of propositional formulas,

we do not have η-conversions in IPC2 (see Girard et al. [27], p. 859). This shows that for the definition of strong harmony the definition of introduction and elimination meaning by translation into IPC2 is perhaps not the best device. We consider the lack of an appropriate definition of strong harmony a major open problem, and we provide two tentative solutions (with the emphasis on 'tentative').

First proposal: Complementation by canonical rules. In order to avoid the problems of second-order logic, we can stay in intuitionistic propositional logic as follows. Suppose for a constant c certain introduction rules cI and certain elimination rules cE are proposed, and we ask: When are cI and cE in harmony with each other? Suppose cI is the canonical elimination rule for the introduction rules cI , and cE is the canonical introduction rule for the elimination rules cE . We also call cI the canonical complement of cI , and cE the canonical complement of cE . We define two new connectives c1 and c2. Connective c1 has cI as its introduction rules and its complement cI as its elimination rule. Conversely, connective c2 has cE as its elimination rules and its complement cE as its introduction rules. In other words, for one connective we take the given introduction rules as complemented by the canonical elimination rule, and for the other connective we take the given elimination rules as complemented by the canonical introduction rule. Furthermore, we associate with c1 and c2 reduction procedures in the usual way, based on the pairs cI /cI and cE /cE as primitive rules. Then we say that cI and cE are in strong harmony, if c1 is isomorphic to c2, that is, if there are proofs from c1 to c2 and back, such that the composition of these proofs is identical to the identity proof c1 or c2, depending on which side one starts with.10 In this way, by splitting up c into two connectives, we avoid the explicit translation into IPC2.11

Second proposal: Change to the notion of canonical elimination. As mentioned above, we do not encounter any problem in IPC2, if we translate the introduction meaning of disjunction by its disjunction-free second-order translation, as isomorphism is trivial in this case. In fact, whenever we have more than one introduction rule for some c then the disjunction-free second-order translation is identical to the second-order translation of the elimination meaning for the canonical (indirect) elim-

ination. We have a problem in the case of the connective +, which has the introduction

meaning p and the elimination meaning ∀q(( pq)q). However, for + an

alternative elimination rule is derivable, namely the rule

+ p

p

In fact, this sort of elimination rule is available for all connectives with only a single introduction rule. We call it the 'direct' as opposed to the 'indirect' elimination rule.

For example, the connective &⊃ with the introduction rule

[ p1]

p1 p2

has as its direct elimination rules

p1 & p2

p1 p1 &⊃ p2

p1 & p2 p1 p2

If we require that the canonical elimination rules always be direct where possible, that is, whenever there is not more than one introduction rule, and indirect only if there are multiple introduction rules, then the problem of reduction to IPC2 seems to disappear. In the direct case of a single introduction rule, the elimination meaning is trivially identical to the introduction meaning. In the indirect case, they now become trivially identical again. This is because disjunction, which is used to express the introduction meaning for multiple introduction rules, is translated into disjunctionfree second-order logic in a way that makes its introduction meaning identical to its elimination meaning.

This second proposal would require the revision of basic tenets of proof-theoretic semantics, because ever since the work of von Kutschera [36], Prawitz [47] and Schroeder-Heister [53] on general constants, and since the work on general elimination rules, especially for implication, by Tennant [69, 70], López-Escobar [37] and von Plato [43],12 the idea of the indirect elimination rules as the basic form of elimination rules for all constants has been considered a great achievement. That said, the abandonment of projection-based conjunction and modus-ponens-based implication has received some criticism (Dyckhoff [15], Schroeder-Heister [66], Sect. 15.8). In fact, even the first proposal above might require this priority of the direct elimination

12For a discussion see Schroeder-Heister [65].

rules. If we consider conjunction with ∧I and ∧E given by the standard rules

p1 p2 p1 ∧ p2 p 1 p 2

p1 p 1 p 2

p2

then ∧I is the generalised ∧-elimination rule

[ p1, p2]

p1 p2 q

q

whereas ∧E is identical with ∧I . This means that strong harmony would require that projection-based conjunction and conjunction with general elimination are isomorphic, but no such isomorphism obtains.13

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

Related topics