A logic for category theory (Q685421)

The foundations of category theory are considered. Following the example of Tarski's reductionism for first order logic, the authors have built a logical system and a set theory which they call NaDSet (NaD from Natural Deduction). Subtle use of controlled self-reference and other subtle technical means allows them to avoid artificial distinction between large and small categories, and to obtain the main result that the set of all functors forms a category (under appropriate definitions of composition and equivalence) within NaDSet. The authors refer also to the consistency proof for NaDSet. The paper could be useful for future work because it contains explicite formulations within NaDSet of main notions and constructions of category theory. It sounds a little misleading that the authors call their system a Natural Deduction System though usually in proof theory one calls natural deduction systems (following Gentzen) the systems with introduction and elimination rules, and in NaDSet they use left and right introduction rules in style of Gentzen system LK.