4 ms·

A new foundation for mathematics

80 points by magoghm 12y ago

jesuslop 12y ago
The Mizar project has been verifying a good share of math results for decades, not to demerit HoTT but to clarify the article.
- cscurmudgeon 12y ago
  Exactly. The HoTT folks seem to be unaware of developments like Mizar and the the Journal of Formalized Mathematics (where you submit a computer proof along with your paper).
  - chrismonsanto 12y ago
    They are almost certainly aware of Mizar. Mizar's foundation is ZFC+Tarski's axiom. If you are developing a foundation based on homotopy theory/type theory you probably don't care about results formalized in Mizar. Also the type theory people in general prefer constructivist mathematics, and would reject Axiom of Choice and friends being in the foundation.
    - cscurmudgeon 12y ago
      But doesn't Mizar void the argument that we need a new foundation as set theory has not been conducive to mechanized proofs?
      - tel 12y ago
        I don't think the argument is that it's impossible to mechanize proofs outside of HoTT---just that it's prettier and perhaps better there.
        cscurmudgeon 12y ago
        "Prettier" is subjective.
        tel 12y ago
        Absolutely. Never claimed otherwise.
      - jesuslop 12y ago
        I think this is right (not an HoTT expert), it voids it. I'd say that what type theory brings in, that didn't come for free in set theory (ZFC or Mizar's Tarski-Grodendiek extension), is the Curry-Howard correspondence that has the slogan "propositions as types, proofs as programs". With that correspondence you can see the same thing as a program (in a typed lambda calculus depending of the type theory of interest), or as a proof in a corresponding logic.
jbapple 12y ago
> The disadvantage of set theory is that its principles are very difficult to translate into the programming language of a proof assistant. I don't think that's true. There's an Isabelle theory for ZF, and the ZF axioms are actually simpler than the axiomatic system that Coq uses, the Calculus of Inductive Constructions. Backing up for a second, I'm just not sure how HoTT will make using proof assistants so much simpler. I've done a couple of largish (> 1000 lines) proof developments in Coq. The hardest part never seemed to me to be that mismatch between CIC and ZF. The hard part was that proofs are actually hard to do in a careful and complete way. The proofs I did in math class were easy because we left out a lot of the details. Let me give an example. This is from the HoTT book, Book version: first-edition-611-ga1a258c, page 368: "The field of rationals Q is constructed along the same lines as well, namely as the quotient Q : ≡ ( Z × N ) / ≈ where ( u, a ) ≈ ( v, b ) : ≡ ( u ( b + 1 ) = v ( a + 1 )) . In other words, a pair ( u, a ) represents the rational number u/ ( 1 + a ) . There can be no division by zero because we cunningly added one to the denominator a. Here too we have a canonical choice of representatives, namely fractions in lowest terms. Thus we may apply Lemma 6.10.8 to obtain a set Q, which again has a decidable equality. We do not bother to write down the arithmetical operations on Q as we trust our readers know how to compute with fractions even in the case when one is added to the denominator. Let us just record the conclusion that there is an entirely unproblematic construction of the or- dered field of rational numbers Q, with a decidable equality and decidable order. It can also be characterized as the initial ordered field." If you have experience with using proof assistants, you know how handwavy this is compared to the work required to actually get this done. Here's that development in Coq right now: https://github.com/coq/coq/tree/trunk/theories/QArith https://github.com/coq/coq/tree/trunk/theories/QArith Does HoTT really make these things simpler to write and prove? If so, what is the evidence?
- jerf 12y ago
  "Does HoTT really make these things simpler to write and prove? If so, what is the evidence?" There are people who can answer that question (or at least try to, after all I can not guarantee satisfaction), I am not one of them, and based on previous conversations on this topic, very few of them are here. (Not necessarily zero, but few.) I would suggest searching Math Overflow for an answer to your question, and failing that, post it. http://mathoverflow.net/search?q=hott http://mathoverflow.net/search?q=hott (And if you do, please drop a reply to me with a link. I'd be interested to at least read the result, though I'm well out of my depth to be commenting on it.)
amathstudent 12y ago
I'm curious - can anyone point me to an overview/exposition of this that is more hand-wavy than the book? I'm interested understanding the ideas in this work, because proofs as objects would be a major step forward, but I don't even know much about the existing systems of foundations (ZFC etc), nevermind type theory...
- sjy 12y ago
  Did you read the Introduction from pp1-12 of HoTT? I thought it was a pretty good overview.
  - amathstudent 12y ago
    I tried. I was hoping for something more like: "a field is something you can add, subtract, multiply, & divide in" and less like: "a field is a set that is a commutative group with respect to two different operations (excepting 0), linked by the distributive law". I need something to hold on to when reading the more formal treatment.
    - tel 12y ago
      I highly suggest Robert Harper's lectures from the Oregon Programming Languages Summer School. I watched the OPLSS'12 lectures, but I'm sure they're great any year.
otakucode 12y ago
Is there anyone approaching the issue from the other side? Meaning, if I have a good understanding of programming and type theory, using that to explain homotopy theory?
- tel 12y ago
  I think many people are approaching it that way. Ultimately you can end up using higher inductive types as "synthetic homotopy", i.e. homotopy theory which is by construction valid to the definition instead of carefully isolated from other constructions. So you can certainly just take the type theory and start to get at pretty large stuff in actual homotopy theory.
erik123 12y ago
Vladimir Voevodsky is making an interesting step when he says that rewrite steps in math are clearly homeomorphisms. I would like to see some more formal examples of that. It sounds like a promising path. Concerning the replacement of ZFC by Russell types -- contrary to lambda calculus' functions -- I have not run often enough in illustrations that demonstrate the usefulness of Russell types. I am personally much more vouching for a replacement of Zermelo and Fränkel's sets by Alonzo Church's functions than Bertrand Russell's types at this point. It is probably just an issue of lack of familiarity, though.

80 points by magoghm 12y ago

The Mizar project has been verifying a good share of math results for decades, not to demerit HoTT but to clarify the article.

cscurmudgeon 12y ago
Exactly. The HoTT folks seem to be unaware of developments like Mizar and the the Journal of Formalized Mathematics (where you submit a computer proof along with your paper).
- chrismonsanto 12y ago
  They are almost certainly aware of Mizar. Mizar's foundation is ZFC+Tarski's axiom. If you are developing a foundation based on homotopy theory/type theory you probably don't care about results formalized in Mizar. Also the type theory people in general prefer constructivist mathematics, and would reject Axiom of Choice and friends being in the foundation.
  - cscurmudgeon 12y ago
    But doesn't Mizar void the argument that we need a new foundation as set theory has not been conducive to mechanized proofs?
    - tel 12y ago
      I don't think the argument is that it's impossible to mechanize proofs outside of HoTT---just that it's prettier and perhaps better there.
      - cscurmudgeon 12y ago
        "Prettier" is subjective.
        tel 12y ago
        Absolutely. Never claimed otherwise.
    - jesuslop 12y ago
      I think this is right (not an HoTT expert), it voids it. I'd say that what type theory brings in, that didn't come for free in set theory (ZFC or Mizar's Tarski-Grodendiek extension), is the Curry-Howard correspondence that has the slogan "propositions as types, proofs as programs". With that correspondence you can see the same thing as a program (in a typed lambda calculus depending of the type theory of interest), or as a proof in a corresponding logic.

jbapple 12y ago

> The disadvantage of set theory is that its principles are very difficult to translate into the programming language of a proof assistant. I don't think that's true. There's an Isabelle theory for ZF, and the ZF axioms are actually simpler than the axiomatic system that Coq uses, the Calculus of Inductive Constructions. Backing up for a second, I'm just not sure how HoTT will make using proof assistants so much simpler. I've done a couple of largish (> 1000 lines) proof developments in Coq. The hardest part never seemed to me to be that mismatch between CIC and ZF. The hard part was that proofs are actually hard to do in a careful and complete way. The proofs I did in math class were easy because we left out a lot of the details. Let me give an example. This is from the HoTT book, Book version: first-edition-611-ga1a258c, page 368: "The field of rationals Q is constructed along the same lines as well, namely as the quotient Q : ≡ ( Z × N ) / ≈ where ( u, a ) ≈ ( v, b ) : ≡ ( u ( b + 1 ) = v ( a + 1 )) . In other words, a pair ( u, a ) represents the rational number u/ ( 1 + a ) . There can be no division by zero because we cunningly added one to the denominator a. Here too we have a canonical choice of representatives, namely fractions in lowest terms. Thus we may apply Lemma 6.10.8 to obtain a set Q, which again has a decidable equality. We do not bother to write down the arithmetical operations on Q as we trust our readers know how to compute with fractions even in the case when one is added to the denominator. Let us just record the conclusion that there is an entirely unproblematic construction of the or- dered field of rational numbers Q, with a decidable equality and decidable order. It can also be characterized as the initial ordered field." If you have experience with using proof assistants, you know how handwavy this is compared to the work required to actually get this done. Here's that development in Coq right now: https://github.com/coq/coq/tree/trunk/theories/QArith https://github.com/coq/coq/tree/trunk/theories/QArith Does HoTT really make these things simpler to write and prove? If so, what is the evidence?

jerf 12y ago
"Does HoTT really make these things simpler to write and prove? If so, what is the evidence?" There are people who can answer that question (or at least try to, after all I can not guarantee satisfaction), I am not one of them, and based on previous conversations on this topic, very few of them are here. (Not necessarily zero, but few.) I would suggest searching Math Overflow for an answer to your question, and failing that, post it. http://mathoverflow.net/search?q=hott http://mathoverflow.net/search?q=hott (And if you do, please drop a reply to me with a link. I'd be interested to at least read the result, though I'm well out of my depth to be commenting on it.)

amathstudent 12y ago

I'm curious - can anyone point me to an overview/exposition of this that is more hand-wavy than the book? I'm interested understanding the ideas in this work, because proofs as objects would be a major step forward, but I don't even know much about the existing systems of foundations (ZFC etc), nevermind type theory...

sjy 12y ago
Did you read the Introduction from pp1-12 of HoTT? I thought it was a pretty good overview.
- amathstudent 12y ago
  I tried. I was hoping for something more like: "a field is something you can add, subtract, multiply, & divide in" and less like: "a field is a set that is a commutative group with respect to two different operations (excepting 0), linked by the distributive law". I need something to hold on to when reading the more formal treatment.
  - tel 12y ago
    I highly suggest Robert Harper's lectures from the Oregon Programming Languages Summer School. I watched the OPLSS'12 lectures, but I'm sure they're great any year.

otakucode 12y ago

Is there anyone approaching the issue from the other side? Meaning, if I have a good understanding of programming and type theory, using that to explain homotopy theory?

tel 12y ago
I think many people are approaching it that way. Ultimately you can end up using higher inductive types as "synthetic homotopy", i.e. homotopy theory which is by construction valid to the definition instead of carefully isolated from other constructions. So you can certainly just take the type theory and start to get at pretty large stuff in actual homotopy theory.

erik123 12y ago

Vladimir Voevodsky is making an interesting step when he says that rewrite steps in math are clearly homeomorphisms. I would like to see some more formal examples of that. It sounds like a promising path. Concerning the replacement of ZFC by Russell types -- contrary to lambda calculus' functions -- I have not run often enough in illustrations that demonstrate the usefulness of Russell types. I am personally much more vouching for a replacement of Zermelo and Fränkel's sets by Alonzo Church's functions than Bertrand Russell's types at this point. It is probably just an issue of lack of familiarity, though.