Logical Foundations for Category Theory

ID
TR-90-02
Authors
Paul C. Gilmore and George K. Tsiknis
Publishing date
May 1990
Abstract
Category theory provides an abstract and uniform treatment for many mathematical structures, and increasingly has found applications in computer science. Nevertheless, no suitable logic within which the theory can be developed has been provided. The classical set theories of Zermelo-Fraenkel and Godel-Bernays, for example, are not suitable because of the use category theory makes of self-referencing abstractions, such as in the theorem that the set of categories forms a category. That a logic for the theory must be developed, Feferman has argued, follows from the use in the theory of concepts fundamental to logic, namely, propositional logic, quantification and the abstractions of set theory. In this paper a demonstration that the logic and set theory NaDSet is suitable for category theory is provided. Specifically, a proof of the cited theorem of category theory is provided within NaDSet. NaDSet succeeds as a logic for category theory because the resolution of the paradoxes provided for it is based on a reductionist semantics similar to the classical semantics of Tarski for first and second order logic. Self-membership and self-reference is not explicitly excluded. The reductionist semantics is most simply presented as a natural deduction logic. In this paper a sketch of the elementary and logical syntax or proof theory of the logic is described. Formalizations for most of the fundamental concepts and constructs in category theory are presented. NaDSet definitions for natural transformations and functor categories are given and an equivalence relation on categories is defined. Additional definitions and discussions on products, comma categories, universals limits and adjoints are presented. They provide enough evidence to support the claim that any construct, not only in categories, but also in toposes, sheaves, triples and similar theories can be formalized within NaDSet.