Michael Makkai: Abstract set theory and the syntax of FOLDS

Professor em. Michael Makkai (McGill, Montreal) is visiting the Department of Mathematics, Stockholm University 30 November- 11 December, and is connection with this giving two lectures on first-order logic with dependent sorts (FOLDS) in the logic seminar. He will also give an invited talk at the Categorical Logic Workshop, held December 3-4 at the department.

Abstract:

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.