<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">Within type theory certain mathematical ideas can be expressed with dependent types only.</div><div class=""><br class=""></div><div class="">In particular, if the type of the result returned by a function depends on the argument, dependent types are required.</div><div class="">The example I chose is a function that returns the first unit vector of a given dimension: <a href="https://www.owlofminerva.net/files/formulae.pdf#page=12" class="">https://www.owlofminerva.net/files/formulae.pdf#page=12</a></div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Let me quote from an earlier email available at <a href="https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ" class="">https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ</a> :</div><div class=""><br class=""></div><div class=""><i class="">But it is also clear that HOL's type system (and therefore Isabelle/HOL's type system) is poor.<br class=""><br class="">Freek Wiedijk on the (current) HOL family: “There is one important reason why the HOLs are not yet attractive enough to be taken to be the QED system:<br class="">• The HOL type system is too poor. As we already argued in the previous section, it is too weak to properly do abstract algebra.<br class="">But it is worse than that. In the HOL type system there are no dependent types, nor is there any form of subtyping. (Mizar and Coq both have dependent types and some form of subtyping. In Mizar the subtyping is built into the type system. In Coq a similar effect is accomplished through the use of automatic coercions.)<br class="">For formal mathematics it is essential to both have dependent types and some form of subtyping.” [Wiedijk, 2007, p. 130, emphasis as in the original]<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span><a href="https://owlofminerva.net/files/fom_2018.pdf#page=10" class="">https://owlofminerva.net/files/fom_2018.pdf#page=10</a></i></div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">For example, in HOL or Isabelle/HOL group theory cannot be expressed naturally (since type abstraction is missing), not even mentioning functions involving dependent types like that returning the first unit vector of a given dimension as mentioned above.</div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Note that there are also formulations of dependent type theory with classical foundations, see: <a href="https://owlofminerva.net/files/fom_2018.pdf#page=1" class="">https://owlofminerva.net/files/fom_2018.pdf#page=1</a></div><div class=""><br class=""></div><div class="">I would consider type theory superior to set theory as type theory is a systematic approach, whereas the axioms of set theory are historically contingent.</div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Kind regards,</div><div class=""><br class=""></div><div class="">Ken Kubota</div><div class=""><br class=""></div><div class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><span style="color: rgb(210, 210, 210); font-family: sans-serif; font-size: small;" class="">____________________________________________________</span></div><div class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class=""><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><font class="" face="Arial" size="1"><br class=""></font></div><font class="" face="Arial" size="1"><br class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><b class="">Ken Kubota</b></div><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"></div><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"></div><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><a href="https://doi.org/10.4444/100" class="">doi.org/10.4444/100</a></div><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><br class=""></div></font></div></div></div></div></div></div></div></div></div></div></div></div><br class="Apple-interchange-newline">
</div>
<div><br class=""><blockquote type="cite" class=""><div class="">Am 03.03.2020 um 20:43 schrieb Jason Gross <<a href="mailto:jasongross9@gmail.com" class="">jasongross9@gmail.com</a>>:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">I'm in the process of writing my thesis on proof assistant performance bottlenecks (with a focus on Coq), and there's a large class of performance bottlenecks that come from (mis)using the power of dependent types. So in writing the introduction, I want to provide some justification for the design decision of using dependent types, rather than, say, set theory or classical logic (as in, e.g., Isabelle/HOL). And the only reasons I can come up with are "it's fun" and "lots of people do it"<div class=""><br class=""></div><div class="">So I'm asking these mailing lists: why do we base proof assistants on dependent type theory? What are the trade-offs involved?</div><div class="">I'm interested both in explanations and arguments given on list, as well as in references to papers that discuss these sorts of choices.</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">Jason</div></div>
</div></blockquote></div><br class=""></div></div></div></div></div></body></html>