3 ms·

> 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

> 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. https://zmichaelgehlke.com/images/curry-howard-square-graphic.jpg https://zmichaelgehlke.com/images/curry-howard-square-graphi...

zozbot234 4y ago
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.
- zmgsabst 4y ago
  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.
ekidd 4y ago
> 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?
- zmgsabst 4y ago
  Michael Robinson is the person I know working on this topic — and who I borrowed the phrasing from. https://www.drmichaelrobinson.net/sheaftutorial/ https://www.drmichaelrobinson.net/sheaftutorial/ https://arxiv.org/abs/1603.01446 https://arxiv.org/abs/1603.01446
  - ekidd 4y ago
    Thank you, that is very helpful!
spekcular 4y ago
> 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

zozbot234 4y ago

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.

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

ekidd 4y ago

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

zmgsabst 4y ago
Michael Robinson is the person I know working on this topic — and who I borrowed the phrasing from. https://www.drmichaelrobinson.net/sheaftutorial/ https://www.drmichaelrobinson.net/sheaftutorial/ https://arxiv.org/abs/1603.01446 https://arxiv.org/abs/1603.01446
- ekidd 4y ago
  Thank you, that is very helpful!

spekcular 4y ago

> 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