Even though the notion of harmony based on the equivalence of cI and cE in IPC2 or in the calculus of quantified higher-level rules is highly plausible, a stronger notion can be considered.7 Let us illustrate this by an example: Suppose we have the set

∧I consisting of the standard conjunction introduction

p1 p2 p1 ∧ p2

and two alternative sets of elimination rules: ∧E consisting of the standard projection

rules p1 ∧ p2

p1

and ∧E consisting of the alternative rules

p1 ∧ p2

p1 p 1 ∧p 2

p2

p1 ∧ p2 p1p2

It is obvious that ∧E and ∧E are equivalent to each other, and also equivalent to the

rule

[ p1, p2]

p1 ∧ p2 q

q

which is the canonical generalised elimination rule for ∧. However, do ∧E and

∧E mean the same in every possible sense? According to ∧E , conjunction just expresses pairing, that is, a proof of p1 ∧ p2 is a pair (TI1, TI2) of proofs, one for

p1 and one for p2. According to ∧E , conjunction expresses something different. A proof of p1 ∧ p2 is now a pair that consists of a proof of p1, and a proof of p2 which is conditional on p1. Using a functional interpretation of conditional proofs, this second component can be read as a procedure f that transforms a proof of p1 into a proof of p2 so that, according to ∧E , conjunction expresses the pair (TI1, f ). Now (TI1, TI2) and (TI1, f ) are different. From (TI1, f ) we can certainly construct

the pair (TI1, f (TI1)), which is of the desired kind. From the pair (TI1, TI2) we can certainly construct a pair (TI1, f ), where f is the constant function that maps any proof of p1 to TI2. However, if we combine these two constructions, we do not obtain what we started with, since we started with an arbitrary function and we end up with a constant function. This is an intuition that is made precise by the consideration that p1 ∧ p2, where conjunction here has the standard rules ∧I and ∧E , is equivalent to p1 ∧ ( p1 → p2), but is not isomorphic to it (see Došen [6, 9]). Correspondingly, only ∧E , but not ∧E is in harmony with ∧I .

Unlike the notion of equivalence, which only requires a notion of proof in a system, the notion of isomorphism requires a notion of identity of proofs. This is normally achieved by a notion of reduction between proofs, such that proofs that are linked by a chain of reductions are considered identical.8 In intuitionistic natural deduction these are the reductions reducing maximum formulas (in the case of implication this corresponds to β-reduction), as well as the contractions of an elimination immediately followed by an introduction (in the case of implication this corresponds to η-reduction) and the permutative reductions in the case of disjunction

and existential quantification. Using these reductions, moving from p1 ∧ p2 to p1 ∧ ( p1 → p2) and back to p1 ∧ p2 reduces to the identity proof p1 ∧ p2 (i.e., theformula p1 ∧ p2 conceived as a proof from itself), whereas conversely, moving from p1 ∧ ( p1 → p2) to p1 ∧ p2 and back to p1 ∧ ( p1 → p2) does not reduce to the identity proof p1 ∧ ( p1 → p2). In this sense ∧E and ∧E cannot be identified.

More precisely, given a formal system together with a notion of identity of proofs, two formulas ψ1 and ψ2 are called isomorphic if there are proofs of ψ2 from ψ1 and of ψ1 from ψ2, such that each of the combination of these proofs (yielding a proof of ψ1 from ψ1 and ψ2 from ψ2) reduces to the trivial identity proof ψ1 or ψ2, respectively. As this notion, which is best made fully precise in categorial terminology, requires not only a notion of proof but also a notion of identity between proofs, it is an intensional notion, distinguishing between possibly different ways of proving something. The introduction of this notion into the debate on harmony calls for a more finegrained analysis. We may now distinguish between purely extensional harmony, which is just based on equivalence and which may be explicated in the ways described in the previous two subsections, and intensional harmony, which requires additional means on the proof-theoretic side based on the way harmonious proof conditions can be transformed into each other.

However, even though the notion of an isomorphism has a clear meaning in a formal system given a notion of identity of proofs, it is not so clear how to use it to define a notion of intensional harmony. The notion of intensional harmony will also be called strong harmony in contradistinction to extensional harmony which is also called weak harmony.

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