University of Helsinki
Set theory keeps me up at night. Not in a good way. Don’t you also feel weird about how a thing can be a member of something else, at the same time as a part of everything else, at the same time is absolutely nothing? Thaaat’s right I’m talking about the empty set dingdingdingdingdingdingding!
Vague notions always come first. Mathematics has always worked in this way. In the ancient Greek times, philosophers thought that all numbers were rational, until they were proven wrong. Newton had to argue for an “infinitely close to 0” quantity. Most mathematicians would use the concept of sets in their work, but it wasn’t until the beginning of the 20th century, rigorous understanding of set theory developed. It was a classic, a masterpiece, a beam of light shining into the crisis of inconsistency haunting the mansion of mathematics. But what’s the price of it? Now every freshman must learn about how {{a}, {a, b}} actually behaves like an ordered pair, and if you get enough of them together you can even make things that looks like functions!
But seriously, this needs to stop. Axiomatic set theory is very “Hilbertian” in that, the axioms are pretty and simple, but the constructions using them are hell. And the derivations do not always describe a construction. When you get a set as the setting (huh) of a problem, it’s never entirely clear what you’re supposed to do with it. When you read a proof, there is nothing obvious about what fits into where, or how the shapes morph into each other. To me, it’s like when you asked someone to hand you a screwdriver, but they handed you a popsicle stick, and said “Now imagine this popsicle stick is stuck in another popsicle stick, both sides, at a 45-degree angle.” Maybe I’m biased, but I think a screwdriver should have a handle.
You might ask, what then? What are we going to use? Why the heck did we only have the set theory as our foundation to college mathematics then?
Here comes the good news: we actually had other systems! One of them was called type theory, which was first conceived when Whitehead and Russell were working on the Principia Mathematica, a grandiose project to write down literally all of mathematics at the time. That project was toast when Gödel came along, with the cold hard truth that math cannot prove itself right, not back then, not now, and never after. Sent the project 6 feet under. Along with it goes down the early type theory.
But the gist of it remained: a language that actually makes sense, where a natural number is just a natural number, not also a subset of a non-natural non-number. The cinder later reignited when the theory of computation was born, when a new generation of logicians like Turing and Church rules. Lambda calculus was born, along with all the variants of it, like simply-typed lambda calculus, later system F. They brought back the concept of one mathematical object having only one type. The neatness and expressiveness remain to this day, and you are still using a descendant of them whenever you code in Java or C++. That’s also one of the reasons of why type theory is so great. Since all kids are learning coding today, there is a lot of familiarity with one form of it.
Even better: type theory already has been used in math, with flying colors. The computer theorem prover Coq, famously used in the proof for the four-color theorem, is based on type theory systems. Agda, another theorem prover, is already used in domains of higher topology theories, with the brand new homotopy type theory as its foundation.
The crux of type theory is this: in the set theory, you build theorems using the rules from first-order (classical) logic, the rules applications form a tree, and only the leaves are the set theory axioms. In type theory – get this – the types themselves are also the logic! This is called proposition as types. A type could be understood as a proposition, or rather, a proposition is just defined as a type! Logical truth is denoted by the existence of an element in a type. Such types with at least one element are called “inhabited”, reflecting the concept of a true proposition. We also get a huge chunk of proof theory for free, since these elements of a type correspond to the proof of that proposition, so for example we could get cut-elimination from the computation on those elements.
Type theory solves this huge pain of set theory, as it is structural: just like how it is its own logic, the fundamental rules always show you clearly what you need to do at a given point, so you never need to guess. If you need to construct a pair, the rule says you need to give the two elements. If you have a natural number, the rule says you can do mathematical induction on it.
I truly believe the future of mathematics, at least a huge part of it, will be built on a new foundation like type theory. It sure is that much more intuitive for me, and I believe, one day, all of you could also be saved from the horrors of set theoretic constructions.
Hex
References:
- Wadler, P. (2015). Propositions as types. Communications of the ACM, 58(12), 75–84. https://doi.org/10.1145/2699407