<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.apple-tab-span
{mso-style-name:apple-tab-span;}
span.EmailStyle19
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">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></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">This claim is not only stronger as is covers all (!) of mathematics possibly expressible (instead of only "the whole of known [!] mathematics").<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Q0 was specifically designed in this spirit ("to derive practically the whole of [...] mathematics from a single source"), what Andrews calls "expressiveness".<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">The claim that a further developed variant of Q0 would be identical with (all of) mathematics was made earlier here:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><a href="https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/7fCLcrftCQAJ">https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/7fCLcrftCQAJ</a><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif">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="color:black"><o:p></o:p></span></span></p>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Am 09.03.2020 um 01:25 schrieb Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>>:<o:p></o:p></p>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">James,<br>
<br>
This resonates a bit with what Bourbaki wrote in "Introduction to the<br>
Theory of Sets",<br>
<a href="http://sites.mathdoc.fr/archives-bourbaki/feuilleter.php?chap=2_REDAC_E1:">http://sites.mathdoc.fr/archives-bourbaki/feuilleter.php?chap=2_REDAC_E1:</a><br>
<br>
"... nowadays it is known to be possible, logically speaking, to derive<br>
practically the whole of known mathematics from a single source, the<br>
Theory of Sets. ... By so doing we do not claim to legislate for all<br>
time. It may happen at some future date that mathematicians will agree<br>
to use modes of reasoning which cannot be formalized in the language<br>
described here; according to some, the recent evolution of axiomatic<br>
homology theory would be a sign that this date is not so far. It would<br>
then be necessary, if not to change the language completely, at least to<br>
enlarge its rules of syntax. But this is for the future to decide."<br>
<br>
(I learned this quote from Thierry Coquand.)<br>
<br>
Martin<br>
<br>
On 08/03/2020 13:35, James McKinna wrote:<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal" style="margin-left:36.0pt">Martin, on Fri, 06 Mar 2020, you wrote:<br>
<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal" style="margin-left:36.0pt">In other words, choose your proof assistant as a function of what you<br>
want to talk about *and* how you want to talk about it. Martin<br>
<br>
On 06/03/2020 21:05, Martin Escardo wrote:<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal" style="margin-left:36.0pt">The troubling aspect of proof assistants is that they not only<br>
implement proof checking (and definition checking, construction<br>
checking etc.) but that also that each of them proposes a new<br>
foundation of mathematics.<br>
<br>
Which is sometimes not precisely specified, as it is the case of e.g.<br>
Agda. (Which is why I, as an Agda user, I confine myself to a<br>
well-understood subset of Agda corresponding to a (particular)<br>
well-understood type theory.<br>
<br>
For mathematically minded users of proof assistants, like myself,<br>
this is a problem. We are not interested in formal proofs per se. We<br>
are interested in what we are talking about, with rigorously stated<br>
assumptions about our universe of discourse.<o:p></o:p></p>
</blockquote>
</blockquote>
</blockquote>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
</div>
</blockquote>
<p class="MsoNormal" style="margin-left:36.0pt"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">-- <br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe">http://www.cs.bham.ac.uk/~mhe</a><o:p></o:p></p>
</div>
</div>
</blockquote>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
</div>
</div>
<PRE>
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
</PRE></body>
</html>