> If we distill it down from the categorical heights, this brings us back to John Baez’s pithy quote about equality: “Every interesting equation is a lie.” The only obviously true equation is x=x, but it carries no (or little) information. Any other equation, like x=y, is “a lie” because x and y are not the same thing; yet what is interesting about the equality is that they are nevertheless the same in some way. But knowing the equation doesn’t mean that we should forget all about y and use only x; the point of having the equation is that we can pass back and forth between x and y, according to which is most appropriate in any given context.
Because it's obtuse. There are well-known ways of phrasing all of this stuff in set theory (or rather, "legitimate" varieties of set theory) should anyone really care, replicating type-theoretical constructions by adding increasingly large "inaccessible cardinals" to one's pre-existing notion of set. But it's a pointless exercise when the type-theoretical description of these foundations is so much easier to work with. It's only useful if one believes that "set theory" is the only legitimate language for talking about anything foundational, which is again quite silly.
Also, I'm not sure what "all of this stuff" refers to here re: your comment about inaccessible cardinals. You don't need large cardinals to do 99.99% of modern mathematics (essentially, everything but set/proof theory). ZFC is good enough (and you can usually get away with something weaker).
After multiple decades, it's clear you all are never going to bother to learn our stuff nearly as well as we bothered to learn your stuff. This "debate" is thus completely unproductive without any good agreed-upon foundation to argue form.
(How ironic!)
But I do think trumpeting HoTT as a new, improved foundation of mathematics evinces a misunderstanding of what people who work on foundations actually want out of a foundation of mathematics; or even more broadly, the mistaken belief that finding a new foundation of mathematics is an interesting project in the 21st century.
Lurie's comment here explains a bit more: https://mathematicswithoutapologies.wordpress.com/2015/05/13...
(And clearly, Lurie is not some ignorant traditionalist. There's a substantive disagreement that can't be reduced to people not wanting to learn "your stuff.")
I'm desperately trying to find a lovely philosophical writeup on the different purposes to which a "foundation" is put, and why different foundationalists want those foundations for distinct purposes. I can't seem to hunt it down (Google has become steadily less helpful over time). But the thrust is, I don't think anybody is claiming that HoTT ought to replace ZFC for reverse mathematics in particular; it's "just" a capturing of some pervasive intuitions for concepts at the ground floor of the formalism itself. It takes a perspective that makes grappling with some concepts easier to approach. If you're already a deft hand with a different (very well-established) framework, as Lurie exhibits throughout, maybe it's worth it to keep using the entirely viable tools you have!
My claim is that "capturing [...] some pervasive intuitions" is not what ZFC is trying to do, or what people in foundations are interested in. Lurie puts the point well when he says a foundation "mean[s] a small number of concepts and assumptions from which the rest of mathematics can be derived." The purposes here are first, to figure out what exactly one must assume to get the rest of mainstream mathematics, and second, to provide a convenient base for doing metamathematics (since the fewer elementary operations/objects you have to reason with, the easier it is to write proofs). Capturing intuitions is completely orthogonal to this endeavor; no one is claiming that set-theoretic translations of everyday mathematical arguments capture the intuitive content of those arguments, because no one one intended ZFC to ever do that in the first place.
Similarly, no one is claiming that handing someone a Turing machine that performs quicksort is a great way to capture the intuition behind quicksort, or explain the algorithm in an understandable way. Turing machines exist as a special-purpose construct to probe the limits of computation, not to reproduce or communicate high-level algoritmhic reasoning. ZFC is like a Turing machine for (meta)math.
http://www.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20want...
I need to reread it myself, but this is the article I was referencing.
HoTT/UF share some purposes of a foundation with ZFC, and not others. Each has purposes the other does not. That's about the safest thing I can say with any faith that I'm doing it justice.
I want to emphasize I'm not policing semantics just for the sake of being ornery. My reaction is approximately the same as it would be to someone who sends me a graph theory paper and calls it number theory. These distinctions are useful.
This is still gatekeeping who gets to use the word "foundations".
I will go read https://mathematicswithoutapologies.wordpress.com/2015/05/13 but my hopes are not high for a sudden breakthrough.
Set theorists have made a Whig History of sorts where everything leads to ZFC, but that is just their post-hoc reading of the intellectual history.
We can write Whig Histories too. See https://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf for example.
The fact is both narratives are wrong --- intellectual history is always more pluralistic and meandering than partisans want to admit in hindsight. We, as the underdogs, are ready to admit that. Can you all do the same?
See, that is the basic misunderstanding here. Foundations now is a wider topic area than it was in Gödel's day. It's like saying that automobiles run on internal combustion engines in a productive vein of manufacturing going back to Henry Ford (at least). Since those days though, there is this guy Elon who you might like to meet...
My understanding is that regular MLTT already can do all the bold things Set theory does, and HFTT (and other developments) aims to make "Proof Checker" better realized (no more "setoid hell").
Ultimately what us CS people care about is a unity of theory and practice. What drew us to computers int the first place was trying to make explicit and tangible ideas that previously were only laboriously communicated from one generation of big brains to the next in the ivory tower.
In that regards, I would say don't even look HoTT or fancy theory developments. Look at Lean, written by a non-type-theorist, and mathlib, written by a non-constructivist.
Lean and Mathilb are plainly plowing a head in ways that no set theory based tool has ever achieved, and covering all the set theory bold points in the process.
Perhaps a new more elegant type theory will replace Lean soon, but honestly I am not even worried about that. The important thing is making math much more accessible without loss of rigor with these tools. If better theories can follow rather than lead that methological revolution, that's fine with me,
As to Category Theory and essential guidance, I have a simple test :). As mathlib (or its sucesssors) matures, let us see how many proofs are refactored to use category theory! I don't want to poo-poo the deeper connections between type theory and cateogory theory, but merely using lots of category theory "library code" in a type theoretic proof assistant not itself designed with explicit reference to category theory is good enough a success story for me.
In conclusion:
- Risk Assessment: depends how many "large cardinal" type things we want (unlike the 1970s category theorists I personally don't really care)
- Regular type theory: *check*
- HoTT: *check*
- Set theory: *check*, bonus points for more exotic large cardinals
- Regular type theory: *check*
- Set theory: *check*
- HoTT: WIP because culture shock of weird equality
- Set theory: *FAIL*
- Regular type theory: *partial support*, full if we discard all constructive side goals (Lean)
- HoTT: *check*! (Very recent cubical results
- Category theory does best, but can use as "library" rather than "language". good enough for now.But formalizing proofs with computers is essentially separate from the rigorous study of the foundations of math (consistency, relative strength of theories, etc.).
You've complained above about set theorists not learning "your stuff," and now it's my turn to complain. You write: 'Risk Assessment: depends how many "large cardinal" type things we want (unlike the 1970s category theorists I personally don't really care).' Large cardinal axioms are essential to the study of the relative consistency strength of mathematical theories. You personally might not care about them, but accommodating them is not a negotiable detail for anything that purports to be useful in the study of foundations.
And yeah, I'm aware the HoTT people have ways around this, fine. My comment is more about the perspective conveyed by your remarks: if you want to have a seat at the table in a discussion about foundational issues, you need to understand basic facts like this. My suspicion is that you might have had bad interactions with set theorists because you don't share certain knowledge they take for granted, and then they get frustrated and end the conversation early. I truly believe that if you went and read a book on set theory and logic, and learned, e.g., wny large cardinals are important, you might understand better where I and other people are coming from.
It's my understanding that some larger cardinals are needed for foundations, but since the foundations problem was "solved" future work on large cardinals has continued, and that is more "more set theory for set theory's sake", than something needed to accommodate math other "regular" mathematicians are doing.
(With the possible exception of the Grothendiek and Voevodsky line of problems perhaps as the article relates --- separate and ancillary to Voevodsky's desire for a proof checker, and also separate to whether or not categorical methods alone can suffice.)
I actually don't know of type theory having "ways around this". My understanding is that while type theory doesn't appear to face fundamental obstacles here, set theory "has the lead" in making large cardinals (or their equivalents) due to being older, and the type theorists relative disinterest in this area has meant the gap is not closing.
But note that by foundations one has atleast two different meanings. One meaning being examining the consistency of axioms or finding weakest set of axioms for a theorem.
The other meaning being - finding a foundation in which a given mathematical theory is naturally and easily described, analogus to designing a programming language in which the programs are easy to describe.
Most of the time in mathematics, this is done by defining high level concepts and working from there - no need to change the foundational axioms or rules of inference.
But sometimes we need more - for instance, if you read the book "Synthetic Differential Geometry", infinitesimals are naturally embedded in the theory by working in a cartesian closed category of sets. One can either embed this in ZFC using cumbersome models, or change the logic itself(remove the law of excluded middle).
The logic in HOTT deals with equality in a more careful way than the usual foundations. This is not restricted to algebraic topology alone - it certainly includes algebraic geometry and tackles a general issue which will plausibly have many more applications once the technology is available. The field of noncommutative geometry, in the style of Connes, is also about this as the problem of taking quotients is another way of the stating the issue with equality.
It is a work in progress and might take some time before bearing substantive fruit, but note that the current alternative is that any student learning higher level mathematics at the level of Lurie's books has to go through a huge amount of foundational material while the ideas themselves may not be intrinsically complicated. Instead, this complexity is an artifact of embedding the theory in current foundations like the SDG example mentioned above.
With a new foundations, there is the possibility that we can teach the material at this level to students except that there are some tweaks in foundations.
Higher category theory is not the same thing as homotopy type theory. One does not need to learn anything about the foundations of mathematics to read and understand Lurie's work. As far as I know, issues of ZFC vs type theory simply do not arise. You can just pick up Higher Topos Theory and start reading, assuming you have a strong background in algebraic topology.
The linked article is only about higher category theory and making sure all of its claims are written down in a clear and rigorous fashion to be maximally useful to workers in the field. It has nothing to do with the foundations of mathematics as a whole.
By foundations here, I didnt mean foundations of mathematics, rather the amount of material a student needs to read to become familiar with the basic definitions of what a space means. We can teach topology to undergrads, can we teach higher categorical notions of space? Even schemes themselves had a daunting reputation some time back, now we have derived stacks which involve infinite categories.
> You can just pick up Higher Topos Theory and start reading
Yes, but my point, as illustrated in SDG example, was that definitions can be easy or hard depending on which foundations you use. You havent mentioned whether you disagree with this and if you see Kock's book, I think you will agree.
When dealing with higher categories, a foundations which uses '=' symbol in a different way, with an equivalence relation(modelled on homotopy equivalence) playing a much more prominent role could make the theory much more natural.
Note, that I am not even emphasizing sets vs type theory here, but excluded middle and a good notion of equivalence(and equivalence between equivalences... like in homotopy theory) in the foundations.
Maybe a lot of this debate will get dissolved if we just use two different words for 'examining consistency of axioms' and 'naturality of theory as encoded in a given system' instead of using the same word - foundations - for both of them.
At the very least if discussions begin with an awareness of this distinct usage, there would be lot less talking past each other.
Urs Schreiber makes the same point about naturality here - https://golem.ph.utexas.edu/category/2016/03/foundations_of_...
2) Why would we ever want to teach higher categorical notions of space to undergraduates? We can barely get them out in four years knowing real analysis and abstract algebra. The next stop would be the basic theory of manifolds, not higher topos theory.
3) I looked at Kock's book (the draft of the CUP book on his website). The definitions are more abstract than the ones I would give to undergrads, and consequently harder for them to understand. The appeal is not clear to me.
4) You don't have to change your foundations (meaning ZFC vs. type theory, etc.) to do higher category theory in a reasonable way. Again, go pick up Lurie's books. The exposition would not really be affected by whether you choose type theory or ZFC for a foundation. Let me know if you think there's a counterexample to this claim. (The exposition probably would be affected if you denied the law of excluded middle, for the worse; luckily Lurie doesn't do that.)
5) Foundations are sort of irrelevant here anyway. The point of ZFC is that you can forget about it when actually doing math. If you're thinking about foundations when reading Lurie's books, you're doing something wrong. (Consider: most mathematicians have zero opinion about foundational questions or concepts because they have no bearing on their day to day work.)
You can theoretically do everything you want in ZFC, but it's low level and a bit outdated and you don't actually want to write formal proofs in it. We know from experience that it is possible to translate the kinds of proofs that people do on paper into formal ZFC proofs, at least in theory. The mathematicians that study ZFC-like foundations are OK with that "in theory"-qualifier and are instead investigating the theoretical properties of the foundations.
The goals of (homotopy) type theory are very different: they are trying to be suitable for actually doing modern mathematics in, and computer proof assistants are being developed that make it possible to actually write down formal proofs in them, in the form of proof code. For this to work it needs to be possible to translate all the kinds of arguments that mathematicians write down on paper into formal proof steps. It is not sufficient to remark that it is theoretically possible to find some kind of translation: it must actually be done for the computer to accept the validity, and the burden must not lie on the mathematician writing down the proof. Instead, the system must make it easy to write down the steps that the mathematician wants to do. One of the kinds of arguments that mathematicians use on paper is that if A is isomorphic to B, then a theorem about A automatically gives you a corresponding theorem about B. Homotopy type theory is trying to formally enable this kind of reasoning.
In summary, the foundations people interested in ZFC have a very different goal than than the foundations people interested in (homotopy) type theory. The fact that the ZFC people are perfectly happy with ZFC and only care about ZFC doesn't mean much. The goals of the type theory people are not achieved by ZFC, not by a long shot.
Note that it is not the case that the general body of mathematicians cares about ZFC and does not care about HoTT. They care neither about HoTT nor about ZFC. The nod to ZFC that mathematicians give when pressed is mere lip service; most mathematicians would not even be able to list the axioms of ZFC. Only foundations people care about ZFC, and the kind of foundations that the ZFC people care about is irrelevant to the practice of general mathematics.
> The goals of (homotopy) type theory are very different: they are trying to be suitable for actually doing modern mathematics
> Only foundations people care about ZFC, and the kind of foundations that the ZFC people care about is irrelevant to the practice of general mathematics.
Exactly this, thanks!
I agree with your point about HoTT not being useful to the algebraic topology community, but this seems orthogonal to its usefulness in formalization: I also would not expect Lean's type theory to be directly useful to working mathematicians. Instead it can make formalization easy or even possible: Even Jacob Lurie seems to acknowledge that it could be useful for that and only disputes that it does not bring new insights on an intuitive, informal level. My reading of the discussion is that some HoTT proponents see HoTT as a new language of mathematics (similar to category theory) and that Lurie does not believe that this perspective adds much, but that he does believe that one can use that perspective to understand the theorems.
In the linked discussion Voevodsky points out that "Calculus of Inductive Constructions, the type theory that we currently using to formalize mathematics in the univalent style [and basically what Lean uses] is surprisingly convenient for doing mathematics at the level of sets and categories (and maybe 2-categories). As for mathematics of higher h-levels it is, in practice, of very little use. Note that this is a great advance of what was before as before we did not even have a system for doing abstract mathematics both formally and conveniently at the level of sets." [0]
This highlights how crucial type theory is to do modern algebraic topology, even as he seems to claim that HoTT actually can not formalize Lurie's work? Still, he seems to agree that dependent type theories were a step in the right direction (unsurprisingly, since he founded HoTT) and that more work is needed for finding new foundations for mathematics. Indeed, the, as you write below, "mistaken belief that finding a new foundation of mathematics is an interesting project in the 21st century" is something that some people in foundations (and close to the Lean community) like Jeremy Avigad are actively pursuing: see e.g. https://arxiv.org/pdf/2009.09541.pdf
[0]: https://mathematicswithoutapologies.wordpress.com/2015/05/13...
What was special about it? From memory, the formalisation [1] proceeded exactly how you would expect. Locales are simply an Isabelle mechanism (in addition to type classes) through which hierarchies of structures are built up.
[1]: https://www.isa-afp.org/entries/Grothendieck_Schemes.html
Some idea of what people in foundations think about day-to-day can be gleaned by searching the Foundations of Math mailing list archive: https://cs.nyu.edu/pipermail/fom/
In particular: don't confuse higher category theory (of interest to the algebraic topology community at large) with homotopy type theory (which is not). Jacob Lurie has a rather pointed conversation with Urs Schreiber about this, linked to here: https://mathematicswithoutapologies.wordpress.com/2015/05/18....
edit: I'd love to hear from the downvoters why they disagree with this take. It's pretty standard, afaik.