Closed categories and the theory of proofs
作者： G. E. Mints
DOI: 10.1007/BF01404107
关键词: Enriched category 、 Discrete category 、 Morphism 、 Mathematics 、 Coherence theorem 、 Symmetric monoidal category 、 Algebra 、 Category theory 、 Closed monoidal category 、 Cartesian closed category 、 Statistics and Probability 、 Applied mathematics 、 General Mathematics
摘要: The main aim of this article is to suggest a translation the simplest concepts category theory into language (structural) proofs, use simplify proofs some known results [1], and obtain two new ones: coherence theorem for canonical morphisms in (nonmonoidal, nonsymmetric) closed categories [2], solution problem equality morphisms. Extensions these monoidal closed, symmetric are sketched. decision procedure obtained by means correct faithful an expansion λ-language, which has tools special account “superfluous” premises implications (the thinning rule). expansions λ-language have so far appeared literature not possessed facility.
springer.com
sci-hub.se 参考文章(16)
G. Kreisel, A Survey of Proof Theory II Proceedings of the Second Scandinavian Logic Symposium. ,vol. 63, pp. 109- 170 ,(1971) , 10.1016/S0049-237X(08)70845-0
Joachim Lambek, Deductive systems and categories II. Standard constructions and closed categories Lecture Notes in Mathematics. pp. 76- 122 ,(1969) , 10.1007/BFB0079385
Joachim Lambek, Deductive systems and categories III. Cartesian closed categories, intuitionist propositional calculus, and combinatory logic Springer, Berlin, Heidelberg. pp. 57- 82 ,(1972) , 10.1007/BFB0073965
G. M. Kelly, An abstract approach to coherence Coherence in Categories. pp. 106- 147 ,(1972) , 10.1007/BFB0059557
Dag Prawitz, Natural Deduction: A Proof-Theoretical Study ,(1965)
Dag Prawitz, Ideas and Results in Proof Theory Proceedings of the Second Scandinavian Logic Symposium. ,vol. 63, pp. 235- 307 ,(1971) , 10.1016/S0049-237X(08)70849-8
Metamathematical investigation of intuitionistic arithmetic and analysis UT Back-in-Print Service. ,(1973) , 10.1007/BFB0066739
J. Zucker, The correspondence between cut-elimination and normalization II Annals of Mathematical Logic. ,vol. 7, pp. 113- 155 ,(1974) , 10.1016/0003-4843(74)90010-2
G. Kreisel, A survey of proof theory Journal of Symbolic Logic. ,vol. 33, pp. 321- 388 ,(1968) , 10.2307/2270324
G.M. Kelly, S. Maclane, Coherence in closed categories Journal of Pure and Applied Algebra. ,vol. 1, pp. 97- 140 ,(1971) , 10.1016/0022-4049(71)90013-2