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.