A~coherence theorem for canonical morphisms in cartesian closed categories

A. A. Babaev ; S. V. Solov'ev

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VIII, Tome 88 (1979), pp. 3-29

Résumé

A coherence theorem states that any diagram of canonical maps from $A$ to $B$ is commutative, i.e. any two maps from $A$ to $B$ are equal if objects $A,B$ satisfy some natural condition. We employ familiar translation ([2], [6]) of the canonical maps in cartesian closed category into derivations in ($\,\supset$)-fragment of intuitionistic propositional calculus. Two maps are equal iff corresponding derivations are equivalent (i.e. they have the same normal form or their deductive terms are equivalent ([2], [5]). We consider the following form of coherence theorem. If $S$ is a sequent and any propositional variable occurs no more than twice in $S$ then any two derivations of $S$ are equivalent. (It makes no difference to consider cut-free $L$-deductions or normal natural deductions (cf.[9]).) We give two proofs of the coherence theorem. The first proof (due to A. Babajev) uses the natural deduction system and deductive terms. The second proof (due to S. Solovaov) uses a reduction of the formula depth [7] and Kleene's results on permutability of inferences in Gentzen's calculi LK and LJ.