4 ms·

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

by 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.)
tel 12y ago
I'm no expert, but I believe the hope is that quotients are easier to work with in HoTT than they would be elsewhere since you can treat the resulting "cosets" as true objects instead of structure with proof. Also, it should be much easier to transport proofs from type to type according to isomorphisms that are discovered. I'm hardly versed enough to say whether those things are (a) true (b) actually occurring (c) powerful enough to be worth the potential headaches HoTT incurs or (d) deserving of acclaim, but it's at least my understanding.
- jbapple 12y ago
  As far as quotients go, I have used setoids before for that purpose. Maybe HoTT makes quotients even more convenient. http://coq.inria.fr/V8.2pl1/refman/Reference-Manual030.html http://coq.inria.fr/V8.2pl1/refman/Reference-Manual030.html
  - tel 12y ago
    Yes, my understanding is that quotients should be much more convenient to use than setoids. Univalance means you can more or less ignore equality in the quotient after you define it---proofs should just be transportable.
4ad 12y ago
The problem is not whether HoTT is easier than ZF. The problem is that ZF is impossible to be used in a proof assistant because it uses classical logic. HoTT uses intuitionistic logic where all proofs are constructive.
- tel 12y ago
  Non-constructive proofs aren't problematic for theorem provers---they just have no computable interpretation. You can just assert the Law of Excluded Middle if you like whenever and all of the programs "downstream" will still be checkable. You can even technically provide computable semantics to Pierce's law via call/cc.

by jbapple 12y ago

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

tel 12y ago

I'm no expert, but I believe the hope is that quotients are easier to work with in HoTT than they would be elsewhere since you can treat the resulting "cosets" as true objects instead of structure with proof. Also, it should be much easier to transport proofs from type to type according to isomorphisms that are discovered. I'm hardly versed enough to say whether those things are (a) true (b) actually occurring (c) powerful enough to be worth the potential headaches HoTT incurs or (d) deserving of acclaim, but it's at least my understanding.

jbapple 12y ago
As far as quotients go, I have used setoids before for that purpose. Maybe HoTT makes quotients even more convenient. http://coq.inria.fr/V8.2pl1/refman/Reference-Manual030.html http://coq.inria.fr/V8.2pl1/refman/Reference-Manual030.html
- tel 12y ago
  Yes, my understanding is that quotients should be much more convenient to use than setoids. Univalance means you can more or less ignore equality in the quotient after you define it---proofs should just be transportable.

4ad 12y ago

The problem is not whether HoTT is easier than ZF. The problem is that ZF is impossible to be used in a proof assistant because it uses classical logic. HoTT uses intuitionistic logic where all proofs are constructive.

tel 12y ago
Non-constructive proofs aren't problematic for theorem provers---they just have no computable interpretation. You can just assert the Law of Excluded Middle if you like whenever and all of the programs "downstream" will still be checkable. You can even technically provide computable semantics to Pierce's law via call/cc.