<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 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 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 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="">Hi Thorsten,<br class=""><br class=""><div><blockquote type="cite" class=""><div class="">Am 10.03.2020 um 12:10 schrieb Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" class="">Thorsten.Altenkirch@nottingham.ac.uk</a>>:</div><br class="Apple-interchange-newline"><div class=""><div class="WordSection1" style="page: WordSection1; caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; 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;"><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div><div class=""><div class=""><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">2. It should be possible to derive all of mathematics from type theory (in particular, from a dependent type variant of Andrews' Q0).<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">This claim is not only stronger as is covers all (!) of mathematics possibly expressible (instead of only "the whole of known [!] mathematics").<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">Q0 was specifically designed in this spirit ("to derive practically the whole of [...] mathematics from a single source"), what Andrews calls "expressiveness".<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">The claim that a further developed variant of Q0 would be identical with (all of) mathematics was made earlier here:<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><a href="https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/7fCLcrftCQAJ" style="color: purple; text-decoration: underline;" class="">https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/7fCLcrftCQAJ</a><o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div></div><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-size: 10pt; font-family: Arial, sans-serif;" class="">I don’t agree with this description. As set theory, type theory is an evolving system. For example a while ago we were using intensional type theory with uniqueness of identity proofs and now we have a much more extensional type theory with univalence and without uip. And also the question isn’t just wether we “can derive” all Mathematics but can we structure mathematical constructions in a reasonable way. Otherwise we are left with the usual argument that all programs can be written in machine language.<span style="" class=""><o:p class=""></o:p></span></span></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></blockquote></div><div class=""><br class=""></div><div class="">It seems that the traditions of type theory we represent are very different, so a reasonable answer should reflect the underlying basic design decisions.</div><div class="">In the examples you mention intensional type theory, the univalence axiom, and the desire to "structure mathematical constructions in a reasonable way".</div><div class=""><br class=""></div><div class="">My concept of type theory is in the tradition of Russell, Church, and Andrews – in particular Andrews' Q0, which is an elegant reformulation of Church's type theory (1940, see: <a href="https://owlofminerva.net/sep-q0" class="">https://owlofminerva.net/sep-q0</a>).</div><div class="">The purpose of the types in this concept of type theory is mainly to preserve the dependencies such that (negative) self-reference causing paradoxes/antinomies is avoided, as discussed here: <a href="https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html" class="">https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html</a></div><div class=""><br class=""></div><div class="">This means that types are the result of simple operations such as lambda abstraction and lambda application (cf. wff constructions (b) and (c) at [Andrews 2002 (ISBN 1-4020-0763-9), p. 211]).</div><div class=""><br class=""></div><div class="">Moreover, using Andrews' concept of "expressiveness" (also intuitively used by Church before), all mathematical concepts can be reduced – naturally (not like in machine language) – to a few basic notions: </div><div class=""><div class="">Q0 basically has a single variable binder (lambda), two primitive symbols and two primitive types, and a single rule of inference.</div><div class="">R0 has only little more (some features required for type variables, type abstraction, and dependent types).</div></div><div class=""><div class="">Both are Hilbert-style systems (operating at the object language level only).</div></div><div class=""><br class=""></div><div class="">The notion of type theory you refer to seems to intend more than just preventing (negative) self-reference.</div><div class="">The univalence axiom, and the desire to „structure mathematical constructions in a reasonable way“ are motivated by philosophical or metamathematical considerations.</div><div class="">These motivations have their legitimation, but shouldn’t be part of the formal language.</div><div class=""><br class=""></div><div class="">For this reason I already object to the Pi type (as implemented in Lean), or dependent function type, which I consider a metamathematical notion: <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="">I believe that type abstraction is fully sufficient to express what the Pi type is supposed to express.</div><div class=""><br class=""></div><div class="">How is type abstraction implemented in Lean, and where can I find the group definition?</div><div class=""><br class=""></div><div class="">Concerning constructivism (intuitionism) and intensionality, these are philosophical debates with little relevance for mathematics nowadays.</div><div class="">I fully agree to Kevin Buzzard’s argument that "within mathematics departments, the prevailing view is that Hilbert won the argument 100 years ago and we have not looked back since, despite what constructivists want us to believe." – <a href="https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/" class="">https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/</a></div><div class=""><br class=""></div><div class="">Kind regards,</div><div class=""><div class=""><br class=""></div><div class="">Ken Kubota</div><div class=""><div class=""><br class=""></div><div 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></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></body></html>