×

Towards a categorical foundation of mathematics. (English) Zbl 0896.03051

Makowsky, Johann A. (ed.) et al., Logic colloquium ’95. Proceedings of the Annual European Summer Meeting of the Association of Symbolic Logic, Haifa, Israel, August 9–18, 1995. Berlin: Springer. Lect. Notes Log. 11, 153-190 (1998).
This article is an extended introduction, reasonably non-technical and partly philosophical in character, to the author’s attempts to construct a ‘Structuralist Foundation of Abstract Mathematics’ (SFAM), as exemplified by his recent works ‘Avoiding the axiom of choice in general category theory’ [J. Pure Appl. Algebra 108, 109-173 (1996; Zbl 0859.18001)], ‘Generalized sketches as a framework for completeness theorems’ [J. Pure Appl. Algebra 115, 49-79, 179-212 and 241-274 (1997; Zbl 0871.03045)] and his forthcoming monograph ‘First-order logic with dependent sorts, with applications to category theory’ (to appear in Springer Lecture Notes in Logic). It should be emphasized that SFAM does not yet exist as a precisely formulated theory; what the author is trying to do is to give some idea of the flavour it will have, and in particular of the ways in which it will differ from classical set-theoretic foundations. The primary respect in which SFAM differs from classical set theory is in its rejection of the idea of equality and membership as ‘global’ predicates: it accepts as meaningful the question whether two elements of a given abstract set are equal to each other, but not the question whether two abstract sets are equal. For abstract sets, as objects of the catgeory of abstract sets, the only meaningful question we can ask is whether they are isomorphic – and this is not a primitive relation, but one derived from the structure of the category in which they live. However, categories themselves cannot be the objects of a category, because we cannot have a meaningful notion of isomorphism between them (without imposing a meaningful notion of equality between their objects): indeed, the principles of SFAM require us to reject the traditional notion of functor between categories, in favour of the notion of ‘anafunctor’ introduced in the first of the author’s papers cited above; this leads to the result that categories form (not a \(2\)-category but) a bicategory, or even better a ‘saturated anabicategory’. This leads on to an infinite hierarchy of ‘weak \(n\)-dimensional categories’: it is at this point, roughly half way through the present paper, that the reviewer suspects the majority of readers (in particular, those who are not au fait with the recent developments in higher-dimensional category theory) will be strongly tempted to give up. They would, however, be well advised to persevere: for the second half of the paper (from section 8 onwards) consists of an elegant and easily readable account of the basic syntax of FOLDS (‘First-Order Logic with Dependent Sorts’), which the author proposes as the language in which SFAM is to be formulated. Obviously, this account is not entirely self-contained: for many details it refers forward to the author’s monograph cited above, as well as backward to the work on sketches out of which the idea of FOLDS was born. But it should certainly be enough to infuse those readers who manage to get this far with the desire to read more about FOLDS when the fuller treatment becomes available.
For the entire collection see [Zbl 0884.00035].

MSC:

03G30 Categorical logic, topoi
18A15 Foundations, relations to logic and deductive systems
03B15 Higher-order logic; type theory (MSC2010)
03A05 Philosophical and critical aspects of logic and foundations
18D05 Double categories, \(2\)-categories, bicategories and generalizations (MSC2010)
PDFBibTeX XMLCite