3 ms·

HOL is a classical rather than constructive logic. Moreover, there is less concern about soundness of the logic.

by mafribe 11y ago

Ericson2314 11y ago
Hmm? It's fine to postulate LEM etc for irrelevant types. I've never heard of any soundness concerns with the PLs I mentioned.
dtornabene 11y ago
Could you post some links on the soundness comment? I share a fellow siblings comment of a little skepticism? But I'm neither a professionally nor scholarly logician, though I've read and owned (a couple of times) Van Heijenoorts From Frege to Godel, so feel free to throw some meat my way if you follow up with this comment.
- mafribe 11y ago
  Well-developed proof assistants like Coq and Isabelle/HOL are the current pinnacle in scientific rigour. But soundness of a foundational system is always a worry and will always remain so. By Goedel's 2nd incompleteness theorem, you cannot verify absolute soundness. This is true for HOL just as for CoC/MLTT. However, Coq, Agda etc have a much more expressive logic, which is less well understood, and I think a couple of genuine logical breakdowns have been found over the years in Coq and Agda, see e.g. [1, 2, 3], but they could all be fixed. (I'm not following the development closely, but I think the Coq/HoTT implementation even seems to require patching Coq to disable critical checks.) I don't think that the HOL tradition has had to revise logical foundations. [1] https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.h... [2] https://sympa.inria.fr/sympa/arc/coq-club/2014-01/msg00036.html https://sympa.inria.fr/sympa/arc/coq-club/2014-01/msg00036.h... [3] https://coq.inria.fr/cocorico/CoqTerminationDiscussion https://coq.inria.fr/cocorico/CoqTerminationDiscussion
  - dtornabene 11y ago
    this is fascinating! Thank you so much! I had no idea that the logic for Coq was more expressive, I can understand quite clearly how that can lead to breakdowns. I'm just slowly returning to this stuff through haskell. Heady stuff, that second mailing list post.

HOL is a classical rather than constructive logic. Moreover, there is less concern about soundness of the logic.

by mafribe 11y ago

HOL is a classical rather than constructive logic. Moreover, there is less concern about soundness of the logic.

Hmm? It's fine to postulate LEM etc for irrelevant types. I've never heard of any soundness concerns with the PLs I mentioned.

dtornabene 11y ago

Could you post some links on the soundness comment? I share a fellow siblings comment of a little skepticism? But I'm neither a professionally nor scholarly logician, though I've read and owned (a couple of times) Van Heijenoorts From Frege to Godel, so feel free to throw some meat my way if you follow up with this comment.

mafribe 11y ago
Well-developed proof assistants like Coq and Isabelle/HOL are the current pinnacle in scientific rigour. But soundness of a foundational system is always a worry and will always remain so. By Goedel's 2nd incompleteness theorem, you cannot verify absolute soundness. This is true for HOL just as for CoC/MLTT. However, Coq, Agda etc have a much more expressive logic, which is less well understood, and I think a couple of genuine logical breakdowns have been found over the years in Coq and Agda, see e.g. [1, 2, 3], but they could all be fixed. (I'm not following the development closely, but I think the Coq/HoTT implementation even seems to require patching Coq to disable critical checks.) I don't think that the HOL tradition has had to revise logical foundations. [1] https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.h... [2] https://sympa.inria.fr/sympa/arc/coq-club/2014-01/msg00036.html https://sympa.inria.fr/sympa/arc/coq-club/2014-01/msg00036.h... [3] https://coq.inria.fr/cocorico/CoqTerminationDiscussion https://coq.inria.fr/cocorico/CoqTerminationDiscussion
- dtornabene 11y ago
  this is fascinating! Thank you so much! I had no idea that the logic for Coq was more expressive, I can understand quite clearly how that can lead to breakdowns. I'm just slowly returning to this stuff through haskell. Heady stuff, that second mailing list post.