A logic for category theory (Q685421)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A logic for category theory |
scientific article |
Statements
A logic for category theory (English)
0 references
7 July 1994
0 references
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.
0 references
Gentzen style deduction
0 references
foundations of category theory
0 references
reductionism
0 references
self-reference
0 references