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
    0 references
    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
    0 references
    Gentzen style deduction
    0 references
    foundations of category theory
    0 references
    reductionism
    0 references
    self-reference
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references