Set theory with types

Summary

Set theory with types 21 Nov 2025 [ AUTOMATH NG de Bruijn type theory set theory type classes Principia Mathematica Archive of Formal Proofs ] 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 cov...