5 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 m

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.
- spekcular 4y ago
  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.
  - ogogmad 4y ago
    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.
- c-cube 4y ago
  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.
zmgsabst 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. 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.

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.

spekcular 4y ago
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.
- ogogmad 4y ago
  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.
c-cube 4y ago
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.

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