A foundations of mathematics for the 21st century
It's here! For decades, mathematicians been dreaming of an approach to math where different proofs that x = y can be seen as different paths
in a space
. It's finally been made precise, thanks to Vladimir Voevodsky and a gang of mathematicians who holed up for a year at the Institute for Advanced Studies, at Princeton.
I won't try to explain it, since that's what the book does. I'll just mention a few of the radical new features:
• It includes set theory as a special case, but it's founded on more general things called 'types'. Types include sets, but also propositions. Proving a proposition amounts to constructing an element of a certain type. So, proofs are no longer 'outside' the mathematics being discussed, they're inside it just like everything else.
• The logic is - in general - 'constructive', meaning that to prove something exists amounts to giving a procedure for constructing it. As a result, the system can be and is being
computerized with the help of programs like Coq and AGDA.
• Types can be seen as 'spaces', and their elements as 'points'. A proof that two elements of a type are equal can be seen as constructing a path between two points. Sets are just a special case: the '0-types', which have no interesting higher-dimensional aspect. There are also types that look like spheres and tori! Technically speaking, the branch of topology called homotopy theory
is now a part of logic! That's why the subject is called homotopy type theory
• Types can also be seen as infinity-groupoids
. Very roughly, these are structures with elements, isomorphisms between elements, isomorphisms between isomorphisms, and so on ad infinitum
. So, a certain chunk of the important new branch of math called 'higher category theory' is now part of logic, too.
• The most special contribution of Voevodsky is the univalence axiom
. Very very
roughly, this expands the concept of 'equality' so that it's just as general as the hitherto more flexible concept of 'isomorphism' - or, if you know some more fancy math, 'equivalence'. Mathematicians working on homotopy theory and higher category theory have known for decades that equality is too rigid a concept to be right - for certain applications. The univalence axiom updates our concept of equality so that it's good again! (However, nobody knows if this axiom is constructive - this is a big open question.)
Since this is all about foundations
, and it's all quite new, please don't ask me yet what its practical applications are. Ask me in a hundred years. For now, I can tell you that this is the 'upgrade' that the foundations of math has needed ever since the work of Grothendieck. It's truly 21-century math.
It's also a book for the 21st century, because it's escaped the grip of expensive publishers! While it's 600 pages long, a hardback copy costs less than $27. Paperback costs less than $18, and an electronic copy is free! #spnetwork #homotopytheory #ncategories #logic #foundations