Closed categories and the theory of proofs

G. E. Mints

Zapiski Nauchnykh Seminarov POMI, Theoretical application of methods of mathematical logic. Part II, Tome 68 (1977), pp. 83-114

Résumé

The main aim of this article is to suggest a translation of the simplest concepts of category theory into the language of (structural) theory of proofs, to use this translation to simplify the proofs of some known results [1], and to obtain two new ones: the coherence theorem for canonical morphisms in (nonmonoidal, nonsymmetric) closed categories [2], and the solution of the problem of equality of canonical morphisms. Extensions of these results to monoidal closed, symmetric closed, and monoidal symmetric closed categories are sketched. The decision procedure is obtained by means of a correct and faithful translation of canonical morphisms into an expansion of the $\lambda$-language, which has the tools for a special account of “superfluous” premises of implications (the thinning rule). The expansions of the $\lambda$-language which have so far appeared in the literature have not possessed this facility.