Abstract
Applying methods of the proof theory, it is shown that two canonical morphisms are equal in all Cartesian closed categories if and only if some of their realizations in the category of finite sets are equal. All realizations of formal combinations of objects using the functors x and hom are isomorphic in all Cartesian closed categories if and only if some of their realizations in the category of finite sets are isomorphic. On the base of these results, a purely syntactic decision algorithm for (extensional) isomorphism of formal combinations of objects and a new decision algorithm for equality of canonical morphisms are obtained.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Literature cited
J. Lambek, “Deductive systems and categories. I,” Math. Syst. Theory, No. 2, 287–318 (1968).
J. Lambek, “Deductive systems and categories. II,” in: Lecture Notes Math., Vol. 86 (1969), pp. 76–122.
J. Lambek, “Deductive systems and categories. III,” in: Lecture Notes Math., Vol. 274 (1972), pp. 57–82.
J. Lambek, “Fromλ-calculus to Cartesian closed categories,” Preprint, McGill University, Montreal (1979).
C. Mann, “The connection between equivalence of proofs and Cartesian closed categories,” Proc. London Math. Soc.,31, No. 3, 289–310 (1975).
G. E. Mints, “Category theory and proof theorey. I,” in: Actual Questions of Logic and Science Methodology [in Russian], Kiev (1980), pp. 252–278.
G. E. Mints, “Closed categories and proof theory,” Zap. Nauchn. Sem. Leningr. Otd. Inst. Akad. Nauk SSSR,68, 197–208 (1977).
M. Szabo, “A categorical equivalence of proofs,” Notre Dame J. Form. Log.,15, No. 2, 171–191 (1974).
Yu. L. Ershov, Theory of Numerations [in Russian], Moscow (1977).
D. Prawitz, Natural Deduction. A Proof Theoretical Study, Stockholm (1965).
S. MacLane, “Topology and logic as a source of algebra,” Bull. Am. Math. Soc.,82, No. 1, 1–40 (1976).
Additional information
Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 105, pp. 174–194, 1981.
Rights and permissions
About this article
Cite this article
Solov'ev, S.V. The category of finite sets and Cartesian closed categories. J Math Sci 22, 1387–1400 (1983). https://doi.org/10.1007/BF01084396
Received:
Revised:
Issue date:
DOI: https://doi.org/10.1007/BF01084396