<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="">There are two problems with this quote in favor of set theory.<div class=""><br class=""></div><div class="">1. The axioms of set theory are historically contingent, i.e., they only cover the mathematics practiced at a given time.</div><div class="">For example, ZFC doesn’t cover large cardinals. An additional axiom is necessary.</div><div class="">One can easily generalize this argument by establishing new mathematical fields not covered by a given set of axioms.</div><div class="">As mentioned earlier:</div><div class=""><i class=""><span class="Apple-tab-span" style="white-space:pre"> </span>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.</i></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span><a href="https://groups.google.com/d/msg/lean-user/_A82awhFlcM/4odQJX3rCgAJ" class="">https://groups.google.com/d/msg/lean-user/_A82awhFlcM/4odQJX3rCgAJ</a></div><div class=""><br class=""></div><div class=""><div class="">2. It should be possible to derive all of mathematics from type theory (in particular, from a dependent type variant of Andrews' Q0).</div><div class="">This claim is not only stronger as is covers all (!) of mathematics possibly expressible (instead of only "the whole of known [!] mathematics").</div><div class="">Q0 was specifically designed in this spirit ("to derive practically the whole of [...] mathematics from a single source"), what Andrews calls "expressiveness".</div><div class="">The claim that a further developed variant of Q0 would be identical with (all of) mathematics was made earlier here:</div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span><a href="https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/7fCLcrftCQAJ" class="">https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/7fCLcrftCQAJ</a></div><div class=""><br class=""></div><div class="">See also this contribution:</div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>Type Theory vs. Set Theory (HOL, Isabelle/HOL, Q0, and R0 vs. ZFC)</div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span><a href="https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00000.html" class="">https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00000.html</a></div><div class=""><br class=""></div><div class="">In short:</div><div class="">While type theory is a systematic approach, set theory was an auxiliary solution useful for practical needs at that time.</div><div class=""><div class=""><br class=""></div><div class="">Jean van Heijenoort had expressed this very precisely:</div></div><div class=""><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span><span style="font-family: LMRoman10; font-size: 11pt;" class="">9. Jean van Heijenoort on the </span><span style="font-family: LMRoman10; font-size: 11pt; font-style: italic;" class="">development of type theory and set theory</span><span style="font-family: LMRoman10; font-size: 11pt;" class="">: “In spite of the great
advances that set theory was making, the very notion of set remained vague. The situation
became critical after the appearance of the Burali-Forti paradox and intolerable after that of
the Russell paradox, the latter involving the bare notions of set and element. One response to
the challenge was Russell’s theory of types </span><span style="font-family: LMRoman10; font-size: 11pt;" class="">[</span><span style="font-size: 11pt; font-family: LMMathItalic10;" class="">...</span><span style="font-family: LMRoman10; font-size: 11pt;" class="">]</span><span style="font-family: LMRoman10; font-size: 11pt;" class="">. Another, coming at almost the same time, was
Zermelo’s axiomatization of set theory. The two responses are extremely different; the former
is a far-reaching theory of great significance for logic and even ontology, while the latter is an
immediate answer to the pressing needs of the working mathematician.” [Heijenoort, </span><span style="font-family: LMRoman10; font-size: 11pt; color: rgb(0, 255, 0);" class="">1967c</span><span style="font-family: LMRoman10; font-size: 11pt;" class="">,
p. 199] </span></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span><a href="https://owlofminerva.net/files/fom_2018.pdf#page=12" class="">https://owlofminerva.net/files/fom_2018.pdf#page=12</a></div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Kind regards,<br class=""><br class="">Ken Kubota</div><div class=""><br class=""></div><div class=""><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><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><br class=""><blockquote type="cite" class=""><div class="">Am 09.03.2020 um 01:25 schrieb Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" class="">m.escardo@cs.bham.ac.uk</a>>:</div><br class="Apple-interchange-newline"><div class=""><div class="">James,<br class=""><br class="">This resonates a bit with what Bourbaki wrote in "Introduction to the<br class="">Theory of Sets",<br class=""><a href="http://sites.mathdoc.fr/archives-bourbaki/feuilleter.php?chap=2_REDAC_E1:" class="">http://sites.mathdoc.fr/archives-bourbaki/feuilleter.php?chap=2_REDAC_E1:</a><br class=""><br class="">"... nowadays it is known to be possible, logically speaking, to derive<br class="">practically the whole of known mathematics from a single source, the<br class="">Theory of Sets. ... By so doing we do not claim to legislate for all<br class="">time. It may happen at some future date that mathematicians will agree<br class="">to use modes of reasoning which cannot be formalized in the language<br class="">described here; according to some, the recent evolution of axiomatic<br class="">homology theory would be a sign that this date is not so far. It would<br class="">then be necessary, if not to change the language completely, at least to<br class="">enlarge its rules of syntax. But this is for the future to decide."<br class=""><br class="">(I learned this quote from Thierry Coquand.)<br class=""><br class="">Martin<br class=""><br class="">On 08/03/2020 13:35, James McKinna wrote:<br class=""><blockquote type="cite" class="">Martin, on Fri, 06 Mar 2020, you wrote:<br class=""><br class=""><blockquote type="cite" class="">In other words, choose your proof assistant as a function of what you<br class="">want to talk about *and* how you want to talk about it. Martin<br class=""><br class="">On 06/03/2020 21:05, Martin Escardo wrote:<br class=""><blockquote type="cite" class="">The troubling aspect of proof assistants is that they not only<br class="">implement proof checking (and definition checking, construction<br class="">checking etc.) but that also that each of them proposes a new<br class="">foundation of mathematics.<br class=""><br class="">Which is sometimes not precisely specified, as it is the case of e.g.<br class="">Agda. (Which is why I, as an Agda user, I confine myself to a<br class="">well-understood subset of Agda corresponding to a (particular)<br class="">well-understood type theory.<br class=""><br class="">For mathematically minded users of proof assistants, like myself,<br class="">this is a problem. We are not interested in formal proofs per se. We<br class="">are interested in what we are talking about, with rigorously stated<br class="">assumptions about our universe of discourse.<br class=""></blockquote></blockquote></blockquote><br class=""></div></div></blockquote><br class=""><blockquote type="cite" class=""><div class=""><div class="">-- <br class="">Martin Escardo<br class=""><a href="http://www.cs.bham.ac.uk/~mhe" class="">http://www.cs.bham.ac.uk/~mhe</a><br class=""></div></div></blockquote></div><br class=""></div></div></body></html>