<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 class=""><br class=""></div><div><blockquote type="cite" class=""><div class="">Am 13.03.2020 um 17:19 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="">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]).<o:p class=""></o:p></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">This means you have a very intensional view of Mathematics centred around encodings. I think this is misleading because Mathematics is about abstraction and abstract concepts, encodings are only coincidental.</div></div></div></blockquote><div><br class=""></div><div>Of course, encoding is not a self-purpose.</div><div>That all logical connectives can be defined in terms of the Sheffer stroke is coincidental and not of particular interest.</div><div>But the concept of expressiveness (reducibility) used by Andrews (and intuitively by Church) is very natural, and for good reason many mathematicians endorse these formulations of higher-order logic (Church's type theory, Andrews' Q0, Gordon's HOL), and the implementations are widely used (HOL4, HOL Light, Isabelle/HOL).</div><div>In this concept, the reduction to certain primitive symbols is very natural and reveals the inner logic of high level notions.</div><div><br class=""></div><br class=""><blockquote type="cite" 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; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""></o:p></div><div class=""><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-size: 11pt;" 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: </span></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 style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">Q0 basically has a single variable binder (lambda), two primitive symbols and two primitive types, and a single rule of inference.<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="">R0 has only little more (some features required for type variables, type abstraction, and dependent types).<o:p class=""></o:p></div></div></div><div class=""><div class=""><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">Both are Hilbert-style systems (operating at the object language level only).<o:p class=""></o:p></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">This seems to be a view of mathematical foundations stuck in the middle of the last century.<o:p class=""></o:p></div></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 style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">The notion of type theory you refer to seems to intend more than just preventing (negative) self-reference.<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 univalence axiom, and the desire to „structure mathematical constructions in a reasonable way“ are motivated by philosophical or metamathematical considerations.<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="">These motivations have their legitimation, but shouldn’t be part of the formal language.<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 style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" 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" style="color: blue; text-decoration: underline;" class="">https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ</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="">I believe that type abstraction is fully sufficient to express what the Pi type is supposed to express.<o:p class=""></o:p></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">So you are only interested in some mathematical machine code but not in the high level notions. Such a view of mathematical foundation is akin to the view some programmers had (and maybe still have) that all what matters is machine code. To the contrary you can build the same foundations on different notions of machine code. The machine code is irrelevant, all what matters are the abstractions.</div></div></div></blockquote><div><br class=""></div><div>It is important to distinguish two different kinds of high level notions:</div><div>Those that can be reduced naturally to primitive symbols, and those which try to express metamathematical ideas (which seems to be your notion).</div><div>The latter shouldn't be implemented as primitive symbols in the basic formal language, but should be the result of metamathematical reasoning.</div><div><br class=""></div><br class=""><blockquote type="cite" 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 class=""><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><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><span style="font-size: 11pt;" class="">How is type abstraction implemented in Lean, and where can I find the group definition?</span></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 style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">I have no idea about Lean, not do I know what you mean by “type abstraction”. Polymorphism, that is constructions which are parametric in types are simply depdnent functions which have a universe as input.</div></div></div></blockquote><div><br class=""></div><div>Lambda as the single variable binder in formulations of higher-order logic (Church, Andrews, Gordon) traditionally can be used to bind _term variables_ only.</div><div>Type abstraction allows for binding _type variables_ also.</div><div>See <a href="https://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/" class="">https://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/</a></div><div>and <a href="https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html" class="">https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html</a></div><div>Kevin Buzzard has (like Freek Wiedijk) correctly stated that current classical higher-order logic is too weak to express certain mathematical concepts.</div><div>The main reason is that the feature of type abstraction is missing.</div><div>Gordon has suggested implementing this, but unfortunately this didn't happen in the current HOL systems (HOL4, HOL Light, Isabelle/HOL).</div><div>Andrews and Melham did some work into this direction, but used the traditional quantifiers to bind type variables, not lambda.</div><div><br class=""></div><br class=""><blockquote type="cite" 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 class=""><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><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="">Concerning constructivism (intuitionism) and intensionality, these are philosophical debates with little relevance for mathematics nowadays.<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="">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/" style="color: blue; text-decoration: underline;" class="">https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/</a><o:p class=""></o:p></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">I think you miss a trick or two here. Constructivism is highly relevant, especially in computer science when we want to marry computer science with mathematical constructions. Hilbert is already dead since a while and before the first computer has been build. The world is changing, maybe philosophers and mathematicians should take notice of this.</div></div></div></blockquote><div><br class=""></div><div>The formulation of the formal system depends on the purpose.</div><div>Even within mathematics different formulations are required: <a href="https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/lArtWey5CQAJ" class="">https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/lArtWey5CQAJ</a> (last part on the two-step approach).</div><div>However, from a logical (mathematical) point of view I do not see any need for constructivism.</div><div><br class=""></div><div><br class=""></div><blockquote type="cite" 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 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="">Cheers,<o:p class=""></o:p></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">Thorsten<o:p class=""></o:p></div></div></div></div></div></div></div></div></div></div></div></div></div></blockquote></div><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""></div><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""></div>Kind regards,</div><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""></div><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Ken Kubota</div><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class=""><br class=""></div><div class=""><div 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 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></body></html>