Michael Makkai: FOLDS equivalences as the basis of a general theory of identity for concepts in higher dimensional categories

Abstract:

1.The theory of abstract sets is based on a formal language that is given within FOLDS, first-order logic with dependent sorts. Abstract set theory was introduced in an informal manner by F. W. Lawvere in Section 2 of his 1976 paper “Variable quantities and variable structures in topoi”. Lawvere used his informal, but very informative description of abstract set theory for the purposes of topos theory. In 2003, and then in a more detailed manner in 2013, I introduced the formalization I will talk about here. It is more directly set-theoretical than topos theory, which is based on the language of categories. The structuralist imperative, stated by Bourbaki as an explicit requirement on any concept of structure, a special case of which is that “an abstract set has no external properties save its cardinality” (Lawvere), appears, necessarily in the absence of a formal language, as a desideratum in Lawvere's exposition. The main result of my work is that in the new formalization, the structuralist imperative becomes a provable general fact, in the form that any concept formulated in the dependent-typed language of abstract sets is invariant under isomorphism.

I will use the opportunity of abstract sets to introduce, albeit only in an informal way, the general syntax of FOLDS.

2. I introduced FOLDS in 1995 in the monograph “First Order Logic with Dependent Sorts with Applications to Category Theory” (available on my web-site both in its originally typed and also in a TEXed version). In the paper “Towards a Categorical Foundation of Mathematics”, published in 1998, but written at the same time as the monograph in 1995, I gave a descriptive outline of the theory. The syntax is explained both symbolic-logically, and by using tools of categorical logic. The main reason why I came out with FOLDS is that I found that there is a notion generalizing isomorphism – called FOLDS equivalence -- for structures for a FOLDS language such that:1) many (all?) notions of equivalence used in higher- dimensional categories coincide with appropriate instances of the FOLDS equivalence, and 2) first-order properties of structures in general are invariant under FOLDS equivalence if and only if they are equivalently formulatable in the FOLDS syntax. My main application of FOLDS is a statement of the universe of the so-called multitopic categories; see The Multitopic Category of All Multitopic Categories on my web-site, in both the 1999 and the corrected 2004 versions. In the talk, I will necessarily be rather informal about the subject, with suggestive examples rather than precise general definitions.