# The ICICS/CS Reading Room

## UBC CS TR-90-02 Summary

- No on-line copy of this technical report is available.

- Logical Foundations for Category Theory, May 1990 Paul C. Gilmore and George K. Tsiknis
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.
\nIn 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.
\nNaDSet 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.
\nFormalizations 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.

If you have any questions or comments regarding this page please send mail to
help@cs.ubc.ca.