8 ms·

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 v

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.

zmgsabst 4y ago
> 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!”
- spekcular 4y ago
  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?
  - ebingdom 4y ago
    > 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.
    - 4y ago
raphlinus 4y ago
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.
- spekcular 4y ago
  Yes, it's not so clear to me either. But I'm willing to grant this point for the sake of the argument.
- zozbot234 4y ago
  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.
  - practal 4y ago
    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. [1]: https://obua.com/publications/philosophy-of-abstraction-logic/2/ https://obua.com/publications/philosophy-of-abstraction-logi...
ebingdom 4y ago
> 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.
- hash-no-gal-fld 4y ago
  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.
  - ebingdom 4y ago
    Yeah, I only meant as opposed to judgmental equality, not the quality of being a proposition.
- thechao 4y ago
  > 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.
- deleted 4y ago
  [deleted]
zozbot234 4y ago
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.
ohbtvz 4y ago
> 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.
robinzfc 4y ago
> 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. [0] [Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics] (https://www.sciencedirect.com/science/article/pii/S1570868305000765 https://www.sciencedirect.com/science/article/pii/S157086830...)
- zozbot234 4y ago
  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.
pron 4y ago
> 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.
- zozbot234 4y ago
  > work with a particular representative with a particular equality HoTT lets you do this when such a canonical representative exists. The point is to be able to generalize beyond that.
  - layer8 4y ago
    Why does it need to be canonical?
  - pron 4y ago
    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"?
cjfd 4y ago
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.
- spekcular 4y ago
  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.
  - ogogmad 4y ago
    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.
    - spekcular 4y ago
      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-fashionable-mathematics/ 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.
CoastalCoder 4y ago
> I realize it's Christmas Eve, but this post tempts my inner curmudgeon. Genius! I'm reading your comment in my best Boris Karloff (Grinch) voice. You just improved my already-nice Christmas morning :)
ogogmad 4y ago
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.
- 4y ago
puffoflogic 4y ago
> 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.
- spekcular 4y ago
  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?
- ogogmad 4y ago
  And it became the highest voted comment here. Draw your own conclusion about this place.
clircle 4y ago
For the same reasons that things like lisp and Bayesian stats get upvoted too: it’s contrarian nerd cool.
- epgui 4y ago
  Bayesian stats are only “contrarian” from a historical or undergrad perspective… It’s pretty mainstream and not really that controversial. Lisps are very different than non-lisps, but… what’s contrarian about that?

zmgsabst 4y ago

> 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!”

spekcular 4y ago
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?
- ebingdom 4y ago
  > 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.
  - 4y ago

raphlinus 4y ago

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.

spekcular 4y ago
Yes, it's not so clear to me either. But I'm willing to grant this point for the sake of the argument.
zozbot234 4y ago
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.
- practal 4y ago
  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. [1]: https://obua.com/publications/philosophy-of-abstraction-logic/2/ https://obua.com/publications/philosophy-of-abstraction-logi...

ebingdom 4y ago

> 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.

hash-no-gal-fld 4y ago
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.
- ebingdom 4y ago
  Yeah, I only meant as opposed to judgmental equality, not the quality of being a proposition.
thechao 4y ago
> 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.
deleted 4y ago
[deleted]

zozbot234 4y ago

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.

ohbtvz 4y ago

> 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.

robinzfc 4y ago

> 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. [0] [Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics] (https://www.sciencedirect.com/science/article/pii/S1570868305000765 https://www.sciencedirect.com/science/article/pii/S157086830...)

zozbot234 4y ago
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.

pron 4y ago

> 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.

zozbot234 4y ago
> work with a particular representative with a particular equality HoTT lets you do this when such a canonical representative exists. The point is to be able to generalize beyond that.
- layer8 4y ago
  Why does it need to be canonical?
- pron 4y ago
  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"?

cjfd 4y ago

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.

spekcular 4y ago
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.
- ogogmad 4y ago
  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.
  - spekcular 4y ago
    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-fashionable-mathematics/ 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.

CoastalCoder 4y ago

> I realize it's Christmas Eve, but this post tempts my inner curmudgeon. Genius! I'm reading your comment in my best Boris Karloff (Grinch) voice. You just improved my already-nice Christmas morning :)

ogogmad 4y ago

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.

4y ago

puffoflogic 4y ago

> 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.

spekcular 4y ago
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?
ogogmad 4y ago
And it became the highest voted comment here. Draw your own conclusion about this place.

clircle 4y ago

For the same reasons that things like lisp and Bayesian stats get upvoted too: it’s contrarian nerd cool.

epgui 4y ago
Bayesian stats are only “contrarian” from a historical or undergrad perspective… It’s pretty mainstream and not really that controversial. Lisps are very different than non-lisps, but… what’s contrarian about that?