What's accepted by mathematicians as the foundation of mathematics is an objective fact about the mathematical community. You can look up the answer to the question "What is the standard, commonly accepted foundation for mathematics?" in any number of reference books. Some options to get you started: Kunen's Foundations of Mathematics; Jech's Set Theory (super common books for graduate students).
My challenge to you: find a single book written in the last, say 50 years, where the answer to this question is not ZFC (or ZF with some equivocation about whether we should accept choice).
Re: "Equivalence is equivalent to equality," first of all, most mathematicians would take this to be false. Like, if "x" stands for cartesian product, they would say (A x B) x C and A x (B x C) are different objects. (This is a point commonly made in undergraduate algebra classes, and the reason they would say this is of course they they implicitly think of everything as sets, since set theory is the standard foundation!) They are isomorphic objects, but not equal ones. Second, to the extent that mathematicians suppress isomorphisms like this in their writing, this is not a new observation. We've known that mathematicians do this for decades, and in principle we could always unravel such isomorphisms when writing things down carefully if we needed to. This is not some special insight of HoTT. Compare to the forcing example I gave - this is a genuinely new insight about the Calkin algebra facilitated by "classical" methods of mathematical logic.
Re: DNNs, the question of what is a semantics for DNN does not count as an example, no. What would count: statements about things like consistency, independence, shapes, numbers, etc. It's cool that you can use HoTT for engineering things but it's not an application to discovering new pure mathematics or the consistency/proof strength/independence/etc. of that mathematics. The latter is the usual definition of "metamathematics."
Here's an example of a (true) metamathematical statement: HoTT is consistent if ZFC plus two inaccessible cardinals is consistent. (Interestingly, this is the best argument I'm aware of for the claim that HoTT is consistent, and its power derives largely from the fact that ZFC is the Gold Standard for foundations.)
Facilitating metamathematical inquiry of this kind is perhaps the primary reason mathematicians are still interested in set theory and classical logic. (I include here large cardinals, model theory, etc. For further discussion, see the books I mentioned above.)
I don't think the principles that HoTT wants to take as axiomatic are actually fundamental or ontologically basic enough to be made axiomatic. Is that so shocking?
We've been over this. To say "It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations" is not inconsistent with your claim that "there a portions of mathematics never formalized on ZFC." Both claims are true!
Also, re: the mathematical point, I asked above: "What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?" You proceeded to give examples that did not fit this description. If you agree that HoTT is not good for metamathematical inquiry, then great, we agree on something!
Also, DNNs are (definitionally) not a topic in pure mathematics.
With respect, I find your point of view "oddly narrow-minded," and not representative of what most mathematicians think about these issues. Taking these points in order:
1) I haven't written anything about constructive logic because I don't care for it, and other issues seemed more interesting to discuss. Further, the law of excluded middle has a robust presence in modern mathematical practice. A foundational system without LEM essentially by definition cannot replace ZFC for the purpose that ZFC is used for within modern mathematics. I understood the discussion to be about what should be used to ground mathematical practice.
2) "You have opinions about what you'd like from foundations." Not really. Rather, there are different goals one might want a foundational system to achieve, and we can discuss the merits of systems based on how well they meet our desired goals. I have already said, for example, that if your goal is the practical formalization of complex proofs, then type theory might very well be suitable for achieving that goal (as demonstrated by Lean).
My objections in this thread have always been that HoTT proponents are not always precise about what goals they want to achieve, and why they think HoTT is best for achieving them. That is true even if I don't care for the stated goals.
3) "They are dogmatic and are not the opinions of those mathematicians working on foundations. Those mathematicians are interested in constructive logic, computability, the computational meaning of mathematics, replacing sets with topological spaces, replacing sets with objects closer to mathematical practice, etc." The work you've just characterized is not mainstream within the community of mathematicians working on foundations and logic. Go look at what gets published in the Journal of Mathematical Logic, for example. It's just a sociological fact that the constructivist stuff (in particular) is somewhat niche (outside of say reverse mathematics, which is different than what you noted). The views I express are fairly widespread, though I put them a bit more sharply than others.
Here's a question to illustrate this point: Who at an R1 math department works primarily on the issues you mentioned? Who got hired or got tenure on the basis of this work? I can't think of anyone off the top of my head. There are at best a few topologists who got hired for their topological work who branched out into these things later. I don't doubt that if you search you can find a handful of examples - but that number is going to be much smaller than the equivalent number of people doing "classical" set theory and logic.
4) What's so wrong with not wanting the univalence axiom in my foundational system? Or thinking that this axiom is in fact a negative? It's not very ontologically primitive, after all.
The disagreement is about whether there are reasons aside from facilitating formalization to care about HoTT. (Because if not, it seems like we should all be jumping on the Lean bandwagon instead.)
It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations. The point of my post was not to explain my experience with textbooks, it was to note that you can check virtually any published source on this topic to find a reference for that claim.
Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Again, I'll happily admit type theory can be good for engineering stuff. But you claimed it was good for metamathematical inquiry. I'm looking for a statement about things like consistency, independence, shapes, numbers, etc. Set theoretical inquiry gave us tons of those, as I pointed out above.
I understand your last sentence to agree with the statement that everything could be formalized in ZFC given sufficient effort. (I do not really care by what means we know this can be done.) If so, then I'm not sure why you disagree with what I wrote previously.
Come on now. I just told in what sense ZFC has not been replaced, and you mentioned something different. No one ever claimed people actually wrote down their proofs in ZFC - again, that was never the purpose.
> Are there any which don’t exclusively apply to the mechanics of set theory itself?
Forcing has been applied to a variety of statements, including those about "normal" mathematics. The first example that comes to mind is the question of whether all automorphisms of the Calkin algebra are inner (Farah, 2011). There are many, many others.
> That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects:
You have still not given a statement an ordinary mathematician should be interested in! Type theory might good for engineering things - I'm totally on board with that. But if you claim HoTT has meta-mathematical interest, you need to give a meta-mathematical justification. That is, you need to prove something new (and interesting).
Tackling the second part first: Yes, mathematicians use all sorts of reasoning in pursuit of mathematical truth. Sometimes this reasoning is mildly sloppy, or abuses notation. So what? We all know in principle that this reasoning can be written down formally in ZFC with enough effort, if we really needed to, and this is enough to satisfy us. If you go to a mathematician and claim their work in number theory isn't actually rigorous because they wrote "7" to mean the equivalence class of 7 mod p, instead of a separate symbol like a 7 with an overbar, they will laugh at you.
> But the whole point is how to keep track of what questions one is evidently allowed to ask - what questions are demonstrably not as ill-posed as "is the number 7 equal to the trivial group".
I don't understand what you mean by "questions one is evidently allowed to ask." You can ask any questions you want. In particular, as long as we agree that whatever question you want to ask can be translated into a question about sets, we can resolve that question by answering the analogous question in the framework of ZFC. All I object to is the claim that some set is, ontologically speaking, the same as the number 7, and hence that set theory proves "junk theorems."
Here's a silly analogy. Suppose we work at NASA and we want to fly a rocket to the moon. We agree that the answer the question of how much fuel we need, we can write a computer simulation with a representation of the rocket, the earth, the moon, and so on. We run the simulation and answer our question in that simulation, and if the simulation is a good representation of reality that also answers our question in reality, and then we go to the moon and everyone is happy. However, nowhere in this process do we believe that the rocket in the simulation is the same thing as the rocket IRL.
What does it mean for "a thing to be the actual thing"? I don't think any formalization you can write down will "actually" be the number 7 (though I'm happy to consider any attempt to do this with an open mind).
> You're very dogmatic about what people should accept from a foundation. You seem happy to accept an approach that has very little to say about practice, which is certainly an opinion, but not universally held.
> There is a point of view that foundations should reflect and inform practice - or maybe even challenge practice - and are not just there to make you feel more comfortable philosophically.
I don't understand this comment. Studying set theory has said a lot about mathematical practice - for instance, about what we can and can't hope to prove in certain systems, or about what axioms are needed for what statements. That's important stuff!
More generally, there's the question of what you hope to accomplish by supplying a foundation for mathematics. Any value claim about some foundational system is contingent on what goal you have. As I said above, if that goal is actually writing down computer-checkable formalized versions of complex proofs, then ZFC is perhaps not the foundation you want to use.
But, historically speaking, that was not what people had in mind. There was a desire to reduce mathematical reasoning to a few philosophically basic concepts so that we could be confident in its coherence and consistency. And a desire for providing a framework for studying mathematical reasoning itself. I think it's really important to understand this historical context, otherwise you end up with misleading claims like "ZFC is a bad foundational system because it doesn't help me formalize my research papers."
Further, the reason I get grumpy when HoTT stuff is posted here is that the postings are rarely explicit about just why, exactly, they think HoTT should supplant ZFC as the accepted foundation of mathematics (or even exist on equal footing, creating a plurality of foundational systems). If you take the goal of a foundational system to be practically formalizing proofs, we have no evidence HoTT is particularly suited for this, and (as far as I know) no serious movement by the HoTT community to actually realize this vision (relative to what the Lean community is doing). I'm not claiming the first mover in some space should always dominate, just that if the HoTT people want to arguing for their foundational system on the grounds that it assists in formalizing math, maybe they should actually demonstrate their superiority by formalizing some math. For a longer comment on this, see: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa....
So if we disregard formalization, the arguments in favor of HoTT that remain are philosophical ones. But, as I've explained elsewhere in this thread, I find them all misguided. They all basically seem like arguments about aesthetics but don't actually tell me why HoTT is better than ZFC for the philosophical goals mentioned above.
> I came to a different conclusion: they very much meant to ground mathematics in ZFC formalisms — and went to the effort of projects like Principia trying to achieve that. ZFC was a failure in this regard, almost immediately replaced by category theory and type theory.
ZFC hasn't been "replaced" by anything. The standard line in all published textbooks that I'm aware of is that ZFC is the accepted (by the professional mathematical community) foundation for doing mathematics (assuming this question is even raised). Even the type theorists admit this!
> That’s why we replaced Turing machines with type theories, lambda calculus, automata, etc. Our modern research uses these formalisms because they’re outright better.
The Turing machine is a fundamental concept in theoretical CS that isn't going anywhere. Consider that the standard textbook on the theory of computation (Sipser's) has three parts, and the second is entirely devoted to studying computability using the Turing machine concept. Or that the strength of pushdown automata is usually explained in relation to Turing machines.
> OK, so what are the concrete fruits of this?
The first two things you listed are not metamathematical statements. I'm not sure what you mean by the third. (Sure, many things can be recognized as special cases of category-specific concepts. But that's a claim about category theory, not HoTT.)
> This is also a weird demand while leading off with how people don’t actually work in ZFC.
People do not write their papers in first order logic starting from the ZFC axioms, that's true. But the study of set theory has led to large number of metamathematical successes, such as forcing and the independence of the continuum hypothesis.
> Nevertheless, topos theory is what explains the algebra-geometry duality: you have two languages (type theories) that map to isomorphic categories. You can then extend that idea to things like the Curry-Howard square.
OK, so what's the actual concrete statement an ordinary mathematician should be interested in?
I think this is a common misconception. In set theory, one does not say that some set is the same as (ontologically) the number 7. After all, we understood what the number 7 is far before we had the concept of an abstract set in our mathematical vocabulary.
Rather, set theory lets us say that questions about 7 are equivalent to other questions about sets. So, 7 is prime if and only if some claim about sets holds, stuff like that. We do indeed usually pick some particular set to represent the number 7 for the purpose of this translation, but that isn't a claim that 7 is that set (since, e.g., there are many ways to choose a set to represent 7). So one cannot ask questions like 'is the number 7 equal to the trivial group?' within ZFC but only questions like 'is the set I've chosen to represent 7 equal to the set I've chosen to represent the trivial group,' which - while strange - shouldn't cause any philosophical worries.
I suppose to some extent this is a matter of taste. I'll just say that, in my experience, people are typically very comfortable with, e.g., logical connectives and the primitive notion of a set of objects from grade school mathematics education. So this framework is "natural" and readily believed.
Further, in ZFC, the only basic notation is that of a set. In something like the calculus of constructions, there are five fundamental notions (if I remember correctly). From the standpoint of ontological parsimony, that's a win for ZFC.
Axiom of separation just says we can make subsets of things - I think this is not so hard to swallow. I'm curious what you find counterintuitive about it.
The point of the ZFC axioms was never to write down actual formalizations of complicated proofs. It was to provide a small, parsimonious foundation for all of mathematics with a minimal number of "obvious" commitments, to give us confidence that the mathematics we're doing is consistent, and to provide a basis for metamathematical investigations. (Roughly speaking - this compresses a lot of history. Also ZFC may not be the optimal set theory for doing this, and its choice as the standard foundation is somewhat historically contingent.)
A good analogy is the idea of a Turing machine in theoretical CS. It's an idealized model for studying the theory of computation. To object that it's impractical to write a complicated program like a computer algebra system using the Turning machine formalism misses the point.
> The key idea of univalence is an axiom that says equivalence is equivalent to equality; and that if we only want equivalence as our standard, that we can substitute proofs of equivalence for proofs of equality.
I just said I don't want equivalence to be equivalent to equality!
> The main insight is that topology of diagrams determines the semantics of your logic; which helps us explore concepts like abstraction and proof simplification. (This relates to topos theory — which creeps up in CS fairly often.)
OK, so what are the concrete fruits of this? What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?
I realize it's Christmas Eve, but this post tempts my inner curmudgeon.
I do not understand why homotopy type theory posts are so popular on this website. My view is that all the "philosophical" arguments in favor of it (vs. the standard set theory foundations) misunderstand the issues at play. Further, the "practical" arguments in terms of facilitating formalization are not so compelling given the HoTT people haven't actually (as far as I know) formalized much mathematics - whereas (seemingly) less ideological communities like users of Lean have made great progress.
To expand on the comment about the philosophical arguments: take for example the abstract of this article. It states:
> It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal.
It is sometimes quite useful in practice to recognize that two isomorphic objects are not literally the same. So I am skeptical of any approach that wants to blur those distinctions.
Also, more to the point: ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs.
People have posted books on arxiv for at least a decade. Their rules state: "Submissions to arXiv should be topical and refereeable scientific contributions that follow accepted standards of scholarly communication."
Spotify high quality is 320 kps, if I remember correctly. This should be indistinguishable from lossless unless something is weird with the track.
I've done A/B testing with decent headphones (http://abx.digitalfeed.net/list.html) and not been able to tell the difference. Maybe you can, but I'd bet that most people can't, and in any case the result is far from butchery.
My challenge to you: find a single book written in the last, say 50 years, where the answer to this question is not ZFC (or ZF with some equivocation about whether we should accept choice).
Re: "Equivalence is equivalent to equality," first of all, most mathematicians would take this to be false. Like, if "x" stands for cartesian product, they would say (A x B) x C and A x (B x C) are different objects. (This is a point commonly made in undergraduate algebra classes, and the reason they would say this is of course they they implicitly think of everything as sets, since set theory is the standard foundation!) They are isomorphic objects, but not equal ones. Second, to the extent that mathematicians suppress isomorphisms like this in their writing, this is not a new observation. We've known that mathematicians do this for decades, and in principle we could always unravel such isomorphisms when writing things down carefully if we needed to. This is not some special insight of HoTT. Compare to the forcing example I gave - this is a genuinely new insight about the Calkin algebra facilitated by "classical" methods of mathematical logic.
Re: DNNs, the question of what is a semantics for DNN does not count as an example, no. What would count: statements about things like consistency, independence, shapes, numbers, etc. It's cool that you can use HoTT for engineering things but it's not an application to discovering new pure mathematics or the consistency/proof strength/independence/etc. of that mathematics. The latter is the usual definition of "metamathematics."
Here's an example of a (true) metamathematical statement: HoTT is consistent if ZFC plus two inaccessible cardinals is consistent. (Interestingly, this is the best argument I'm aware of for the claim that HoTT is consistent, and its power derives largely from the fact that ZFC is the Gold Standard for foundations.)
Facilitating metamathematical inquiry of this kind is perhaps the primary reason mathematicians are still interested in set theory and classical logic. (I include here large cardinals, model theory, etc. For further discussion, see the books I mentioned above.)