6 ms·

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

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

zmgsabst 4y ago
> ZFC hasn't been "replaced" by anything. 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
- spekcular 4y ago
  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).
  - zmgsabst 4y ago
    > 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.
    - spekcular 4y ago
      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.

zmgsabst 4y ago

> ZFC hasn't been "replaced" by anything. 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

spekcular 4y ago
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).
- zmgsabst 4y ago
  > 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.
  - spekcular 4y ago
    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.