This I find intriguing:
Can we actually use [homotopy] type theory as the foundation for mathematics? That is, must we consider the objects of mathematics to “really” be built out of sets, with “types” just a convenient fiction for talking about such structures? Or can we consider types to be the basic objects of mathematics, with everything else built out of them?
The answer is undoubtedly yes: the “sets” in type theory can encode mathematics just like the sets of ZFC can.
The real question, therefore, is not “can we?” but “should we?” This is where things get more philosophical. Over the past century, mathematicians and philosophers have become accustomed to the fundamental objects of mathematics being discrete sets, with no spatial or homotopical structure. However, a priori there is no reason this has to be the case.One of the central insights of category theory and homotopy theory is that no class of mathematical objects should be considered without the corresponding notion of isomorphism or equivalence: we study groups up to isomorphism, spaces up to homeomorphism, categories up to equivalence, and so on. Thus, all mathematical collections naturally form groupoids when equipped with the relevant “notion of sameness”. The theory of all groups is much less tractable, and much less interesting, than the category of all groups; so even though the former is “simpler” in the sense of containing no nontrivial automorphisms, it is reasonable to regard the latter as being at least as fundamental.
One possible objection to treating spaces as fundamental is to ask how we should decide which rules our “spaces as fundamental” should satisfy. [Different mathematical fields] will have their own toposes and their own type theories.
[But] why must we insist on singling out some particular theory as “the” foundation of mathematics? The idea of a “foundation for mathematics” stems from the great discovery of 20th century logic that we can encode mathematics into various formal systems and study those systems mathematically. But in the 21st century, we are sufficiently familiar with this process that we no longer need to tie ourselves to only one such system. In ZFC orthodoxy there is an absolute notion of “set” out of which everything is constructed. Spaces exist, but they are second-class citizens, ultimately reducible to sets, and the basic axioms of set theory don’t apply to them. But from a pluralistic viewpoint, mathematics can be developed relative to any topos, obeying the same general rules of type theory. We have consistent rules for translating between toposes along functors, and there are some toposes in which mathematics looks a bit simpler. However, there is no justification for regarding any particular topos or type theory as the “one absolute universe of mathematics”. Just as modern physicists switch reference frames as needed, modern mathematicians should be free to switch foundational systems as appropriate. Set theory and 20th century logic were a crucial stepping-stone to bring us to a point where we can survey the multitude of universes of mathematics; but once there, we see that there is nothing special about the route we took.
Those sentences are taken from the conclusion of a recent arXiv paper by Michael Shulman on ‘Homotopy type theory: the logic of space‘, a long chapter written for a forthcoming book (I’ve not marked all the lacunae in this quotation which I’ve brutally cut by more than half). Unfortunately, despite Shulman’s expository gifts in some of his other exoteric papers, what comes before I find pretty impenetrable: but I’m sure that the problem is with me lacking enough background, not with Shulman’s ideas. So I’m still promising myself to try to get my head around what, in this vein, is happening in homotopy type theory, at least well enough to see what there this in the more philosophical claims made for it.
But that’s for after I get IFL2 sorted …
It’s ideology, resentment (of set theory’s foundational status), and a crypro-religious privileging of a category-theoretic / type-theoretic point of view, hence talk of “ZFC orthodoxy”, as if it’s set theory that’s dogmatic.
Well, that’s view! :) Which is why I’d like to understand better what’s really going on …
Perhaps I should have said it’s political, rather than religious, but talk of “ZFC orthodoxy” suggested the latter.
Anyway, it’s reasonable to say that we don’t have to pick one particular theory as “the” foundation, but the supposedly “pluralistic viewpoint” is to see everything in terms of toposes and type theory. The aim isn’t to open up foundations to more different ways of doing things; it’s to replace set theory + FOL with something they prefer. Saying “modern mathematicians should be free to switch foundational systems as appropriate” turns out not to have ordinary set-theoretic foundations as one of those systems: instead, the freedom is just to pick different a different topos or type system.
One consequence of switching to toposes and type theory is that FOM becomes much harder to understand. Even syntax and semantics become harder to understand (section 2.1 in the paper). From some points of view, perhaps that’s an advantage. It’s a bit like doing church services in Latin so that only priests can understand them.
“Saying “modern mathematicians should be free to switch foundational systems as appropriate” turns out not to have ordinary set-theoretic foundations as one of those systems: instead, the freedom is just to pick different a different topos or type system.”
I don’t think this is fair at all. In this very paper, Shulman writes:
“in the 21st century, we are sufficiently familiar with this process that we no longer need to tie ourselves to only one such system.42 Even ZFC has a role from this point of view: it is a synthetic theory of well-founded membership structures!”
I would agree that the paper sometimes uses ‘foundational systems’ in a way that includes ZFC as one of those systems.
However, I don’t think that’s what the paper’s talking about when it says ‘modern mathematicians should be free to switch foundational systems as appropriate’. There, it does not seem to be talking about switching between ZFC and type theory; instead the idea seems to be that ‘from a pluralistic viewpoint, mathematics can be developed relative to any topos, obeying the same general rules of type theory.’ That’s what the ‘pluralistic viewpoint’ and the analogy with reference frames in Einsteinian physics seems to be about.
In the same paragraph, the pluralistic viewpoint is contrasted with ‘ZFC orthodoxy’. Indeed, almost every mention of ZFC in the paper is contrasting ZFC and the paper’s preferred approach; and one finds such things as this: ‘unlike ZFC, type theory is not a fixed system of axioms or rules, but a “modular” framework for such systems.’ As with the ‘pluralistic viewpoint’, the ‘modular framework’ is type theory, not something that includes type-theoretic foundations as one possibility and ‘orthodox’ ZFC foundations as another.
Of course, the topos / type theory approach can still accommodate a suitably expressed version of ZFC, just as the topos / type theory approach can be modeled in ZFC (or in ZFC plus a suitably large cardinal). That’s how I understand the passage about ZFC having a role.