Set theory with types
It is known that mathematics is heavily reliant on set theory, but no one can agree on what set theory is. Many people today understand that we have a choice between set theory and type theory, but they don’t know what type theory is either. Many think that type theory refers to some sort of dependent type theory, as found in Lean or Agda, while everything else is set theory. But prior to 1980 or so, “type theory” generally referred to higher-order logic and related systems. In 1973, NG de Bruijn wrote a paper called “Set Theory with Type Restrictions”. His discussion of set theory with types was intended as motivation for the AUTOMATH language, a dependent type theory. His thoughts are fascinating and pertinent today.
Set theory according to de Bruijn
De Bruijn begins “it has been believed throughout this century that set theory is the basis of all mathematics.” He specifies this as “Cantor set theory”, or Zermelo–Fraenkel (ZF). And indeed a lot of people continue to insist on this ZF foundation. Paradoxically, mathematicians (who are the ones with skin in the game) are generally the least interested in the technicalities of set theory: actual set theorists are scarce, and the questions they study seldom have a direct impact on other branches of mathematics. De Bruijn continues:
It seems, however that there is a revolt. Some people have begun to dislike the doctrine “everything is a set”, just at the moment that educational modernizers have pushed set theory even into kindergarten. It is not unthinkable that this educational innovation is one of the things that make others try to get rid of set theory’s grip for absolute power.
I was one of those who was taught a tiny bit of set theory in school, when I was something like eight years old. I don’t think it went beyond unions and intersections of two sets. They didn’t even cover Aronszajn trees. I don’t know who was behind this educational trend, but intersections and unions are useful concepts even in everyday life. Roger Needham liked to describe unrealistic expectations as “an elaborate description of the empty set”; people need to be able to understand such remarks.
De Briujn’s chief objection to ZF set theory comes from “the weird idea that everything is set”:
In our mathematical culture we have learned to keep things apart. If we have a rational number and a set of points in the Euclidean plane, we cannot even imagine what it means to form the intersection. The idea that both might have been coded in ZF with a coding so crazy that the intersection is not empty seems to be ridiculous.
He also mentions the possibility of writing $x\in x$, which seems nonsensical and gave us Russell’s paradox. Also objectionable to many are the numerous coding tricks employed, where the ordered pair $(x,y)$ becomes $\{\{x\},\{x,y\}\}$ and the natural number $n$ becomes $\{0, \ldots, n-1\}$. He continues:
The natural, intuitive way to think of a set, is to collect things that belong to a class or type given beforehand. In this way one can try to get theories that stay quite close to their interpretations, that exclude $x\in x$ and are yet rich enough for everyday mathematics.
... continue reading