As I understand it, submissions are moderated (albeit lightly -- not to the degree of formal peer review). So, since it's on the arXiv, we can assume that the moderators felt it belongs there.
I've seen a number of other book-length items on the arXiv before, including e.g. Seven Sketches in Compositionality [1], so this isn't a particularly new trend, either.
To post there you simply need someone to vet you. Typically your advisor, coauthor, or a colleague but they don't check the relationship. The system is rarely abused tbh. Introductions, surveys, and books are actively welcomed. At least I welcome them and find them extremely useful. We want open access (and open source) knowledge, right?
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."
I didn't really have time for the school, but I'm working through the book to learn MLTT. (Although I took a break to work through PLFA and do advent of code.)
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.
> So I am skeptical of any approach that wants to blur those distinctions.
HoTT doesn’t blur those distinctions — it formalizes the distinction.
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.
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.)
> ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs.
Counterpoint: no it doesn’t, because almost every working mathematician uses a higher level type theory in their work that “compiles” to ZFC and will run away screaming if you try to make them compile their work down to formal ZFC statements because set theory is a garbage foundation — the worst of the three options.
“My axioms do everything but formalize proofs!” is the equivalent of “my car does everything but drive!”
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?
> 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
I would argue that type theory does a better job at this than set theory. With set theory, you need to believe in two separate things: (1) the language of first-order logic (or some other logic) with its inference rules, (2) the set theory axioms. With type theory, there is only the language of lambda terms. And the rules for type theory are straightforward and intuitive for programmers, e.g., you can only call a function on an argument if the function's domain matches the type of the argument. Contrast that with set theory, where you have highly counterintuitive and seemingly arbitrary axioms like the axiom of separation.
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.
Nobody's comparing the aesthetics of sets to types. That's not the point... People want mathematical proofs to automatically determine programs, or to be more than just proofs somehow. They want to exploit the capabilities of constructive logic. The fact that arbitrary sets can intersect each other makes extracting computational meaning from set theory proofs harder. The fact that types can be like sets but don't have to be is also why they're interesting: The notion has more flexibility.
I'm not sure you can call the type rules for CiC "intuitive for programmers". They're quite powerful and go further than "type of argument matches expected type".
Compared to CoC, first order logic is a model of simplicity, and I think it's reasonable to argue that adding the inductive types to get to CiC is as complex as adding a handful of axioms to Fol to obtain ZFC. And don't forget to pick a flavor of universe polymorphism or cumulativity to make it usable. That's not exactly simple.
I think there's a good case for CiC or HoTT being nice and usable for mathematicians. I don't think they're simple or more appealing to programmers. A kernel for metamath is the simplest, and it has more independent implementations than any other system.
> 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.
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.
> To object that it's impractical to write a complicated program like a computer algebra system using the Turning machine formalism misses the point.
No — it’s exactly the point.
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.
> OK, so what are the concrete fruits of this?
Translating a type theory into a AST; translating an AST into bytecode. White boarding to design software. Formalisms for Feynman diagrams and similar.
Then you have that sheaves are the natural language for data fusion and sensor integration - which doesn’t apply to people who don’t know the topic, but is an industrial reason to learn it.
On the purely mathematical side, topos theory is what has shown relationships between many areas of mathematics, by showing when you translate those theories from their own language into categories you get equivalent structures.
> What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?
This is also a weird demand while leading off with how people don’t actually work in ZFC.
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.
ZF(C) was not a failure as a proof-of-concept, and before formalizations could be verified by machinery that was all that a formalization could be useful for! This was just as true of Russell and Whitehead's Principia, of course. Category theory was not originally intended as a foundation, either.
I agree that ZFC was an important and useful step in mathematics — but it fell short of its aims in both ways:
- you can’t provide a solid basis for all math (though, ZFC is useful to prove that)
- you can’t use it to produce papers of increased assurance, eg to remove the issues that had arisen with contrary calculus proofs
Category theory was intended to solve a shortcoming of ZFC: the lack of tools to reason about “large” similarity and classes — such as algebra and geometry being the same topic. Category theory formalized those notions.
> Then you have that sheaves are the natural language for data fusion and sensor integration - which doesn’t apply to people who don’t know the topic, but is an industrial reason to learn it.
Ah, this is super interesting. Are there any good introductions to this topic, especially ones accessible to people who know some basic category theory and a bit about topoi, but who are weak at topology?
> 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?
My experience is the opposite: ZFC hasn’t been “replaced” in the sense that it never was - we always used an intermediate language of established theory which we compiled to ZFC. ZFC never formalized all of mathematics, as the high level congruences that drove category theory were always developed on an independent framework. Further, computers always were grounded in type theory and diagram equivalence (literally, the correspondence between circuit diagrams and type theories).
> But the study of set theory has led to large number of metamathematical successes, such as forcing and the independence of the continuum hypothesis.
Are there any which don’t exclusively apply to the mechanics of set theory itself?
> The first two things you listed are not metamathematical statements.
I noted fruits ranging from applied mathematics (eg, computer products) to meta mathematics; I think it’s important to understand applications as well.
> OK, so what's the actual concrete statement an ordinary mathematician should be interested in?
That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects:
- we can encode proof engines as difference equations to run in GPUs
- we can extract some “effective type theory” from difference equations interpreted as diagrams, which preliminary results suggest also relates to convolutions
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).
> I just told in what sense ZFC has not been replaced, and you mentioned something different.
You told me your personal experience with textbooks and I told you mine. That’s how conversations work — why are you upset?
You’re also factually wrong: I was pointing out areas of mathematics that (contrary to your claim) were never formalized in ZFC.
> You have still not given a statement an ordinary mathematician should be interested in!
I don’t think you’re being sincere at this point: the formalisms to accelerate reasoning engines and to extract semantic content of DNNs is of clear interest to many working professionals.
- - - - -
I think both threads have something in common:
You’re dressing up your personal feelings (and ignorance) as grand statements about the field.
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.
> It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations.
This is factually untrue — there a portions of mathematics never formalized on ZFC and there’s not consensus around that. I listed the areas that weren’t formalized on ZFC already.
You’re making bullshit up to make your personal biases sound grander than they are.
- - - -
> But you claimed it was good for metamathematical inquiry.
No — you claimed that, as a strawman of my position.
But you’re welcome to answer yourself: how do you formalize that equivalence is equivalent to equality without univalence?
You’re on a huff, but never addressed the original point. From my very first post.
> Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem.
Wrong.
We lacked the meta mathematical framework outlining what semantics is to enable us to do that — until HoTT told us that the semantics of a system are in its topology. In that sense, HoTT is merely a fact about topos theory: the topology of your semantic model is the interesting part.
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.
Yes — we have been over that: multiple independent bases means there’s no “standard” one and you’re projecting your own biases as grand proclamations.
I understand your ego doesn’t let you separate your experience from that others may have — and so anyone who doesn’t share your view is “objectively” wrong. That flaw in thinking is common in STEM personalities — but what you’re calling “objective” is your subjective bias.
> 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?"
I answered in my very first post and reiterated it in the last one, but you still haven’t addressed that:
Equivalence is equivalent to equality.
How do you formalize that meta mathematical notion in other frameworks? — or are you going to ignore that a third time because you don’t have an answer?
> Also, DNNs are (definitionally) not a topic in pure mathematics.
Definitionally, the question “what is semantics?” is meta mathematics — even if you apply the answer.
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.)
Is there actually any proof system running on GPUs?! I'd love to read about that. Afaict it must be super hard because tree manipulation is not great on GPUs...
There's tons of juice left on the CPU side. Again I recommend Metamath Zero (which is somewhat of an opposite direction as HoTT), as it's able to check the entire Metamath proof database in a few hundred milliseconds. This is orders of magnitude faster than most other proof systems.
If you did want to manipulate trees on the GPU, then my stack monoid work[1] might be a good basis for it.
Of course, a whole nother direction is to use AI to develop proofs, which is a fascinating and growing area (see Holophrasm[2] and DeepMind work[3]). That of course runs on the GPU.
I think you're overstating the case against ZFC as a practical basis for proof formalization. The Metamath project has got pretty far even without powerful tactics and so on, and has an appealingly simple kernel. That work continues in Mario Carneiro's Metamath Zero, which does add some pretty basic automation, and is able to prove a simple C-like compiler among other things.
Of course I admit that Lean is pretty much cleaning everybody else's clock, but it's not clear to me that's because of the inherent superiority of type theory over set theory. It's equally plausible that it's just well engineered, and there's been a lot more attention on automating type theory by computer scientists.
If you want to "automate" set theory, you pretty much have to build a type theory on top of it. This is what Mizar does (one of the oldest projects in formalized math, but still going strong). It also starts by assuming extremely strong set-theoretic axioms, to make this more convenient.
The type theoretic approach is ultimately more elegant; the basic foundation is a bit more complex than material set theory, but the complexity is of a kind that's used basically everywhere in a practical formalization. It avoids the pattern of building complicated stuff on top of an overly simple axiomatic basis.
You are probably confusing "automation" with "mechanisation" here, and maybe also with "computing".
It is very easy to automate set theory, at least when it is just embedded in first-order logic, and at least compared to type theory. Automation of first-order logic is MUCH further and MUCH easier than automation of type theory, which is usually not much automated at all apart from a few tactics here and there.
Furthermore, the prevalent use of type theory for mechanised interactive theorem proving is based on the work of Church on simple type theory, and extensions of that into dependent types. Computer scientists like the lambda calculus and types, and it gives a nice and general way for implementing binding. It also is straightforward to compute in it, but that is also easy to implement for set theory if you are interested in it (most people doing set theory are not).
Ultimately, though, both set theory and type theory are just specific mathematical theories. This became apparent to me after I discovered what is probably the best foundational logic, Abstraction Logic (AL) [1], in which you can represent both as mathematical theories. AL is like first-order logic, but plus operators (and therefore binding), and like higher-order logic, but minus static types.
What is missing for AL is an actual system implementing it, but that is in the works.
> ...in which you can represent both as mathematical theories...
There are many logical frameworks (LF's) that are targeted at this same space. They're especially useful for exploring automated conversions of high-level "theories" to different axiomatic systems.
Yes, I know. The reason why you call them "frameworks" instead of logics is because they don't have a model-theory based semantics, but are justified via proof theory. Abstraction logic on the other hand is a logic with its own model-theory based semantics.
To further elaborate why this is important: When you implement a logic in some LF, then it is up to you to do a pen and paper argument of what the semantics of your logic is, and why it is faithfully represented via the constructs of the LF, which itself has no semantics. On the other hand, to implement a logic in AL, you just write down its axioms, and the semantics of AL automatically gives a semantics for your logic, including soundness and completeness results. Of course, you still need to do a pen and paper argument that the semantics of your logic via AL is faithful to the semantics of your standalone logic. But this will only be done for the first few logics you implement in AL, future logics will just inherit their semantics from AL, and that will be their semantics then by definition.
Lean is well engineered, is also marketed as a programming language, and expressive enough to do proper math in it. Type theory is more elegant to implement than set theory based on first-order logic. That's about it.
Nevertheless, first-order logic is not the last word when it comes to formalising set theory, I think Abstraction Logic (AL)[1] is. When you start formalising set-like and type-like things in AL, the border between sets and types disappears. That border is just an artefact of history, useful for foundational studies, but will lose its importance for anything practical.
> I do not understand why homotopy type theory posts are so popular on this website.
Martin-Löf type theory (and, therefore, homotopy type theory) is like an idealized programming language that is capable of expressing both programs and proofs, such that you can prove your code correct in the same language. Hacker News is a mostly technical community that often likes to geek out on programming languages.
Homotopy type theory is an especially cool flavor of type theory that finally gives a satisfying answer to the question of when two types should be considered propositionally equal.
I don't think you intended "propositionally" equal in your final sentence. Equality is data in HoTT. If you take the propositional truncation then you usually throw away too much.
> finally gives a satisfying answer to the question of when two types should be considered propositionally equal
One of my fondest memories was listening to Walid Taha debate Jeremy Siek, Todd Veldhuizen, and others, over beers, about the best way to define type equivalence in nontrivial type systems. It seemed so abstract, until I had to debug a template instantiation issue in GCC.
Lean as a system is also founded on a theory of types (which can also be seen as a "structural" set theory). If you want to see what a 'practical' formalization based on material set theory might look like, there's Metamath. The difference in usability is quite stark.
> So I am skeptical of any approach that wants to blur those distinctions.
The HoTT approach does not blur this; it says that isomorphism is equivalent to sameness, so there are ways to regard isomorphic objects as "much like the same" in some contexts while "not the same" in others.
> I do not understand why homotopy type theory posts are so popular on this website.
It's easy. When you don't know a lot of math beyond college, but you see a post like this one, voting it up lets you pretend that you're in-the-know. "Oh yeah, I'm competent enough to upvote this. I know math." You may even end up fooling yourself into believing it. Same thing happens with physics, chemistry, linguistics... posts.
> except serve as a basis for practical formalization of proofs
I do formalized mathematics as a hobby and I can not see any basis for that opinion.
Freek Wiedijk wrote an interesting paper [0] where he compared the complexity of various foundations as encoded in Automath.
Mizar, which is based on Tarski–Grothendieck set theory (an extension of ZFC) is a proof assistant whose library was the largest for a couple of decades, only recently surpassed by Lean's Mathlib (perhaps). Metamath is mentioned below in comments and of course my favorite Isabelle/ZF are also based on ZFC.
The complexity of foundations is not the only relevant measure, you should also look at total complexity. Type theory is such that useful formalizations can be built directly on it as an axiomatic basis (and when this can't be done it's seen as something to be addressed, as with HoTT as a direct foundation for homotopy), whereas set theories don't let you do this.
> except serve as a basis for practical formalization of proofs
That might well be true for advanced mathematics, but in practical software engineering, TLA+, which uses ZFC for its "data" portion (its computational portion is based on a linear temporal logic called TLA), is not only the most popular of the "deep" specification languages (although that's not saying too much), but one of the most successful practical applications by ordinary practitioners (i.e. not logicians or other academic researchers) of deep formal logic in the history of formal logic. True, most users don't bother writing deductive proofs in the TLA+ proof assistant and prefer using model checkers available for TLA+ because they have a higher ROI, but still.
> My view is that all the "philosophical" arguments in favor of it (vs. the standard set theory foundations) misunderstand the issues at play.
Perhaps ironically, it is precisely the power of the notion of isomorphism that means it is often simpler and more practical to keep it in the meta-logic and work with a particular representative with a particular equality rather than baking the very notion of isomorphism into the heart of the logic itself (which is very interesting from a logician's perspective, but doesn't necessarily lead to better pragmatic results for practitioners). I.e. it is because isomorphism is so fundamental that we don't need it in the logic, and it can serve as the foundation for a foundation rather as the foundation itself. Of course, logicians enjoy exploring taking as much of the meta-logic and philosophy and putting it into the logic. That's pretty much what logicians are meant to do. Unfortunately, not too many of them are also interested in the question of how to make a logic more friendly to practitioners.
The larger point is should a foundation serve logicians interested in designing mathematical foundations or practitioners interested in formalising proofs (and specifications)? It's easy to see why such theories would be interesting to logicians, who should certainly study them, but they may not help furthering formal mathematics or the use of formal logic in the field.
Of course, putting more meta-theory into the logic should be explored, and it's even possible that it may turn out to have other desired effects. However, a foundation is usually not of interest to practitioners for the same reasons it is of interest to logicians, and it is that point that logicians sometimes miss. They try selling a particular theory on the basis of things that are of interest to them (we've put isomorphism in the language) rather than things that are of interest to practitioners (proofs are shorter, written in a more natural way, easier for machines to assist with etc.). The reasons to research a topic are often not those that best sell it to others. In other words, would it also be "the point" for a practitioner "to be able to generalise beyond that"?
> The larger point is should a foundation serve logicians interested in designing mathematical foundations or practitioners interested in formalising proofs (and specifications)?
I think this question can easily be answered in the affirmative. A key point of HoTT and univalence is that being able to work with isomorphism as if it was equality, and freely transport proofs and functions 'across' isomorphisms, makes for more intuitive proofs that get less bogged down in issues of logical formalism and closer to what a practitioner would want to write.
(I don't know, and I don't have a dog in this fight, being neither a practitioner nor a logician. I'm asking because, following the thread of the discussion, I could easily see a logician saying "Of course this will make it easier for the practitioners" about something that, in actual practice, the practitioners don't care about at all.)
I think that transporting proofs "for free" is of less interest since we're talking about formal, and so mechanised, proofs [1], but the matter of writing proofs more naturally could definitely be a selling point. Can you point to some examples of that?
[1]: A computer can formally apply meta-logical transformations as a proof tactic, too. Why not put that into the logic if it can be done formally? To keep it simpler and easier for practitioners to learn. (Some systems, like TLA+, allow you to specify and prove higher order theorems that aren't expressible as formulas in the logic; so while you might not be able to express the general notion of an isomorphism in this way, you can express a theorem that can then be used by the proof assistant to transfer proofs based on isomorphisms with respect to some specific number of operators with some specific arities)
Come to think of it, there's another aspect I don't understand. The validity of a theorem depends only on the assumptions used in the proof (so, for example, if I have a formal set theory proof that depends only on group axioms, then it applies to all groups). That is not a property that is usually expressible in the the logic -- it's a property of the proof theory of the logic -- but it is nevertheless true. Not being a logician, I'm not interested in writing proofs about my logic's proof theory, I don't need to define new proof rules as I don't develop new logics, and my logic's proof assistant is free to rely on theorems about the logic's proof theory. What do I, as a practitioner, gain by making the proof theory part of the logic?
IMO ZFC is extremely ugly because it has no notion of types. One can ask questions like 'is the number 7 equal to the trivial group?'. Ultimately both are a bunch of nested sets so a priori they may or may not be equal. The calculus of constructions is, I think the nicest looking candidate for a foundation of mathematics. It is very nice that definitions, which one is going to need anyway in any sort of mathematical exposition, are part of the system from the start.
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.
OK, but that's in ZFC. You don't have to do things that way. Not everything needs to be an encoding of a thing. Sometimes we want a thing to be the actual thing.
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.
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.
OK listen, spekcular. You haven't responded to any of my comments about constructive logic.
> But, historically speaking, that was not what people had in mind.
You have opinions about what you'd like from foundations. 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.
> 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
Nobody's really saying that. That's your own combative fanatasy or confusion. You're not a logician; you don't know foundations; and you're ignorant of logic-in-CS, based on your inability to understand some of the terms used and the following remark you've made:
> 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.
That word salad alone should make people stop listening to you. But this is HN, so *shrug*.
You are right maybe about combinatorics, but in this sort of maths, you are useless and oddly narrow-minded.
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.
> So one cannot ask questions like 'is the number 7 equal to the trivial group?'
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". You're saying that set theory doesn't even attempt to do this, so it seems that this is one thing that type theory does a better job of addressing. Mathematicians commonly engage in what are formally abuses of notation, mixing up equivalence classes and their representatives, or neglecting distinctions between sets that are defined quite differently and related by an injection, e.g. the natural numbers and the integers. These arguments need some fixing before they can be made logically rigorous, and type theory helps with that.
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.
> So what? We all know in principle that this reasoning can be written down formally in ZFC with enough effort
But how can you know this? You're starting from reasoning in natural language that, by your own admission, sometimes engages in "sloppy" abuses of notation, such as treating isomorphism as if it could be equated with identity. Whenever mathematicians argue that "this can be written down formally in ZFC" they're essentially using a sloppy, informal, ad-hoc version of type theory and higher-level logic in the process; they're merely in denial about this point.
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.
> everything could be formalized in ZFC given sufficient effort
Since I'm not sure what could be comprised under "everything", I don't think I can agree with that statement. The whole point of "practical" formalization efforts is to add some rigor to such assertions. And you've acknowledged that type theoretical foundations can be useful to practitioners, so what's it exactly that you disagree about?
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.)
Constructive logic is logic without the Law of Excluded Middle. It is the part of mathematics that is actually relevant to computing.
HoTT serves as a good foundation for constructive logic; perhaps better than any other. Set theory (like ZFC) makes doing constructive logic very awkward, as the very idea of an infinite set (which can be union'd and intersected with any other infinite set) is unnatural in such a logic (but can be made to work if you accept some pain). Martin-Lof Type Theory isn't "good enough", because it handles equality quite poorly, which is fundamental to logic. For instance, how would you state the Axiom Of Unique Choice in Martin-Lof Type Theory?
The idea behind HoTT (over Martin-Lof TT) is that path-connectedness in a topological space is somehow more fundamental than equality. Equality is recovered when that space becomes discrete. Everything that's possible in set theoretic foundations is possible in HoTT, because a set is just a discrete topological space. Equivalence relations are constructed by simply building bridges between points, and then contracting connected components down to points.
The idea behind Martin-Lof TT is that there is a rough duality between how you prove things and how you program things. Propositions correspond to types in MLTT, and proofs correspond to programs. In MLTT, this is taken to be an isomorphism between proofs->programs and propositions->types. In HoTT, this is usually not taken to be an isomorphism, as propositions are instead understood as only some of the types (the subsingletons).
In MLTT, the whole point of constructive logic becomes clear. The proposition "There are infinitely many prime numbers" is a type (like in some programming languages) whose elements are programs which take integers as input and produce larger primes as output. If you look at the standard proof of "There are infinitely many prime numbers", you'll see that it determines an algorithm. This is not the best example, as the resulting algorithm is rather naive, but there are plenty of better examples.
> 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.
It's called inverting a surjective function. You can do that in HoTT, or any foundation. In fact, this remark shows you're dangerously over-opinionated.
> 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.
What does ZFC really do? The axioms are pretty obtuse, abstract, divorced from mathematical practice (who the hell needs to know that an integer is an infinite set), infinitary and non-constructive and hostile to computers.
You invoke LEM when you can't decide computationally whether a proposition is true or not. If you could decide, you wouldn't invoke it.
Admittedly, I exaggerated a bit because my comments were already too long. You can always prove an algorithm correct by using LEM somewhere. It's just nice to have a mathematical universe where "everything is computable" which immediately rules out LEM.
> 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.
This paragraph betrays that you have not done much work at all with HoTT. Type theory would be inconsistent if distinguishable objects could be substituted. It is not accurate to say that they are treated as "literally the same". Indeed the whole point of HoTT is that substitutive equality is not the only useful kind.
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?
Here's a short paper that I spent several hours grokking as my first intro to Homotopy Type Theory, and which eventually sent me down a journey learning algebra, topology, and logic in order to fully understand HoTT:
83 comments
[ 3.0 ms ] story [ 159 ms ] threadI've seen a number of other book-length items on the arXiv before, including e.g. Seven Sketches in Compositionality [1], so this isn't a particularly new trend, either.
[1] https://arxiv.org/abs/1803.05316v3
This book looks to be based on those notes (which themselves came from a course a year earlier).
I’d definitely recommend this book on the strength of that experience.
[1] - https://hott.github.io/HoTT-2019/images/hott-intro-rijke.pdf
https://github.com/martinescardo/HoTTEST-Summer-School/tree/... https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest_su...
I didn't really have time for the school, but I'm working through the book to learn MLTT. (Although I took a break to work through PLFA and do advent of code.)
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.
HoTT doesn’t blur those distinctions — it formalizes the distinction.
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.
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.)
> ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs.
Counterpoint: no it doesn’t, because almost every working mathematician uses a higher level type theory in their work that “compiles” to ZFC and will run away screaming if you try to make them compile their work down to formal ZFC statements because set theory is a garbage foundation — the worst of the three options.
“My axioms do everything but formalize proofs!” is the equivalent of “my car does everything but drive!”
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 would argue that type theory does a better job at this than set theory. With set theory, you need to believe in two separate things: (1) the language of first-order logic (or some other logic) with its inference rules, (2) the set theory axioms. With type theory, there is only the language of lambda terms. And the rules for type theory are straightforward and intuitive for programmers, e.g., you can only call a function on an argument if the function's domain matches the type of the argument. Contrast that with set theory, where you have highly counterintuitive and seemingly arbitrary axioms like the axiom of separation.
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.
Compared to CoC, first order logic is a model of simplicity, and I think it's reasonable to argue that adding the inductive types to get to CiC is as complex as adding a handful of axioms to Fol to obtain ZFC. And don't forget to pick a flavor of universe polymorphism or cumulativity to make it usable. That's not exactly simple.
I think there's a good case for CiC or HoTT being nice and usable for mathematicians. I don't think they're simple or more appealing to programmers. A kernel for metamath is the simplest, and it has more independent implementations than any other system.
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.
> To object that it's impractical to write a complicated program like a computer algebra system using the Turning machine formalism misses the point.
No — it’s exactly the point.
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.
> OK, so what are the concrete fruits of this?
Translating a type theory into a AST; translating an AST into bytecode. White boarding to design software. Formalisms for Feynman diagrams and similar.
Then you have that sheaves are the natural language for data fusion and sensor integration - which doesn’t apply to people who don’t know the topic, but is an industrial reason to learn it.
On the purely mathematical side, topos theory is what has shown relationships between many areas of mathematics, by showing when you translate those theories from their own language into categories you get equivalent structures.
> What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?
This is also a weird demand while leading off with how people don’t actually work in ZFC.
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.
https://zmichaelgehlke.com/images/curry-howard-square-graphi...
- you can’t provide a solid basis for all math (though, ZFC is useful to prove that)
- you can’t use it to produce papers of increased assurance, eg to remove the issues that had arisen with contrary calculus proofs
Category theory was intended to solve a shortcoming of ZFC: the lack of tools to reason about “large” similarity and classes — such as algebra and geometry being the same topic. Category theory formalized those notions.
Ah, this is super interesting. Are there any good introductions to this topic, especially ones accessible to people who know some basic category theory and a bit about topoi, but who are weak at topology?
https://www.drmichaelrobinson.net/sheaftutorial/
https://arxiv.org/abs/1603.01446
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?
My experience is the opposite: ZFC hasn’t been “replaced” in the sense that it never was - we always used an intermediate language of established theory which we compiled to ZFC. ZFC never formalized all of mathematics, as the high level congruences that drove category theory were always developed on an independent framework. Further, computers always were grounded in type theory and diagram equivalence (literally, the correspondence between circuit diagrams and type theories).
> But the study of set theory has led to large number of metamathematical successes, such as forcing and the independence of the continuum hypothesis.
Are there any which don’t exclusively apply to the mechanics of set theory itself?
> The first two things you listed are not metamathematical statements.
I noted fruits ranging from applied mathematics (eg, computer products) to meta mathematics; I think it’s important to understand applications as well.
> OK, so what's the actual concrete statement an ordinary mathematician should be interested in?
That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects:
- we can encode proof engines as difference equations to run in GPUs
- we can extract some “effective type theory” from difference equations interpreted as diagrams, which preliminary results suggest also relates to convolutions
> 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).
You told me your personal experience with textbooks and I told you mine. That’s how conversations work — why are you upset?
You’re also factually wrong: I was pointing out areas of mathematics that (contrary to your claim) were never formalized in ZFC.
> You have still not given a statement an ordinary mathematician should be interested in!
I don’t think you’re being sincere at this point: the formalisms to accelerate reasoning engines and to extract semantic content of DNNs is of clear interest to many working professionals.
- - - - -
I think both threads have something in common:
You’re dressing up your personal feelings (and ignorance) as grand statements about the field.
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.
This is factually untrue — there a portions of mathematics never formalized on ZFC and there’s not consensus around that. I listed the areas that weren’t formalized on ZFC already.
You’re making bullshit up to make your personal biases sound grander than they are.
- - - -
> But you claimed it was good for metamathematical inquiry.
No — you claimed that, as a strawman of my position.
But you’re welcome to answer yourself: how do you formalize that equivalence is equivalent to equality without univalence?
You’re on a huff, but never addressed the original point. From my very first post.
> Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem.
Wrong.
We lacked the meta mathematical framework outlining what semantics is to enable us to do that — until HoTT told us that the semantics of a system are in its topology. In that sense, HoTT is merely a fact about topos theory: the topology of your semantic model is the interesting part.
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.
I understand your ego doesn’t let you separate your experience from that others may have — and so anyone who doesn’t share your view is “objectively” wrong. That flaw in thinking is common in STEM personalities — but what you’re calling “objective” is your subjective bias.
> 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?"
I answered in my very first post and reiterated it in the last one, but you still haven’t addressed that:
Equivalence is equivalent to equality.
How do you formalize that meta mathematical notion in other frameworks? — or are you going to ignore that a third time because you don’t have an answer?
> Also, DNNs are (definitionally) not a topic in pure mathematics.
Definitionally, the question “what is semantics?” is meta mathematics — even if you apply the answer.
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.)
Currently moving shape types to digital image transforms; next up is Zn.
https://www.zmgsabstract.com/whitepapers/shapes-as-digital-i...
https://www.zmgsabstract.com/whitepapers/shapes-have-operati...
There's tons of juice left on the CPU side. Again I recommend Metamath Zero (which is somewhat of an opposite direction as HoTT), as it's able to check the entire Metamath proof database in a few hundred milliseconds. This is orders of magnitude faster than most other proof systems.
If you did want to manipulate trees on the GPU, then my stack monoid work[1] might be a good basis for it.
Of course, a whole nother direction is to use AI to develop proofs, which is a fascinating and growing area (see Holophrasm[2] and DeepMind work[3]). That of course runs on the GPU.
[1]: https://arxiv.org/abs/2205.11659
[2]: https://arxiv.org/abs/1608.02644
[3]: https://www.deepmind.com/publications/proving-theorems-using...
It does? Where? I'm not huge in theoretical CS, but I have never seen topos theory show up in CS. Maybe I just didn't notice?
Of course I admit that Lean is pretty much cleaning everybody else's clock, but it's not clear to me that's because of the inherent superiority of type theory over set theory. It's equally plausible that it's just well engineered, and there's been a lot more attention on automating type theory by computer scientists.
The type theoretic approach is ultimately more elegant; the basic foundation is a bit more complex than material set theory, but the complexity is of a kind that's used basically everywhere in a practical formalization. It avoids the pattern of building complicated stuff on top of an overly simple axiomatic basis.
It is very easy to automate set theory, at least when it is just embedded in first-order logic, and at least compared to type theory. Automation of first-order logic is MUCH further and MUCH easier than automation of type theory, which is usually not much automated at all apart from a few tactics here and there.
Furthermore, the prevalent use of type theory for mechanised interactive theorem proving is based on the work of Church on simple type theory, and extensions of that into dependent types. Computer scientists like the lambda calculus and types, and it gives a nice and general way for implementing binding. It also is straightforward to compute in it, but that is also easy to implement for set theory if you are interested in it (most people doing set theory are not).
Ultimately, though, both set theory and type theory are just specific mathematical theories. This became apparent to me after I discovered what is probably the best foundational logic, Abstraction Logic (AL) [1], in which you can represent both as mathematical theories. AL is like first-order logic, but plus operators (and therefore binding), and like higher-order logic, but minus static types.
What is missing for AL is an actual system implementing it, but that is in the works.
[1]: https://obua.com/publications/philosophy-of-abstraction-logi...
There are many logical frameworks (LF's) that are targeted at this same space. They're especially useful for exploring automated conversions of high-level "theories" to different axiomatic systems.
To further elaborate why this is important: When you implement a logic in some LF, then it is up to you to do a pen and paper argument of what the semantics of your logic is, and why it is faithfully represented via the constructs of the LF, which itself has no semantics. On the other hand, to implement a logic in AL, you just write down its axioms, and the semantics of AL automatically gives a semantics for your logic, including soundness and completeness results. Of course, you still need to do a pen and paper argument that the semantics of your logic via AL is faithful to the semantics of your standalone logic. But this will only be done for the first few logics you implement in AL, future logics will just inherit their semantics from AL, and that will be their semantics then by definition.
Nevertheless, first-order logic is not the last word when it comes to formalising set theory, I think Abstraction Logic (AL)[1] is. When you start formalising set-like and type-like things in AL, the border between sets and types disappears. That border is just an artefact of history, useful for foundational studies, but will lose its importance for anything practical.
[1]: https://obua.com/publications/philosophy-of-abstraction-logi...
Martin-Löf type theory (and, therefore, homotopy type theory) is like an idealized programming language that is capable of expressing both programs and proofs, such that you can prove your code correct in the same language. Hacker News is a mostly technical community that often likes to geek out on programming languages.
Homotopy type theory is an especially cool flavor of type theory that finally gives a satisfying answer to the question of when two types should be considered propositionally equal.
One of my fondest memories was listening to Walid Taha debate Jeremy Siek, Todd Veldhuizen, and others, over beers, about the best way to define type equivalence in nontrivial type systems. It seemed so abstract, until I had to debug a template instantiation issue in GCC.
> So I am skeptical of any approach that wants to blur those distinctions.
The HoTT approach does not blur this; it says that isomorphism is equivalent to sameness, so there are ways to regard isomorphic objects as "much like the same" in some contexts while "not the same" in others.
It's easy. When you don't know a lot of math beyond college, but you see a post like this one, voting it up lets you pretend that you're in-the-know. "Oh yeah, I'm competent enough to upvote this. I know math." You may even end up fooling yourself into believing it. Same thing happens with physics, chemistry, linguistics... posts.
I do formalized mathematics as a hobby and I can not see any basis for that opinion.
Freek Wiedijk wrote an interesting paper [0] where he compared the complexity of various foundations as encoded in Automath.
Mizar, which is based on Tarski–Grothendieck set theory (an extension of ZFC) is a proof assistant whose library was the largest for a couple of decades, only recently surpassed by Lean's Mathlib (perhaps). Metamath is mentioned below in comments and of course my favorite Isabelle/ZF are also based on ZFC.
[0] [Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics] (https://www.sciencedirect.com/science/article/pii/S157086830...)
That might well be true for advanced mathematics, but in practical software engineering, TLA+, which uses ZFC for its "data" portion (its computational portion is based on a linear temporal logic called TLA), is not only the most popular of the "deep" specification languages (although that's not saying too much), but one of the most successful practical applications by ordinary practitioners (i.e. not logicians or other academic researchers) of deep formal logic in the history of formal logic. True, most users don't bother writing deductive proofs in the TLA+ proof assistant and prefer using model checkers available for TLA+ because they have a higher ROI, but still.
> My view is that all the "philosophical" arguments in favor of it (vs. the standard set theory foundations) misunderstand the issues at play.
Perhaps ironically, it is precisely the power of the notion of isomorphism that means it is often simpler and more practical to keep it in the meta-logic and work with a particular representative with a particular equality rather than baking the very notion of isomorphism into the heart of the logic itself (which is very interesting from a logician's perspective, but doesn't necessarily lead to better pragmatic results for practitioners). I.e. it is because isomorphism is so fundamental that we don't need it in the logic, and it can serve as the foundation for a foundation rather as the foundation itself. Of course, logicians enjoy exploring taking as much of the meta-logic and philosophy and putting it into the logic. That's pretty much what logicians are meant to do. Unfortunately, not too many of them are also interested in the question of how to make a logic more friendly to practitioners.
HoTT lets you do this when such a canonical representative exists. The point is to be able to generalize beyond that.
Of course, putting more meta-theory into the logic should be explored, and it's even possible that it may turn out to have other desired effects. However, a foundation is usually not of interest to practitioners for the same reasons it is of interest to logicians, and it is that point that logicians sometimes miss. They try selling a particular theory on the basis of things that are of interest to them (we've put isomorphism in the language) rather than things that are of interest to practitioners (proofs are shorter, written in a more natural way, easier for machines to assist with etc.). The reasons to research a topic are often not those that best sell it to others. In other words, would it also be "the point" for a practitioner "to be able to generalise beyond that"?
I think this question can easily be answered in the affirmative. A key point of HoTT and univalence is that being able to work with isomorphism as if it was equality, and freely transport proofs and functions 'across' isomorphisms, makes for more intuitive proofs that get less bogged down in issues of logical formalism and closer to what a practitioner would want to write.
(I don't know, and I don't have a dog in this fight, being neither a practitioner nor a logician. I'm asking because, following the thread of the discussion, I could easily see a logician saying "Of course this will make it easier for the practitioners" about something that, in actual practice, the practitioners don't care about at all.)
[1]: A computer can formally apply meta-logical transformations as a proof tactic, too. Why not put that into the logic if it can be done formally? To keep it simpler and easier for practitioners to learn. (Some systems, like TLA+, allow you to specify and prove higher order theorems that aren't expressible as formulas in the logic; so while you might not be able to express the general notion of an isomorphism in this way, you can express a theorem that can then be used by the proof assistant to transfer proofs based on isomorphisms with respect to some specific number of operators with some specific arities)
Come to think of it, there's another aspect I don't understand. The validity of a theorem depends only on the assumptions used in the proof (so, for example, if I have a formal set theory proof that depends only on group axioms, then it applies to all groups). That is not a property that is usually expressible in the the logic -- it's a property of the proof theory of the logic -- but it is nevertheless true. Not being a logician, I'm not interested in writing proofs about my logic's proof theory, I don't need to define new proof rules as I don't develop new logics, and my logic's proof assistant is free to rely on theorems about the logic's proof theory. What do I, as a practitioner, gain by making the proof theory part of the logic?
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.
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.
> 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.
> But, historically speaking, that was not what people had in mind.
You have opinions about what you'd like from foundations. 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.
> 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
Nobody's really saying that. That's your own combative fanatasy or confusion. You're not a logician; you don't know foundations; and you're ignorant of logic-in-CS, based on your inability to understand some of the terms used and the following remark you've made:
> 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.
That word salad alone should make people stop listening to you. But this is HN, so *shrug*.
You are right maybe about combinatorics, but in this sort of maths, you are useless and oddly narrow-minded.
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.
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". You're saying that set theory doesn't even attempt to do this, so it seems that this is one thing that type theory does a better job of addressing. Mathematicians commonly engage in what are formally abuses of notation, mixing up equivalence classes and their representatives, or neglecting distinctions between sets that are defined quite differently and related by an injection, e.g. the natural numbers and the integers. These arguments need some fixing before they can be made logically rigorous, and type theory helps with that.
> 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.
But how can you know this? You're starting from reasoning in natural language that, by your own admission, sometimes engages in "sloppy" abuses of notation, such as treating isomorphism as if it could be equated with identity. Whenever mathematicians argue that "this can be written down formally in ZFC" they're essentially using a sloppy, informal, ad-hoc version of type theory and higher-level logic in the process; they're merely in denial about this point.
Since I'm not sure what could be comprised under "everything", I don't think I can agree with that statement. The whole point of "practical" formalization efforts is to add some rigor to such assertions. And you've acknowledged that type theoretical foundations can be useful to practitioners, so what's it exactly that you disagree about?
Genius! I'm reading your comment in my best Boris Karloff (Grinch) voice. You just improved my already-nice Christmas morning :)
HoTT serves as a good foundation for constructive logic; perhaps better than any other. Set theory (like ZFC) makes doing constructive logic very awkward, as the very idea of an infinite set (which can be union'd and intersected with any other infinite set) is unnatural in such a logic (but can be made to work if you accept some pain). Martin-Lof Type Theory isn't "good enough", because it handles equality quite poorly, which is fundamental to logic. For instance, how would you state the Axiom Of Unique Choice in Martin-Lof Type Theory?
The idea behind HoTT (over Martin-Lof TT) is that path-connectedness in a topological space is somehow more fundamental than equality. Equality is recovered when that space becomes discrete. Everything that's possible in set theoretic foundations is possible in HoTT, because a set is just a discrete topological space. Equivalence relations are constructed by simply building bridges between points, and then contracting connected components down to points.
The idea behind Martin-Lof TT is that there is a rough duality between how you prove things and how you program things. Propositions correspond to types in MLTT, and proofs correspond to programs. In MLTT, this is taken to be an isomorphism between proofs->programs and propositions->types. In HoTT, this is usually not taken to be an isomorphism, as propositions are instead understood as only some of the types (the subsingletons).
In MLTT, the whole point of constructive logic becomes clear. The proposition "There are infinitely many prime numbers" is a type (like in some programming languages) whose elements are programs which take integers as input and produce larger primes as output. If you look at the standard proof of "There are infinitely many prime numbers", you'll see that it determines an algorithm. This is not the best example, as the resulting algorithm is rather naive, but there are plenty of better examples.
> 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.
It's called inverting a surjective function. You can do that in HoTT, or any foundation. In fact, this remark shows you're dangerously over-opinionated.
> 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.
What does ZFC really do? The axioms are pretty obtuse, abstract, divorced from mathematical practice (who the hell needs to know that an integer is an infinite set), infinitary and non-constructive and hostile to computers.
How so? How, specifically, does computing need the absence of the Law of Excluded Middle?
Admittedly, I exaggerated a bit because my comments were already too long. You can always prove an algorithm correct by using LEM somewhere. It's just nice to have a mathematical universe where "everything is computable" which immediately rules out LEM.
This paragraph betrays that you have not done much work at all with HoTT. Type theory would be inconsistent if distinguishable objects could be substituted. It is not accurate to say that they are treated as "literally the same". Indeed the whole point of HoTT is that substitutive equality is not the only useful kind.
Lisps are very different than non-lisps, but… what’s contrarian about that?
https://mathweb.ucsd.edu/~ebelmont/hott.pdf
> The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.