Set Theory with Types

16 hours ago

Copy Link

Mathematics traditionally relies on set theory, but there's no consensus on what set theory exactly is.
Type theory is often seen as an alternative to set theory, but its definition is also unclear to many.
NG de Bruijn's 1973 paper 'Set Theory with Type Restrictions' introduces the idea of set theory with types, motivating AUTOMATH, a dependent type theory.
De Bruijn critiques Zermelo–Fraenkel (ZF) set theory for its foundational claim that 'everything is a set', arguing it leads to nonsensical constructs like x ∈ x.
He advocates for a typed set theory where sets are collections of pre-typed elements, preventing meaningless operations and staying closer to mathematical intuition.
De Bruijn suggests that most mathematics can be done within a system that constructs N, N^N, N^(N^N), etc., without needing the full power of ZF set theory.
Higher-order logic, descended from Principia Mathematica, treats sets as boolean-valued functions, blending set theory and predicate logic.
Typed set theory in Isabelle/HOL excludes x ∈ x by type constraints, offering a natural framework for everyday mathematics without ZF's complexities.
The ZFC_in_HOL project integrates ZF set theory into higher-order logic, connecting two mathematical worlds through type classes.
Hereditarily finite sets (hf) provide a simpler, finite alternative to ZF set theory, useful for modeling programming languages and finite state machines.

Hasty Briefsbeta