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.
Recommendations
Nuprl as logical framework for automating proofs in category theory
Logic and Program SemanticsWe describe the construction of a semi-automated proof system for elementary category theory using the Nuprl proof development system as logical framework. We have used Nuprl's display mechanism to implement the basic vocabulary and Nuprl's rule ...
Logical foundations of well-founded semantics
KR'06: Proceedings of the Tenth International Conference on Principles of Knowledge Representation and ReasoningWe propose a solution to a long-standing problem in the foundations of well-founded semantics (WFS) for logic programs. The problem addressed is this: which (non-modal) logic can be considered adequate for well-founded semantics in the sense that its ...