<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.EmailStyle18
{mso-style-type:personal;
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"><b><span style="font-size:12.0pt;color:black">From: </span></b><span style="font-size:12.0pt;color:black">Agda <agda-bounces@lists.chalmers.se> on behalf of Ken Kubota <mail@kenkubota.de><br>
<b>Date: </b>Saturday, 14 March 2020 at 22:00<br>
<br>
</span></p>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Of course, encoding is not a self-purpose.</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">That all logical connectives can be defined in terms of the Sheffer stroke is coincidental and not of particular interest.</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">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).</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">In this concept, the reduction to certain primitive symbols is very natural and reveals the inner logic of high level notions.</p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">First of all it is important to realize that Type Theory in the sense of Church and HOL and Type Theory in the sense of Martin-Loef are some completely different ideas which are only superficially similar in that the share the word Type
and use lambda terms. </p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal" style="margin-bottom:12.0pt">Type Theory ala Martin-Loef (MLTT) was intended as a foundation of constructive Mathematics, while the systems you refer to are based on very strong classical assumptions. The idea that there should be any sort
of reduction from MLTT to Q0 or HOL is quite absurd. We understand reduction as explaining something, the notions you are used have no explanations from an intuitionistic point of view. This sort of reduction should be called complication, because it “reduces”
something I can understand to something I don’t.</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">It is important to distinguish two different kinds of high level notions:</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Those that can be reduced naturally to primitive symbols, and those which try to express metamathematical ideas (which seems to be your notion).</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">The latter shouldn't be implemented as primitive symbols in the basic formal language, but should be the result of metamathematical reasoning.</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
<p class="MsoNormal" style="margin-bottom:12.0pt">This is the game you are playing which seems to be some sort of glass pearl game to me. Modern type theory is quite close to basic mathematical intuitions and is based on organizing mathematical objects as types
– it makes only sense to talk about elements of types. Propositions do not arise as primitive concepts but they can be understood as types which carry no information. A predicate over a type A is a function P : A -> Prop, and proving that a predicate holds
universally is to exhibit an element of the Pi type: Pi x:A.P x. In this way Pi-types are not a “metamathematical notation” but they are the very base of understanding the meaning of quantification. However, Pi-types have more applications, for example we
can use it to give precise types to operations like matrix multiplication indexed by dimensions.</p>
<p class="MsoNormal">Type Theory also is very successful to work with structural Mathematics in the sense of category theory. Understanding this is at the core of Homotopy Type Theory. Type Theory by its very nature only allows structural operations, that is
we cannot observe encodings. The payback is in the univalence principle which basically says that structural equivalence (for example equivalence of categories) is equality. This notion of equality is a bit unusual in that equality in general is not a proposition
but a structure, i.e. there is usually more than one isomorphism between sets. I think there is a deep connection between the constructive and structural nature of type theory, even though classical Mathematicians may be more interested in the latter.</p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Lambda as the single variable binder in formulations of higher-order logic (Church, Andrews, Gordon) traditionally can be used to bind _term variables_ only.</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Type abstraction allows for binding _type variables_ also.</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">See <a href="https://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/">https://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/</a></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">and <a href="https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html">https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html</a></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Kevin Buzzard has (like Freek Wiedijk) correctly stated that current classical higher-order logic is too weak to express certain mathematical concepts.</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">The main reason is that the feature of type abstraction is missing.</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Gordon has suggested implementing this, but unfortunately this didn't happen in the current HOL systems (HOL4, HOL Light, Isabelle/HOL).</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Andrews and Melham did some work into this direction, but used the traditional quantifiers to bind type variables, not lambda.</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal" style="margin-bottom:12.0pt">In MLTT or HOTT, type quantification is handled via the notion of a universe U. Quantification over a universe is handled like quantification over any other type. So for example List is simple a function U ->
U, and a polymorphic function like reverse has a Pi type: Pi A : U, List U -> List U. Indeed here are 2 Pi-types at play here a dependent one Pi, and a non-dependent one -> which is a special case of the dependent one.</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">The formulation of the formal system depends on the purpose.</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Even within mathematics different formulations are required: <a href="https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/lArtWey5CQAJ">https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/lArtWey5CQAJ</a> (last
part on the two-step approach).</p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">However, from a logical (mathematical) point of view I do not see any need for constructivism.</p>
</div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
<p class="MsoNormal">We should strive to explain our notions, not just apply some formal reduction. Classical reasoning is based on the idea that mathematical objects behave like objects in the real world (actually maybe even the real world isn’t completely
classical if we take quantum theory into account). This seems quite preposterous because they are really constructions in our head and an absolute notion of truth isn’t really available here. However, it turns out this is also unnecessary: instead of appealing
to platonic truth we can just talk about evidence. That means a proposition is not something which is true or false, but a proposition is something you can have evidence for. The evidence can be expressed as a type and this is the core of the propositions
as types explanation (sometimes called Curry-Howard equivalence). Once you go with this you find that there is another, intuitively appealing way to do Mathematics which provides much more explanatory power. It also links well with computer science or more
generally with the need to link mathematical constructions to effective procedures.
</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">It is true that many main stream Mathematicians aren’t very concerned with intuitionism. Clearly this is a cultural phenomenon and to conclude that it should be so because it is so seems to be a fallacy. A good understanding of both classical
and constructive notions should be at the core of a decent mathematical education.
</p>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</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>