29 October 2013
2:30 - 4:00   M. Makkai (McGill)
The theory of abstract sets formalized in first-order logic with dependent types

Abstract: On my website (http://www.math.mcgill.ca/makkai/), the last item in the list "Papers" you find a recent paper of mine with the same title, referred to as "the paper" below. Although it has not been published (or even submitted for publication), it is a complete paper in all reasonable aspects. My talk will consist of mathematical excerpts of the, on the whole rather philosophical, paper. I will discuss a passage from F. W Lawvere's famous 1976 paper "Variable quantities and variable structures in topoi". A crucial sentence of said passage amounts to a call to produce a formal language for abstract sets in which all statements on a single variable (abstract) set are invariant under equipollence of sets. I produce such a language (a particular case of FOLDS: First Order Logic with Dependent Sorts), and state and prove "Lawvere's imperative", the required invariance property for the language, as well as a natural generalization of it that I call "Benaceraff's imperative". The paper also attempts to demonstrate the expressive power of the language in a way that seem to be new. The paper has a detailed historical discussion from which it will be seen that many ingredients of the paper are not new, having precursors in works of other authors as well as in my own work. However, I view the mathematical formulations and proofs of the "imperatives" to be new to the paper.