1834 lines
222 KiB
HTML
1834 lines
222 KiB
HTML
<!DOCTYPE html>
|
||
<html xmlns="http://www.w3.org/1999/xhtml">
|
||
<head>
|
||
<title>
|
||
soft question - What makes dependent type theory more suitable than set theory for proof assistants? - MathOverflow
|
||
</title>
|
||
<link rel="shortcut icon" href="https://cdn.sstatic.net/Sites/mathoverflow/Img/favicon.ico?v=8bbfe38cfc48" />
|
||
<link rel="apple-touch-icon" href="https://cdn.sstatic.net/Sites/mathoverflow/Img/apple-touch-icon.png?v=8c5ff8612fb4" />
|
||
<link rel="image_src" href="https://cdn.sstatic.net/Sites/mathoverflow/Img/apple-touch-icon.png?v=8c5ff8612fb4" />
|
||
<link rel="search" type="application/opensearchdescription+xml" title="MathOverflow" href="/opensearch.xml" />
|
||
<link rel="canonical" href="https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista" />
|
||
<meta name="viewport" content="width=device-width, height=device-height, initial-scale=1.0, minimum-scale=1.0" />
|
||
<meta property="og:type" content="website" />
|
||
<meta property="og:url" content="https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista" />
|
||
<meta property="og:site_name" content="MathOverflow" />
|
||
<meta property="og:image" itemprop="image primaryImageOfPage" content="https://cdn.sstatic.net/Sites/mathoverflow/Img/apple-touch-icon@2.png?v=f1c9606b77ff" />
|
||
<meta name="twitter:card" content="summary" />
|
||
<meta name="twitter:domain" content="mathoverflow.net" />
|
||
<meta name="twitter:title" property="og:title" itemprop="name" content="What makes dependent type theory more suitable than set theory for proof assistants?" />
|
||
<meta name="twitter:description" property="og:description" itemprop="description" content="In his talk, The Future of Mathematics, Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&amp;A part of the talk (at 1:00:00) he" />
|
||
<script src="https://rules.quantcount.com/rules-p-c1rF4kxgLUzNc.js" async="async"></script>
|
||
<script async="async" src="https://secure.quantserve.com/quant.js"></script>
|
||
<script async="async" src="https://sb.scorecardresearch.com/beacon.js"></script>
|
||
<script async="async" src="https://www.google-analytics.com/analytics.js"></script>
|
||
<script src="https://ajax.googleapis.com/ajax/libs/jquery/1.12.4/jquery.min.js"></script>
|
||
<script src="https://cdn.sstatic.net/Js/stub.en.js?v=a8e9c6b90096"></script>
|
||
<link rel="stylesheet" type="text/css" href="https://cdn.sstatic.net/Shared/stacks.css?v=8948ecab92be" />
|
||
<link rel="stylesheet" type="text/css" href="https://cdn.sstatic.net/Sites/mathoverflow/primary.css?v=39f584f0c70a" />
|
||
<link rel="alternate" type="application/atom+xml" title="Feed for question 'What makes dependent type theory more suitable than set theory for proof assistants?'" href="/feeds/question/376839" />
|
||
<script src="https://cdn.sstatic.net/Js/citation.en.js?v=4d26d4f9dd2d"></script>
|
||
<meta name="twitter:app:country" content="US" />
|
||
<meta name="twitter:app:name:iphone" content="Stack Exchange iOS" />
|
||
<meta name="twitter:app:id:iphone" content="871299723" />
|
||
<meta name="twitter:app:url:iphone" content="se-zaphod://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista" />
|
||
<meta name="twitter:app:name:ipad" content="Stack Exchange iOS" />
|
||
<meta name="twitter:app:id:ipad" content="871299723" />
|
||
<meta name="twitter:app:url:ipad" content="se-zaphod://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista" />
|
||
<meta name="twitter:app:name:googleplay" content="Stack Exchange Android" />
|
||
<meta name="twitter:app:url:googleplay" content="https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista" />
|
||
<meta name="twitter:app:id:googleplay" content="com.stackexchange.marvin" />
|
||
<script>
|
||
<![CDATA[
|
||
StackExchange.ready(function () {
|
||
|
||
StackExchange.using("postValidation", function () {
|
||
StackExchange.postValidation.initOnBlurAndSubmit($('#post-form'), 2, 'answer');
|
||
});
|
||
|
||
|
||
StackExchange.question.init({showCitation:true,showAnswerHelp:true,totalCommentCount:18,shownCommentCount:5,enableTables:true,questionId:376839});
|
||
|
||
styleCode();
|
||
|
||
StackExchange.realtime.subscribeToQuestion('504', '376839');
|
||
StackExchange.using("gps", function () { StackExchange.gps.trackOutboundClicks('#content', '.js-post-body'); });
|
||
|
||
|
||
|
||
});
|
||
]]>
|
||
</script>
|
||
<script src="https://cdn.sstatic.net/Js/third-party/citation-helper.js?v=2591ce444a3f"></script>
|
||
<script type="text/x-mathjax-config">
|
||
<![CDATA[
|
||
MathJax.Hub.Config({"HTML-CSS": { preferredFont: "TeX", availableFonts: ["STIX","TeX"], linebreaks: { automatic:true }, EqnChunk: (MathJax.Hub.Browser.isMobile ? 10 : 50) },
|
||
tex2jax: { inlineMath: [ ["$", "$"], ["\\\\(","\\\\)"] ], displayMath: [ ["$$","$$"], ["\\[", "\\]"] ], processEscapes: true, ignoreClass: "tex2jax_ignore|dno" },
|
||
TeX: {
|
||
extensions: ["begingroup.js"],
|
||
noUndefined: { attributes: { mathcolor: "red", mathbackground: "#FFEEEE", mathsize: "90%" } },
|
||
Macros: { href: "{}" }
|
||
},
|
||
messageStyle: "none",
|
||
styles: { ".MathJax_Display, .MathJax_Preview, .MathJax_Preview > *": { "background": "inherit" } },
|
||
SEEditor: "mathjaxEditing"
|
||
});
|
||
]]>
|
||
</script>
|
||
<script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-AMS_HTML-full"></script>
|
||
<script>
|
||
<![CDATA[
|
||
StackExchange.ready(function () {
|
||
StackExchange.realtime.init('wss://qa.sockets.stackexchange.com');
|
||
StackExchange.realtime.subscribeToReputationNotifications('504');
|
||
StackExchange.realtime.subscribeToTopBarNotifications('504');
|
||
});
|
||
]]>
|
||
</script>
|
||
<script>
|
||
<![CDATA[
|
||
StackExchange.init({"locale":"en","serverTime":1611597390,"routeName":"Questions/Show","stackAuthUrl":"https://stackauth.com","networkMetaHostname":"meta.stackexchange.com","site":{"name":"MathOverflow","description":"Q&A for professional mathematicians","isNoticesTabEnabled":true,"enableNewTagCreationWarning":true,"insertSpaceAfterNameTabCompletion":false,"id":504,"childUrl":"https://meta.mathoverflow.net","styleCodeWithHighlightjs":true,"negativeVoteScoreFloor":null,"enableSocialMediaInSharePopup":true,"protocol":"https"},"user":{"fkey":"b713db4a2d3569b28c42ae7fbe0bc879c2a8d81e5ce64b0a0527167c219c722e","tid":"05b15e7a-a00d-da9d-60b9-62599d25b08f","rep":0,"isAnonymous":true,"isAnonymousNetworkWide":true},"realtime":{"newest":true,"active":true,"tagged":true,"staleDisconnectIntervalInHours":0},"events":{"postType":{"question":1},"postEditionSection":{"title":1,"body":2,"tags":3}},"story":{"minCompleteBodyLength":75,"likedTagsMaxLength":300,"dislikedTagsMaxLength":300},"jobPreferences":{"maxNumDeveloperRoles":2,"maxNumIndustries":4},"svgIconPath":"https://cdn.sstatic.net/Img/stacks-icons","svgIconHash":"5acef7872715"}, {"userProfile":{},"userMessaging":{},"tags":{},"subscriptions":{"defaultMaxTrueUpSeats":1000},"snippets":{"renderDomain":"stacksnippets.net"},"slack":{"sidebarAdDismissCookie":"slack-sidebar-ad","sidebarAdDismissCookieExpirationDays":60.0},"site":{"allowImageUploads":true,"enableImgurHttps":true,"enableUserHovercards":true,"forceHttpsImages":true},"intercom":{"appId":"inf0secd","hostBaseUrl":"https://stacksnippets.net"},"paths":{},"monitoring":{"clientTimingsAbsoluteTimeout":30000,"clientTimingsDebounceTimeout":1000},"mentions":{"maxNumUsersInDropdown":50},"markdown":{"enableTables":true},"legal":{},"flags":{"allowRetractingCommentFlags":true,"allowRetractingFlags":true},"comments":{},"accounts":{"currentPasswordRequiredForChangingStackIdPassword":true}});
|
||
StackExchange.using.setCacheBreakers({"js/adops.en.js":"22a9bd59b1e9","js/ask.en.js":"e287ffdc77d4","js/begin-edit-event.en.js":"cb9965ad8784","js/events.en.js":"434ed06a5190","js/explore-qlist.en.js":"22610455f68f","js/full-anon.en.js":"b014785052d2","js/full.en.js":"64bcabe1c1a3","js/help.en.js":"e22359259ae0","js/highlightjs-loader.en.js":"0b11820a2ff7","js/inline-tag-editing.en.js":"e5a2bcfcd89d","js/keyboard-shortcuts.en.js":"e8896b87f465","js/markdown-it-loader.en.js":"ecbf27350e73","js/mobile.en.js":"7056b9b8b2a2","js/moderator.en.js":"836b418fa00f","js/postCollections-transpiled.en.js":"c3172f9c06f9","js/post-validation.en.js":"99aa0a63507b","js/prettify-full.en.js":"72e2caa4094c","js/question-editor.en.js":"","js/review.en.js":"30270478755b","js/review-v2-transpiled.en.js":"1484fb9d8cf5","js/revisions.en.js":"e411c9a83890","js/stacks-editor.en.js":"bc1197a9eeb8","js/tageditor.en.js":"40425ddd4257","js/tageditornew.en.js":"cee13c9fca52","js/tagsuggestions.en.js":"4e6582be0533","js/wmd.en.js":"89c7f80fe1ba","js/mathjax-editing.en.js":"3097c6d07c6c"});
|
||
StackExchange.using("gps", function() {
|
||
StackExchange.gps.init(true);
|
||
});
|
||
]]>
|
||
</script><noscript id="noscript-css">
|
||
<style>
|
||
<![CDATA[
|
||
body,.top-bar{margin-top:1.9em}
|
||
]]>
|
||
</style></noscript>
|
||
<script async="async" src="https://cdn.sstatic.net/Js/full-anon.en.js?v=b014785052d2"></script>
|
||
<script async="async" src="https://cdn.sstatic.net/Js/wmd.en.js?v=89c7f80fe1ba"></script>
|
||
<script async="async" src="https://cdn.sstatic.net/Js/post-validation.en.js?v=99aa0a63507b"></script>
|
||
</head>
|
||
<body class="question-page unified-theme">
|
||
<div id="notify-container"></div>
|
||
<header class="top-bar js-top-bar top-bar__network _fixed">
|
||
<div class="wmx12 mx-auto grid ai-center h100" role="menubar">
|
||
<div class="-main grid--cell">
|
||
<a href="#" class="-logo js-gps-track js-network-logo network-logo" data-gps-track="stack_exchange_popup.show" role="menuitem" aria-haspopup="true" aria-controls="topbar-network-logo-dialog" aria-expanded="false"><svg aria-hidden="true" class="native mtn1 svg-icon iconLogoSEAlternativeSm" width="107" height="15" viewbox="0 0 107 15">
|
||
<path d="M48.41 11.93l-1.96-3.2-1.04 1.16v2.04h-1.42V2.18h1.42v6.01L48.14 5h1.72l-2.44 2.7 2.74 4.22h-1.75zm-7.06.08c-1.59 0-3.14-.96-3.14-3.56s1.55-3.54 3.14-3.54c.97 0 1.65.27 2.31.97l-.97.93c-.44-.48-.79-.66-1.34-.66s-1 .22-1.3.62c-.31.38-.42.87-.42 1.68 0 .81.1 1.32.41 1.7.3.4.76.62 1.3.62.56 0 .9-.18 1.35-.66l.97.92c-.66.7-1.34.98-2.31.98zm-5.66-3.15h-1.65c-.83 0-1.26.37-1.26 1s.4.99 1.3.99c.53 0 .93-.04 1.3-.4.22-.2.31-.53.31-1.03v-.56zm.03 3.07v-.63c-.51.5-1 .71-1.87.71-.87 0-1.46-.2-1.89-.63a2.1 2.1 0 01-.55-1.49c0-1.16.82-2 2.42-2h1.86v-.5c0-.87-.44-1.3-1.54-1.3-.77 0-1.15.18-1.54.68l-.92-.86c.66-.77 1.35-1 2.52-1 1.93 0 2.9.8 2.9 2.38v4.64h-1.39zm-5.9 0c-1.32 0-1.93-.93-1.93-1.93V6.18h-.8V5.1h.8V3h1.41v2.1h1.36v1.07H29.3v3.75c0 .5.25.81.78.81h.58v1.2h-.85zm-6.33.08c-1.48 0-2.55-.34-3.49-1.28l1-.98c.72.72 1.51.94 2.52.94 1.3 0 2.04-.55 2.04-1.5 0-.42-.13-.78-.39-1.01-.25-.23-.5-.33-1.08-.41l-1.16-.17a3.4 3.4 0 01-1.88-.78 2.41 2.41 0 01-.72-1.86c0-1.7 1.25-2.86 3.3-2.86 1.3 0 2.22.33 3.07 1.1l-.96.94a2.92 2.92 0 00-2.15-.75c-1.16 0-1.8.65-1.8 1.52 0 .35.1.67.37.9.25.22.65.38 1.11.45l1.13.17c.91.13 1.42.35 1.84.72.54.47.8 1.17.8 2 0 1.8-1.48 2.86-3.55 2.86z" fill="#FEFEFE"></path>
|
||
<path d="M104.16 7.09c-.2-.42-.6-.74-1.2-.74s-.99.32-1.18.74c-.1.25-.15.44-.16.75h2.7a2 2 0 00-.16-.75zm-2.54 1.96c0 .9.56 1.57 1.55 1.57.78 0 1.16-.21 1.61-.66l1.08 1.04a3.4 3.4 0 01-2.7 1.11c-1.68 0-3.29-.76-3.29-3.62 0-2.3 1.26-3.6 3.1-3.6 1.97 0 3.1 1.44 3.1 3.37v.79h-4.45zm-5.48-2.57C95.1 6.48 95 7.37 95 8.3c0 .94.1 1.85 1.15 1.85 1.05 0 1.18-.91 1.18-1.85 0-.93-.13-1.82-1.18-1.82zm-.17 8.22c-1.1 0-1.84-.21-2.58-.92l1.1-1.11c.4.38.8.54 1.4.54 1.06 0 1.43-.74 1.43-1.46v-.72c-.47.51-1 .7-1.7.7-.69 0-1.29-.23-1.68-.62-.67-.66-.73-1.57-.73-2.8 0-1.24.06-2.13.73-2.8.4-.39 1-.62 1.7-.62.75 0 1.24.2 1.73.75v-.67h1.72v6.8c0 1.7-1.21 2.93-3.12 2.93zm-5.76-2.67V7.76c0-.96-.61-1.28-1.17-1.28-.56 0-1.18.32-1.18 1.28v4.27h-1.78V4.97h1.73v.65a2.44 2.44 0 011.78-.73c.7 0 1.28.23 1.67.62.58.57.73 1.24.73 2v4.52H90.2zm-7.1-2.98h-1.4c-.64 0-1 .3-1 .8 0 .49.33.81 1.02.81.5 0 .8-.04 1.12-.34.2-.17.26-.46.26-.89v-.38zm.04 2.98v-.6c-.48.47-.93.67-1.74.67-.8 0-1.4-.2-1.82-.62-.38-.4-.58-.97-.58-1.59 0-1.12.77-2.05 2.42-2.05h1.68V7.5c0-.77-.38-1.11-1.32-1.11-.68 0-1 .16-1.37.58l-1.13-1.1c.7-.75 1.38-.97 2.57-.97 1.99 0 3.02.84 3.02 2.5v4.64h-1.73zm-6.93 0v-4.3c0-.94-.6-1.25-1.15-1.25-.56 0-1.15.32-1.15 1.24v4.31h-1.77V2.38h1.77v3.24a2.35 2.35 0 011.7-.73c1.56 0 2.38 1.08 2.38 2.57v4.57h-1.78zm-6.96.08c-1.42 0-3.18-.76-3.18-3.62 0-2.85 1.76-3.6 3.18-3.6.98 0 1.72.3 2.34.95l-1.2 1.2c-.36-.4-.68-.56-1.14-.56-.42 0-.75.14-1.01.46-.27.33-.4.8-.4 1.55s.13 1.24.4 1.58c.26.3.59.46 1 .46.47 0 .79-.16 1.15-.56l1.2 1.18c-.62.65-1.36.96-2.34.96zm-5.53-.08l-1.3-2.11-1.3 2.11H59l2.45-3.6-2.35-3.46h2.12L62.42 7l1.21-2.02h2.13L63.4 8.43l2.46 3.6h-2.13zm-11.75 0V2.06h6.6V3.8h-4.65v2.33h3.96v1.74h-3.96v2.42h4.65v1.74h-6.6z" fill="#2F96E8"></path>
|
||
<path d="M0 3c0-1.1.9-2 2-2h8a2 2 0 012 2H0z" fill="#8FD8F7"></path>
|
||
<path d="M12 10H0c0 1.1.9 2 2 2h5v3l3-3a2 2 0 002-2z" fill="#155397"></path>
|
||
<path fill="#46A2D9" d="M0 4h12v2H0z"></path>
|
||
<path fill="#2D6DB5" d="M0 7h12v2H0z"></path></svg></a>
|
||
</div>
|
||
<ol class="overflow-x-auto ml-auto -secondary grid ai-center list-reset h100 user-logged-out" role="presentation">
|
||
<li class="-item searchbar-trigger">
|
||
<a href="#" class="-link js-searchbar-trigger" role="button" aria-label="Search" aria-haspopup="true" aria-controls="search" title="Click to show search"><svg aria-hidden="true" class="svg-icon iconSearch" width="18" height="18" viewbox="0 0 18 18">
|
||
<path d="M18 16.5l-5.14-5.18h-.35a7 7 0 10-1.19 1.19v.35L16.5 18l1.5-1.5zM12 7A5 5 0 112 7a5 5 0 0110 0z"></path></svg></a>
|
||
</li>
|
||
<li class="-item inbox-button-item">
|
||
<a href="#" class="-link js-inbox-button" aria-label="Inbox" title="Recent inbox messages" role="menuitem" aria-haspopup="true" aria-expanded="false" data-unread-count="0"><svg aria-hidden="true" class="svg-icon iconInbox" width="20" height="18" viewbox="0 0 20 18">
|
||
<path d="M4.63 1h10.56a2 2 0 011.94 1.35L20 10.79V15a2 2 0 01-2 2H2a2 2 0 01-2-2v-4.21l2.78-8.44c.25-.8 1-1.36 1.85-1.35zm8.28 12l2-2h2.95l-2.44-7.32a1 1 0 00-.95-.68H5.35a1 1 0 00-.95.68L1.96 11h2.95l2 2h6z"></path></svg></a>
|
||
</li>
|
||
<li class="-item achievements-button-item">
|
||
<a href="#" class="-link js-achievements-button" data-unread-class="_highlighted-positive" aria-label="Achievements" title="Recent achievements: reputation, badges, and privileges earned" role="menuitem" aria-haspopup="true" aria-expanded="false" data-unread-count="0" data-lit-up="false"><svg aria-hidden="true" class="svg-icon iconAchievements" width="18" height="18" viewbox="0 0 18 18">
|
||
<path d="M15 2V1H3v1H0v4c0 1.6 1.4 3 3 3v1c.4 1.5 3 2.6 5 3v2H5s-1 1.5-1 2h10c0-.4-1-2-1-2h-3v-2c2-.4 4.6-1.5 5-3V9c1.6-.2 3-1.4 3-3V2h-3zM3 7c-.5 0-1-.5-1-1V4h1v3zm8.4 2.5L9 8 6.6 9.4l1-2.7L5 5h3l1-2.7L10 5h2.8l-2.3 1.8 1 2.7h-.1zM16 6c0 .5-.5 1-1 1V4h1v2z"></path></svg></a>
|
||
</li>
|
||
<li class="-item help-button-item">
|
||
<a href="#" class="-link js-help-button" title="Help Center and other resources" role="menuitem" aria-haspopup="true" aria-controls="topbar-help-dialog" data-ga="["top navigation","help menu click",null,null,null]"><svg aria-hidden="true" class="svg-icon iconHelp" width="18" height="18" viewbox="0 0 18 18">
|
||
<path d="M9 1a8 8 0 100 16A8 8 0 009 1zm.81 12.13c-.02.71-.55 1.15-1.24 1.13-.66-.02-1.17-.49-1.15-1.2.02-.72.56-1.18 1.22-1.16.7.03 1.2.51 1.17 1.23zM11.77 8c-.3.34-.65.65-1.02.91l-.53.37c-.26.2-.42.43-.5.69a4 4 0 00-.09.75c0 .05-.03.16-.18.16H7.88c-.16 0-.18-.1-.18-.15.03-.66.12-1.21.4-1.66.4-.49.88-.9 1.43-1.22.16-.12.28-.25.38-.39a1.34 1.34 0 00.02-1.71c-.24-.31-.51-.46-1.03-.46-.51 0-.8.26-1.02.6-.21.33-.18.73-.18 1.1H5.75c0-1.38.35-2.25 1.1-2.76.52-.35 1.17-.5 1.93-.5 1 0 1.79.18 2.49.71.64.5.98 1.18.98 2.12 0 .57-.2 1.05-.48 1.44z"></path></svg></a>
|
||
</li>
|
||
<li class="-item site-switcher-item">
|
||
<a href="https://stackexchange.com" class="-link js-site-switcher-button js-gps-track" data-gps-track="site_switcher.show" aria-label="Site switcher" title="A list of all 176 Stack Exchange sites" role="menuitem" aria-haspopup="true" aria-expanded="false" data-ga="["top navigation","stack exchange click",null,null,null]"><svg aria-hidden="true" class="svg-icon iconStackExchange" width="18" height="18" viewbox="0 0 18 18">
|
||
<path d="M15 1H3a2 2 0 00-2 2v2h16V3a2 2 0 00-2-2zM1 13c0 1.1.9 2 2 2h8v3l3-3h1a2 2 0 002-2v-2H1v2zm16-7H1v4h16V6z"></path></svg></a>
|
||
</li>
|
||
<li class="-ctas">
|
||
<a href="https://mathoverflow.net/users/login?ssrc=head&returnurl=https%3a%2f%2fmathoverflow.net%2fquestions%2f376839%2fwhat-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista" class="login-link s-btn s-btn__filled py8 js-gps-track" rel="nofollow" data-gps-track="login.click" data-ga="["top navigation","login button click",null,null,null]">Log in</a> <a href="https://mathoverflow.net/users/signup?ssrc=head&returnurl=https%3a%2f%2fmathoverflow.net%2fquestions%2f376839%2fwhat-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista" class="login-link s-btn s-btn__primary py8" rel="nofollow" data-ga="["sign up","Sign Up Navigation","Header",null,null]">Sign up</a>
|
||
</li>
|
||
</ol>
|
||
</div>
|
||
</header>
|
||
<script>
|
||
<![CDATA[
|
||
StackExchange.ready(function () { StackExchange.topbar.init(); });
|
||
StackExchange.scrollPadding.setPaddingTop(50, 10);
|
||
]]>
|
||
</script>
|
||
<div class="py24 bg-black-750 fc-black-200 sm:pt24 sm:pb24 ps-relative js-dismissable-hero">
|
||
<div class="px12 grid ai-center jc-center mx-auto wmx12 sm:fd-column">
|
||
<div class="grid--cell wmx3 fs-body2 mr64 md:mr32 sm:mr0 sm:ta-center sm:mr0 sm:ta-center">
|
||
<p>
|
||
MathOverflow is a question and answer site for professional mathematicians. It only takes a minute to sign up.
|
||
</p><a href="/users/signup?ssrc=hero&returnurl=https%3a%2f%2fmathoverflow.net%2fquestions%2f376839%2fwhat-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista" class="s-btn s-btn__primary">Sign up to join this community</a>
|
||
</div>
|
||
<div class="grid fd-column ai-center wmn3 sm:wmn-initial sm:mt32 hero-background">
|
||
<div class="grid ai-center mb24 sm:mb16">
|
||
<div class="grid--cell mr16">
|
||
<img width="31" src="https://cdn.sstatic.net/Img/hero/anonymousHeroQuestions.svg?v=748bfb046b78" />
|
||
</div>
|
||
<div class="grid--cell">
|
||
Anybody can ask a question
|
||
</div>
|
||
</div>
|
||
<div class="grid ai-center mb24 sm:mb16">
|
||
<div class="grid--cell mr16">
|
||
<img width="35" src="https://cdn.sstatic.net/Img/hero/anonymousHeroAnswers.svg?v=d5348b00eddc" />
|
||
</div>
|
||
<div class="grid--cell">
|
||
Anybody can answer
|
||
</div>
|
||
</div>
|
||
<div class="grid ai-center">
|
||
<div class="grid--cell mr16">
|
||
<img width="24" src="https://cdn.sstatic.net/Img/hero/anonymousHeroUpvote.svg?v=af2bb70d5d1b" />
|
||
</div>
|
||
<div class="grid--cell wmx2">
|
||
The best answers are voted up and rise to the top
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="grid--cell as-start md:ps-absolute t8 r8">
|
||
<button class="s-btn s-btn__muted p8 js-dismiss"><svg aria-hidden="true" class="svg-icon iconClear" width="18" height="18" viewbox="0 0 18 18">
|
||
<path d="M15 4.41L13.59 3 9 7.59 4.41 3 3 4.41 7.59 9 3 13.59 4.41 15 9 10.41 13.59 15 15 13.59 10.41 9 15 4.41z"></path></svg></button>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<script>
|
||
<![CDATA[
|
||
StackExchange.ready(function () {
|
||
StackExchange.Hero.init("nso", "a");
|
||
|
||
var location = 0;
|
||
if ($("body").hasClass("questions-page")) {
|
||
location = 1;
|
||
} else if ($("body").hasClass("question-page")) {
|
||
location = 1;
|
||
} else if ($("body").hasClass("faq-page")) {
|
||
location = 5;
|
||
} else if ($("body").hasClass("home-page")) {
|
||
location = 3;
|
||
}
|
||
|
||
$('.js-cta-button').click(function () {
|
||
StackExchange.using("gps", function () {
|
||
StackExchange.gps.track("hero.action", { hero_action_type: 'cta', location: location }, true);
|
||
});
|
||
});
|
||
|
||
// TODO: we should review the class names and whatnot in use here. Older heroes use id selectors, the newer
|
||
// sticky question hero on SO has a .js-dismiss class instead, but it's apparently not used anywhere...
|
||
// It's not great. Ideally we'd have a set of classes in the partials above that would correspond to
|
||
// the behaviours we want here in a more clear way.
|
||
|
||
// sticky question-page hero at the bottom of the page on SO
|
||
$('.js-dismiss').on('click', function () {
|
||
StackExchange.using("gps", function () {
|
||
StackExchange.gps.track("hero.action", { hero_action_type: "close", location: location }, true);
|
||
});
|
||
StackExchange.Hero.dismiss();
|
||
$(".js-dismissable-hero").fadeOut("fast");
|
||
});
|
||
});
|
||
]]>
|
||
</script>
|
||
<header class="site-header">
|
||
<div class="site-header--container">
|
||
<a class="site-header--link d-flex ai-center fs-headline1 fw-bold" href="https://mathoverflow.net"><img class="h-auto wmx100" src="https://cdn.sstatic.net/Sites/mathoverflow/Img/logo.svg?v=3a674b060adf" alt="MathOverflow" /></a>
|
||
</div>
|
||
</header>
|
||
<div class="container">
|
||
<div id="left-sidebar" data-is-here-when="md lg" class="left-sidebar js-pinned-left-sidebar ps-relative">
|
||
<div class="left-sidebar--sticky-container js-sticky-leftnav">
|
||
<nav role="navigation">
|
||
<ol class="nav-links">
|
||
<li class="">
|
||
<a href="/" class="pl8 js-gps-track nav-links--link" data-gps-track="top_nav.click({is_current:false, location:2, destination:8})">
|
||
<div class="grid ai-center">
|
||
<div class="grid--cell truncate">
|
||
Home
|
||
</div>
|
||
</div></a>
|
||
</li>
|
||
<li>
|
||
<ol class="nav-links">
|
||
<li class="youarehere">
|
||
<a id="nav-questions" href="/questions" class="pl8 js-gps-track nav-links--link" data-gps-track="top_nav.click({is_current:true, location:2, destination:1})">
|
||
<div class="grid ai-center">
|
||
<div class="grid--cell truncate">
|
||
Questions
|
||
</div>
|
||
</div></a>
|
||
</li>
|
||
<li class="">
|
||
<a id="nav-tags" href="/tags" class="pl8 js-gps-track nav-links--link" data-gps-track="top_nav.click({is_current:false, location:2, destination:2})">
|
||
<div class="grid ai-center">
|
||
<div class="grid--cell truncate">
|
||
Tags
|
||
</div>
|
||
</div></a>
|
||
</li>
|
||
<li class="">
|
||
<a id="nav-users" href="/users" class="pl8 js-gps-track nav-links--link" data-gps-track="top_nav.click({is_current:false, location:2, destination:3})">
|
||
<div class="grid ai-center">
|
||
<div class="grid--cell truncate">
|
||
Users
|
||
</div>
|
||
</div></a>
|
||
</li>
|
||
<li class="">
|
||
<a id="nav-unanswered" href="/unanswered" class="pl8 js-gps-track nav-links--link" data-gps-track="top_nav.click({is_current:false, location:2, destination:5})">
|
||
<div class="grid ai-center">
|
||
<div class="grid--cell truncate">
|
||
Unanswered
|
||
</div>
|
||
</div></a>
|
||
</li>
|
||
</ol>
|
||
</li>
|
||
</ol>
|
||
</nav>
|
||
</div>
|
||
</div>
|
||
<div id="content" class="">
|
||
<div itemprop="mainEntity" itemscope="itemscope" itemtype="https://schema.org/Question">
|
||
<div class="inner-content clearfix">
|
||
<div id="question-header" class="grid sm:fd-column">
|
||
<h1 itemprop="name" class="fs-headline1 ow-break-word mb8 grid--cell fl1">
|
||
<a href="/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista" class="question-hyperlink">What makes dependent type theory more suitable than set theory for proof assistants?</a>
|
||
</h1>
|
||
<div class="ml12 aside-cta grid--cell print:d-none sm:ml0 sm:mb12 sm:order-first sm:as-end">
|
||
<a href="/questions/ask" class="ws-nowrap s-btn s-btn__primary">Ask Question</a>
|
||
</div>
|
||
</div>
|
||
<div class="grid fw-wrap pb8 mb16 bb bc-black-075">
|
||
<div class="grid--cell ws-nowrap mr16 mb8" title="2020-11-19 04:59:57Z">
|
||
<span class="fc-light mr2">Asked</span> <time itemprop="dateCreated" datetime="2020-11-19T04:59:57">2 months ago</time>
|
||
</div>
|
||
<div class="grid--cell ws-nowrap mr16 mb8">
|
||
<span class="fc-light mr2">Active</span> <a href="?lastactivity" class="s-link s-link__inherit" title="2020-12-07 08:28:29Z">1 month ago</a>
|
||
</div>
|
||
<div class="grid--cell ws-nowrap mb8" title="Viewed 17,974 times">
|
||
<span class="fc-light mr2">Viewed</span> 18k times
|
||
</div>
|
||
</div>
|
||
<div id="mainbar" role="main" aria-label="question and answers">
|
||
<div class="question" data-questionid="376839" id="question">
|
||
<div class="post-layout">
|
||
<div class="votecell post-layout--left">
|
||
<div class="js-voting-container grid jc-center fd-column ai-stretch gs4 fc-black-200" data-post-id="376839">
|
||
<button class="js-vote-up-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Up vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-an62d709"><svg aria-hidden="true" class="m0 svg-icon iconArrowUpLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 26h32L18 10 2 26z"></path></svg></button>
|
||
<div class="js-vote-count grid--cell fc-black-500 fs-title grid fd-column ai-center" itemprop="upvoteCount" data-value="112">
|
||
112
|
||
</div><button class="js-vote-down-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Down vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-mzycofxc"><svg aria-hidden="true" class="m0 svg-icon iconArrowDownLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 10h32L18 26 2 10z"></path></svg></button> <button class="js-bookmark-btn s-btn s-btn__unset c-pointer py4 js-gps-track" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Bookmark (51)" data-selected-classes="fc-yellow-600" data-gps-track="post.click({ item: 1, priv: 0, post_type: 1 })" aria-describedby="--stacks-s-tooltip-ypukkb5u"><svg aria-hidden="true" class="svg-icon iconBookmark" width="18" height="18" viewbox="0 0 18 18">
|
||
<path d="M6 1a2 2 0 00-2 2v14l5-4 5 4V3a2 2 0 00-2-2H6zm3.9 3.83h2.9l-2.35 1.7.9 2.77L9 7.59l-2.35 1.7.9-2.76-2.35-1.7h2.9L9 2.06l.9 2.77z"></path></svg></button>
|
||
<div class="js-bookmark-count mt4" data-value="51">
|
||
<button class="js-bookmark-btn s-btn s-btn__unset c-pointer py4 js-gps-track" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Bookmark (51)" data-selected-classes="fc-yellow-600" data-gps-track="post.click({ item: 1, priv: 0, post_type: 1 })" aria-describedby="--stacks-s-tooltip-ypukkb5u">51</button>
|
||
</div><a class="js-post-issue grid--cell s-btn s-btn__unset c-pointer py6 mx-auto" href="/posts/376839/timeline" data-shortcut="T" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-label="Timeline" aria-describedby="--stacks-s-tooltip-69b8n23r"><svg aria-hidden="true" class="mln2 mr0 svg-icon iconHistory" width="19" height="18" viewbox="0 0 19 18">
|
||
<path d="M3 9a8 8 0 113.73 6.77L8.2 14.3A6 6 0 105 9l3.01-.01-4 4-4-4h3L3 9zm7-4h1.01L11 9.36l3.22 2.1-.6.93L10 10V5z"></path></svg></a>
|
||
</div>
|
||
</div>
|
||
<div class="postcell post-layout--right">
|
||
<div class="s-prose js-post-body" itemprop="text">
|
||
<p>
|
||
In his talk, <a href="https://www.youtube.com/watch?v=Dp-mQ3HxgDE" rel="noreferrer">The Future of Mathematics</a>, <a href="https://en.wikipedia.org/wiki/Kevin_Buzzard" rel="noreferrer">Dr. Kevin Buzzard</a> states that <a href="https://en.wikipedia.org/wiki/Lean_(proof_assistant)" rel="noreferrer">Lean</a> is the only existing proof assistant suitable for formalizing <em>all of math</em>. In the Q&A part of the talk (at <a href="https://www.youtube.com/watch?v=Dp-mQ3HxgDE#t=1h0m0s" rel="noreferrer">1:00:00</a>) he justifies this as follows:
|
||
</p>
|
||
<ul>
|
||
<li>Automation is very difficult with set theory
|
||
</li>
|
||
<li>Simple type theory is too simple
|
||
</li>
|
||
<li>Univalent type theory hasn't been successful in proof assistants
|
||
</li>
|
||
</ul>
|
||
<p>
|
||
My question is about the first of these: Why is automation very difficult with set theory (compared to dependent type theory)?
|
||
</p>
|
||
</div>
|
||
<div class="mt24 mb12">
|
||
<div class="post-taglist grid gs4 gsy fd-column">
|
||
<div class="grid ps-relative">
|
||
<a href="/questions/tagged/set-theory" class="post-tag js-gps-track" title="show questions tagged 'set-theory'" rel="tag">set-theory</a> <a href="/questions/tagged/soft-question" class="post-tag js-gps-track" title="show questions tagged 'soft-question'" rel="tag">soft-question</a> <a href="/questions/tagged/foundations" class="post-tag js-gps-track" title="show questions tagged 'foundations'" rel="tag">foundations</a> <a href="/questions/tagged/type-theory" class="post-tag js-gps-track" title="show questions tagged 'type-theory'" rel="tag">type-theory</a> <a href="/questions/tagged/proof-assistants" class="post-tag js-gps-track" title="show questions tagged 'proof-assistants'" rel="tag">proof-assistants</a>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="mb0">
|
||
<div class="mt16 grid gs8 gsy fw-wrap jc-end ai-start pt4 mb16">
|
||
<div class="grid--cell mr16 fl1 w96">
|
||
<div class="js-post-menu pt2" data-post-id="376839">
|
||
<div class="grid d-flex gs8 s-anchors s-anchors__muted fw-wrap">
|
||
<div class="grid--cell">
|
||
<a href="/q/376839" rel="nofollow" itemprop="url" class="js-share-link js-gps-track" title="Short permalink to this question" data-gps-track="post.click({ item: 2, priv: 0, post_type: 1 })" data-controller="se-share-sheet s-popover" data-se-share-sheet-title="Share a link to this question" data-se-share-sheet-subtitle="" data-se-share-sheet-post-type="question" data-se-share-sheet-social="facebook twitter" data-se-share-sheet-location="1" data-se-share-sheet-license-url="https%3a%2f%2fcreativecommons.org%2flicenses%2fby-sa%2f4.0%2f" data-se-share-sheet-license-name="CC BY-SA 4.0" data-s-popover-placement="bottom-start" aria-controls="se-share-sheet-0" data-action="s-popover#toggle se-share-sheet#preventNavigation s-popover:show->se-share-sheet#willShow s-popover:shown->se-share-sheet#didShow">Share</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" class="js-cite-link s-btn s-btn__link">Cite</button>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<a href="/posts/376839/edit" class="js-suggest-edit-post js-gps-track" data-gps-track="post.click({ item: 6, priv: 0, post_type: 1 })" title="">Improve this question</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" id="btnFollowPost-376839" class="s-btn s-btn__link js-follow-post js-follow-question js-gps-track" data-gps-track="post.click({ item: 14, priv: 0, post_type: 1 })" data-controller="s-tooltip" data-s-tooltip-placement="bottom" data-s-popover-placement="bottom" aria-controls="" aria-describedby="--stacks-s-tooltip-zwqvh1gx">Follow</button>
|
||
</div>
|
||
</div>
|
||
<div class="js-menu-popup-container"></div>
|
||
</div>
|
||
</div>
|
||
<div class="post-signature grid--cell">
|
||
<div class="user-info">
|
||
<div class="user-action-time">
|
||
<a href="/posts/376839/revisions" title="show all edits to this post" class="js-gps-track" data-gps-track="post.click({ item: 4, priv: 0, post_type: 1 })">edited <span title="2020-11-19 17:58:27Z" class="relativetime">Nov 19 '20 at 17:58</span></a>
|
||
</div>
|
||
<div class="user-gravatar32">
|
||
<a href="/users/2383/lspice">
|
||
<div class="gravatar-wrapper-32">
|
||
<img src="https://www.gravatar.com/avatar/0b931d02ad4238ed1e4d83225a328eba?s=32&d=identicon&r=PG" alt="" width="32" height="32" class="bar-sm" />
|
||
</div></a>
|
||
</div>
|
||
<div class="user-details">
|
||
<a href="/users/2383/lspice">LSpice</a>
|
||
<div class="-flair">
|
||
<span class="reputation-score" title="reputation score " dir="ltr">5,123</span><span title="3 gold badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">3</span></span><span class="v-visible-sr">3 gold badges</span><span title="31 silver badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">31</span></span><span class="v-visible-sr">31 silver badges</span><span title="41 bronze badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">41</span></span><span class="v-visible-sr">41 bronze badges</span>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="post-signature owner grid--cell">
|
||
<div class="user-info">
|
||
<div class="user-action-time">
|
||
asked <span title="2020-11-19 04:59:57Z" class="relativetime">Nov 19 '20 at 4:59</span>
|
||
</div>
|
||
<div class="user-gravatar32">
|
||
<a href="/users/30352/max">
|
||
<div class="gravatar-wrapper-32">
|
||
<img src="https://www.gravatar.com/avatar/0e6e8e830fa6930fce56c3ada5d4a1f2?s=32&d=identicon&r=PG" alt="" width="32" height="32" class="bar-sm" />
|
||
</div></a>
|
||
</div>
|
||
<div class="user-details" itemprop="author" itemscope="itemscope" itemtype="https://schema.org/Person">
|
||
<a href="/users/30352/max">Max</a>
|
||
<div class="-flair">
|
||
<span class="reputation-score" title="reputation score " dir="ltr">1,197</span><span title="2 gold badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">2</span></span><span class="v-visible-sr">2 gold badges</span><span title="8 silver badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">8</span></span><span class="v-visible-sr">8 silver badges</span><span title="17 bronze badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">17</span></span><span class="v-visible-sr">17 bronze badges</span>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="post-layout--right">
|
||
<div id="comments-376839" class="comments js-comments-container bt bc-black-075 mt12" data-post-id="376839" data-min-length="15">
|
||
<ul class="comments-list js-comments-list" data-remaining-comments-count="13" data-canpost="false" data-cansee="true" data-comments-unavailable="false" data-addlink-disabled="true">
|
||
<li id="comment-955833" class="comment js-comment" data-comment-id="955833">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">5</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">@YCor: People who are trying to push their agenda, will usually try to minimise other things. At least "in broad strokes" parts of their agenda... (I'm not accusing Kevin of being unethical, I'm just offering an explanation: if you want people to use Lean and follow your philosophical agenda, it's usually counterproductive to say "Actually set theory is great and you should study it, or at least use Coq for a year or two, before coming to use Lean"...)</span> – <a href="/users/7206/asaf-karagila" title="31,650 reputation" class="comment-user">Asaf Karagila</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment955833_376839"><span title="2020-11-19 17:18:08Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 19 '20 at 17:18</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-955972" class="comment js-comment" data-comment-id="955972">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">5</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">I hope Buzzard joins the discussion. But one thing I found strange is this mention of "chaps" around Voevodsky who haven't done anything with Coq except formalize rings and modules. Did I hear that correctly? It sounded really misleading. Clearly there are extensive libraries of math formalized by Coq; for example, the formalization of the odd order theorem (finite groups of odd order are solvable) by Gonthier et al. was one such tour de force, although not necessarily one developed by the "Voevodsky chaps".</span> – <a href="/users/2926/todd-trimble" title="48,628 reputation" class="comment-user">Todd Trimble<span class="mod-flair" title="moderator">♦</span></a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment955972_376839"><span title="2020-11-20 02:29:03Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 2:29</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956085" class="comment js-comment" data-comment-id="956085">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="supernova">30</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">Let me state, once again, that I thoroughly regret bad-mouthing Coq in a talk which I had no idea would go "viral" to the extent that it has.</span> – <a href="/users/1384/kevin-buzzard" title="37,243 reputation" class="comment-user">Kevin Buzzard</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956085_376839"><span title="2020-11-20 13:50:28Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 13:50</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956129" class="comment js-comment" data-comment-id="956129">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="hot">15</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">Yes, this summarises it well! I have given 20+ talks on this stuff now, and some get recorded, but somehow this one talk went crazy and I completely inadvertantly upset a bunch of Coq users. I do have strong opinions about what is good and bad about the Coq ecosystem but I do a poor job of summarising them in the talk. I have posted far more well-thought-out comments elsewhere (e.g. on the Coq Zulip) but nothing gets the traction of this talk.</span> – <a href="/users/1384/kevin-buzzard" title="37,243 reputation" class="comment-user">Kevin Buzzard</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956129_376839"><span title="2020-11-20 15:32:17Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 15:32</span></a></span> <span title="this comment was edited 1 time"><svg aria-hidden="true" class="va-text-bottom o50 svg-icon iconPencilSm" width="14" height="14" viewbox="0 0 14 14">
|
||
<path d="M11.1 1.71l1.13 1.12c.2.2.2.51 0 .71L11.1 4.7 9.21 2.86l1.17-1.15c.2-.2.51-.2.71 0zM2 10.12l6.37-6.43 1.88 1.88L3.88 12H2v-1.88z"></path></svg></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956237" class="comment js-comment" data-comment-id="956237">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">8</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">@KevinBuzzard In addition to David and Christopher's points, which are largely correct, many people working on HoTT/UF are just not <i>interested</i> in simply formalizing known facts but are more interested in pushing the boundaries. Also there are a lot fewer of us than there are people working in ordinary Coq, and furthermore UniMath is just one project while others like <a href="https://github.com/HoTT/HoTT" rel="nofollow noreferrer">HoTT/HoTT</a> have no objection to using all the features of Coq.</span> – <a href="/users/49/mike-shulman" title="51,944 reputation" class="comment-user">Mike Shulman</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956237_376839"><span title="2020-11-20 22:18:01Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 22:18</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
</ul>
|
||
</div>
|
||
<div id="comments-link-376839" data-rep="50" data-anon="true">
|
||
<a class="js-show-link comments-link" title="expand to show all comments on this post" href="#" onclick="" role="button">show <b>13</b> more comments</a>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div id="answers">
|
||
<a name="tab-top" id="tab-top"></a>
|
||
<div id="answers-header">
|
||
<div class="answers-subheader grid ai-center mb8">
|
||
<div class="grid--cell fl1">
|
||
<h2 class="mb0" data-answercount="5">
|
||
5 Answers
|
||
</h2>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<div class="grid s-btn-group js-filter-btn">
|
||
<a class="grid--cell s-btn s-btn__muted s-btn__outlined" href="/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista?answertab=active#tab-top" data-nav-xhref="" title="Answers with the latest activity first" data-value="active" data-shortcut="A">Active</a> <a class="grid--cell s-btn s-btn__muted s-btn__outlined" href="/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista?answertab=oldest#tab-top" data-nav-xhref="" title="Answers in the order they were provided" data-value="oldest" data-shortcut="O">Oldest</a> <a class="youarehere is-selected grid--cell s-btn s-btn__muted s-btn__outlined" href="/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista?answertab=votes#tab-top" data-nav-xhref="" title="Answers with the highest score first" data-value="votes" data-shortcut="V">Votes</a>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div><a name="376973" id="376973"></a>
|
||
<div id="answer-376973" class="answer accepted-answer" data-answerid="376973" itemprop="acceptedAnswer" itemscope="itemscope" itemtype="https://schema.org/Answer">
|
||
<div class="post-layout">
|
||
<div class="votecell post-layout--left">
|
||
<div class="js-voting-container grid jc-center fd-column ai-stretch gs4 fc-black-200" data-post-id="376973">
|
||
<button class="js-vote-up-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Up vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-gf0puagf"><svg aria-hidden="true" class="m0 svg-icon iconArrowUpLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 26h32L18 10 2 26z"></path></svg></button>
|
||
<div class="js-vote-count grid--cell fc-black-500 fs-title grid fd-column ai-center" itemprop="upvoteCount" data-value="184">
|
||
184
|
||
</div><button class="js-vote-down-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Down vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-f7nziqix"><svg aria-hidden="true" class="m0 svg-icon iconArrowDownLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 10h32L18 26 2 10z"></path></svg></button>
|
||
<div class="js-accepted-answer-indicator grid--cell fc-green-500 py6 mtn8" data-s-tooltip-placement="right" title="Loading when this answer was accepted…" tabindex="0" role="note" aria-label="Accepted">
|
||
<div class="ta-center">
|
||
<svg aria-hidden="true" class="svg-icon iconCheckmarkLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M6 14l8 8L30 6v8L14 30l-8-8v-8z"></path></svg>
|
||
</div>
|
||
</div><a class="js-post-issue grid--cell s-btn s-btn__unset c-pointer py6 mx-auto" href="/posts/376973/timeline" data-shortcut="T" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-label="Timeline" aria-describedby="--stacks-s-tooltip-wqazr074"><svg aria-hidden="true" class="mln2 mr0 svg-icon iconHistory" width="19" height="18" viewbox="0 0 19 18">
|
||
<path d="M3 9a8 8 0 113.73 6.77L8.2 14.3A6 6 0 105 9l3.01-.01-4 4-4-4h3L3 9zm7-4h1.01L11 9.36l3.22 2.1-.6.93L10 10V5z"></path></svg></a>
|
||
</div>
|
||
</div>
|
||
<div class="answercell post-layout--right">
|
||
<div class="s-prose js-post-body" itemprop="text">
|
||
<p>
|
||
I apologize for writing a lengthy answer, but I get the feeling the discussions about foundations for formalized mathematics are often hindered by lack of information.
|
||
</p>
|
||
<p>
|
||
I have used proof assistants for a while now, and also worked on their design and implementation. While I will be quick to tell jokes about set theory, I am bitterly aware of the shortcomings of type theory, very likely more so than the typical set theorist. (Ha, ha, "typical set theorist"!) If anyone can show me how to improve proof assistants with set theory, I will be absolutely deligthed! But it is not enough to just have good ideas – you need to test them in practice on large projects, as many phenomena related to formalized mathematics only appear once we reach a certain level of complexity.
|
||
</p>
|
||
<h3>
|
||
The components of a proof assistant
|
||
</h3>
|
||
<p>
|
||
The architecture of modern proof assistants is the result of several decades of experimentation, development and practical experience. A proof assistant incorporates not one, but several formal systems.
|
||
</p>
|
||
<p>
|
||
The central component of a proof assistant is the <strong>kernel</strong>, which validates every inference step and makes sure that proofs are correct. It does so by implementing a formal system <span class="math-container">$F$</span> (the <strong>foundation</strong>) which is expressive enough to allow formalization of a large amount of mathematics, but also simple enough to allow an efficient and correct implementation.
|
||
</p>
|
||
<p>
|
||
The foundational system implemented in the kernel is too rudimentary to be directly usable for sophisticated mathematics. Instead, the user writes their input in a more expressive formal language <span class="math-container">$V$</span> (the <strong>vernacular</strong>) that is designed to be practical and useful. Typically <span class="math-container">$V$</span> is quite complex so that it can accommodate various notational conventions and other accepted forms of mathematical expression. A second component of the proof assistant, the <strong>elaborator</strong>, translates <span class="math-container">$V$</span> to <span class="math-container">$F$</span> and passes the translations to the kernel for verification.
|
||
</p>
|
||
<p>
|
||
A proof assistant may incorporate a third formal language <span class="math-container">$M$</span> (the <strong>meta-language</strong>), which is used to implement proof search, decision procedures, and other automation techniques. Because the purpose of <span class="math-container">$M$</span> is to implement algorithms, it typically resembles a programming language. The distinction between <span class="math-container">$M$</span> and <span class="math-container">$V$</span> may not be very sharp, and sometimes they are combined into a single formalism. From mathematical point of view, <span class="math-container">$M$</span> is less interesting than <span class="math-container">$F$</span> and <span class="math-container">$V$</span>, so we shall ignore it.
|
||
</p>
|
||
<h3>
|
||
Suitability of foundation <span class="math-container">$F$</span>
|
||
</h3>
|
||
<p>
|
||
The correctness of the entire system depends on the correctness of the kernel. A bug in the kernel allows invalid proofs to be accepted, whereas a bug in any other component is just an annoyance. Therefore, the foundation <span class="math-container">$F$</span> should be simple so that we can implement it reliably. It should not be so exotic that logicians cannot tell how it relates to the accepted foundations of mathematics. Computers are fast, so it does not matter (too much) if the translation from <span class="math-container">$V$</span> to <span class="math-container">$F$</span> creates verbose statements. Also, <span class="math-container">$F$</span> need not be directly usable by humans.
|
||
</p>
|
||
<p>
|
||
A suitable variant of set theory or type theory fits these criteria. Indeed Mizar is based on set theory, while HOL, Lean, Coq, and Agda use type theory in the kernel. Since both set theory and type theory are mathematically very well understood, and more or less equally expressive, the choice will hinge on technical criteria, such as availability and efficiency of proof-checking algorithms.
|
||
</p>
|
||
<h3>
|
||
Suitability of vernacular <span class="math-container">$V$</span>
|
||
</h3>
|
||
<p>
|
||
A much more interesting question is what makes the vernacular <span class="math-container">$V$</span> suitable.
|
||
</p>
|
||
<p>
|
||
For the vernacular to be useful, it has to reflect mathematical practice as much as possible. It should allow expression of mathematical ideas and concepts directly in familiar terms, and without unnecessary formalistic hassle. On the other hand, <span class="math-container">$V$</span> should be a formal language so that the elaborator can translate it to the foundation <span class="math-container">$F$</span>.
|
||
</p>
|
||
<p>
|
||
To learn more about what makes <span class="math-container">$V$</span> good, we need to carefully observe how mathematicians <em>actually</em> write mathematics. They produce <a href="http://hott.github.io/HoTT/dependencies/HoTTCore.svg" rel="noreferrer">complex webs</a> of definitions, theorems, and constructions, therefore <span class="math-container">$V$</span> should support <em>management</em> of large collections of formalized mathematics. In this regards we can learn a great deal by looking at how programmers organize software. For instance, saying that a body of mathematics is "just a series of definitions, theorems and proofs" is a naive idealization that works in certain contexts, but certainly not in practical formalization of mathematics.
|
||
</p>
|
||
<p>
|
||
Mathematicians omit a great deal of information in their writings, and are quite willing to sacrifice formal correctness for succinctness. The reader is expected to fill in the missing details, and to rectify the imprecisions. The proof assistant is expected to do the same. To illustrate this point, consider the following snippet of mathematical text:
|
||
</p>
|
||
<blockquote>
|
||
<p>
|
||
Let <span class="math-container">$U$</span> and <span class="math-container">$V$</span> be vector spaces and <span class="math-container">$f : U \to V$</span> a linear map. Then <span class="math-container">$f(2 \cdot x + y) = 2 \cdot f(x) + f(y)$</span> for all <span class="math-container">$x$</span> and <span class="math-container">$y$</span>.
|
||
</p>
|
||
</blockquote>
|
||
<p>
|
||
Did you understand it? Of course. But you might be quite surprised to learn how much guesswork and correction your brain carried out:
|
||
</p>
|
||
<ul>
|
||
<li>
|
||
<p>
|
||
The field of scalars is not specified, but this does not prevent you from understanding the text. You simply assumed that there is some underlying field of scalars <span class="math-container">$K$</span>. You might find out more about <span class="math-container">$K$</span> in subsequent text. (<span class="math-container">$K$</span> is an <a href="https://coq.inria.fr/refman/language/extensions/evars.html" rel="noreferrer">existential variable</a>.)
|
||
</p>
|
||
</li>
|
||
<li>
|
||
<p>
|
||
Strictly speaking "<span class="math-container">$f : U \to V$</span>" does not make sense because <span class="math-container">$U$</span> and <span class="math-container">$V$</span> are not sets, but structures <span class="math-container">$U = (|U|, 0_U, {+}_U, {-}_U, {\cdot}_U)$</span> and <span class="math-container">$V = (|V|, 0_V, {+}_V, {-}_V, {\cdot}_V)$</span>. Of course, you correctly surmised that <span class="math-container">$f$</span> is a map between the <em>carriers</em>, i.e., <span class="math-container">$f : |U| \to |V|$</span>. (You inserted an <a href="https://coq.inria.fr/distrib/current/refman/addendum/implicit-coercions.html" rel="noreferrer">implicit coercion</a> from a vector space to its carrier.)
|
||
</p>
|
||
</li>
|
||
<li>
|
||
<p>
|
||
What do <span class="math-container">$x$</span> and <span class="math-container">$y$</span> range over? For <span class="math-container">$f(x)$</span> and <span class="math-container">$f(y)$</span> to make sense, it must be the case that <span class="math-container">$x \in |U|$</span> and <span class="math-container">$y \in |U|$</span>. (You <a href="https://en.wikipedia.org/wiki/Type_inference" rel="noreferrer">inferred</a> the domain of <span class="math-container">$x$</span> and <span class="math-container">$y$</span>.)
|
||
</p>
|
||
</li>
|
||
<li>
|
||
<p>
|
||
In the equation, <span class="math-container">$+$</span> on the left-hand side means <span class="math-container">$+_{U}$</span>, and <span class="math-container">$+$</span> on the right-hand side <span class="math-container">${+}_V$</span>, and similarly for scalar multiplication. (You reconstructed the <a href="https://coq.inria.fr/refman/language/extensions/implicit-arguments.html" rel="noreferrer">implicit arguments</a> of <span class="math-container">$+$</span>.)
|
||
</p>
|
||
</li>
|
||
<li>
|
||
<p>
|
||
The symbol <span class="math-container">$2$</span> normally denotes a natural number, as every child knows, but clearly it is meant to denote the scalar <span class="math-container">$1_K +_K 1_K$</span>. (You interpreed "<span class="math-container">$2$</span>" in the <a href="https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#notation-scopes" rel="noreferrer">notation scope</a> appropriate for the situation at hand.)
|
||
</p>
|
||
</li>
|
||
</ul>
|
||
<p>
|
||
The vernacular <span class="math-container">$V$</span> must support these techniques, and many more, so that they can be implemented in the elaborator. It cannot be anything as simple as ZFC with first-order logic and definitional extensions, or bare Martin-Löf type theory. You may consider the development of <span class="math-container">$V$</span> to be outside of scope of mathematics and logic, but then do not complain when computer scientist fashion it after their technology.
|
||
</p>
|
||
<p>
|
||
I have never seen any serious proposals for a vernacular based on set theory. Or to put it another way, as soon as we start expanding and transforming set theory to fit the requirements for <span class="math-container">$V$</span>, we end up with a theoretical framework that looks a lot like type theory. (You may entertain yourself by thinking how set theory could be used to detect that <span class="math-container">$f : U \to V$</span> above does not make sense unless we insert coercions – for if everthying is a set then so are <span class="math-container">$U$</span> and <span class="math-container">$V$</span>, in which case <span class="math-container">$f : U \to V$</span> <em>does</em> make sense.)
|
||
</p>
|
||
<h3>
|
||
Detecting mistakes
|
||
</h3>
|
||
<p>
|
||
An important aspect of suitability of foundation is its ability to detect mistakes. Of course, its purpose is to prevent logical errors, but there is more to mistakes than just violation of logic. There are formally meaningful statements which, with very high probability, are mistakes. Consider the following snippet, and read it carefully:
|
||
</p>
|
||
<blockquote>
|
||
<p>
|
||
<strong>Definition:</strong> A set <span class="math-container">$X$</span> is <em>jaberwocky</em> when for every <span class="math-container">$x \in X$</span> there exists a bryllyg <span class="math-container">$U \subseteq X$</span> and an uffish <span class="math-container">$K \subseteq X$</span> such that <span class="math-container">$x \in U$</span> and <span class="math-container">$U \in K$</span>.
|
||
</p>
|
||
</blockquote>
|
||
<p>
|
||
Even if you have never read Lewis Carroll's works, you should wonder about "<span class="math-container">$U \in K$</span>". It looks like "<span class="math-container">$U \subseteq K$</span>" would make more sense, since <span class="math-container">$U$</span> and <span class="math-container">$K$</span> are both subsets of <span class="math-container">$X$</span>. Nevertheless, a proof assistant whose foundation <span class="math-container">$F$</span> is based on ZFC will accept the above definition as valid, even though it is very unlikely that the human intended it.
|
||
</p>
|
||
<p>
|
||
A proof assistant based on type theory would reject the definition by stating that "<span class="math-container">$U \in K$</span>" is a type error.
|
||
</p>
|
||
<p>
|
||
So suppose we use a set-theoretic foundation <span class="math-container">$F$</span> that accepts any syntactically valid formula as meaningful. In such a system writing "<span class="math-container">$U \in K$</span>" is meaningful and therefore the above definition will be accepted by the kernel. If we want the proof assistant to actually <em>assist</em> the human, it has to contain an additional mechanism that will flag "<span class="math-container">$U \in K$</span>" as suspect, despite the kernel being happy with it. But what is this additional mechanism, if not just a second kernel based on type theory?
|
||
</p>
|
||
<p>
|
||
I am not saying that it is impossible to design a proof assistant based on set theory. After all, <a href="http://mizar.org" rel="noreferrer">Mizar</a>, the most venerable of them all, is designed precisely in this way – set theory with a layer of type-theoretic mechanisms on top. But I cannot help to wonder: why bother with the set-theoretic kernel that requires a type-theoretic fence to insulate the user from the unintended permissiveness of set theory?
|
||
</p>
|
||
</div>
|
||
<div class="mt24">
|
||
<div class="grid fw-wrap ai-start jc-end gs8 gsy">
|
||
<div class="grid--cell mr16" style="flex: 1 1 100px;">
|
||
<div class="js-post-menu pt2" data-post-id="376973">
|
||
<div class="grid d-flex gs8 s-anchors s-anchors__muted fw-wrap">
|
||
<div class="grid--cell">
|
||
<a href="/a/376973" rel="nofollow" itemprop="url" class="js-share-link js-gps-track" title="Short permalink to this answer" data-gps-track="post.click({ item: 2, priv: 0, post_type: 2 })" data-controller="se-share-sheet s-popover" data-se-share-sheet-title="Share a link to this answer" data-se-share-sheet-subtitle="" data-se-share-sheet-post-type="answer" data-se-share-sheet-social="facebook twitter" data-se-share-sheet-location="2" data-se-share-sheet-license-url="https%3a%2f%2fcreativecommons.org%2flicenses%2fby-sa%2f4.0%2f" data-se-share-sheet-license-name="CC BY-SA 4.0" data-s-popover-placement="bottom-start" aria-controls="se-share-sheet-1" data-action="s-popover#toggle se-share-sheet#preventNavigation s-popover:show->se-share-sheet#willShow s-popover:shown->se-share-sheet#didShow">Share</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" class="js-cite-link s-btn s-btn__link">Cite</button>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<a href="/posts/376973/edit" class="js-suggest-edit-post js-gps-track" data-gps-track="post.click({ item: 6, priv: 0, post_type: 2 })" title="">Improve this answer</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" id="btnFollowPost-376973" class="s-btn s-btn__link js-follow-post js-follow-answer js-gps-track" data-gps-track="post.click({ item: 14, priv: 0, post_type: 2 })" data-controller="s-tooltip" data-s-tooltip-placement="bottom" data-s-popover-placement="bottom" aria-controls="" aria-describedby="--stacks-s-tooltip-5kruejcy">Follow</button>
|
||
</div>
|
||
</div>
|
||
<div class="js-menu-popup-container"></div>
|
||
</div>
|
||
</div>
|
||
<div class="post-signature grid--cell fl0">
|
||
<div class="user-info">
|
||
<div class="user-action-time">
|
||
<a href="/posts/376973/revisions" title="show all edits to this post" class="js-gps-track" data-gps-track="post.click({ item: 4, priv: 0, post_type: 2 })">edited <span title="2020-12-07 08:28:29Z" class="relativetime">Dec 7 '20 at 8:28</span></a>
|
||
</div>
|
||
<div class="user-gravatar32"></div>
|
||
<div class="user-details">
|
||
<div class="-flair"></div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="post-signature grid--cell fl0">
|
||
<div class="user-info user-hover">
|
||
<div class="user-action-time">
|
||
answered <span title="2020-11-20 12:02:43Z" class="relativetime">Nov 20 '20 at 12:02</span>
|
||
</div>
|
||
<div class="user-gravatar32">
|
||
<a href="/users/1176/andrej-bauer">
|
||
<div class="gravatar-wrapper-32">
|
||
<img src="https://www.gravatar.com/avatar/59d57d95bc7c45ced5f1969279cec06b?s=32&d=identicon&r=PG" alt="" width="32" height="32" class="bar-sm" />
|
||
</div></a>
|
||
</div>
|
||
<div class="user-details" itemprop="author" itemscope="itemscope" itemtype="https://schema.org/Person">
|
||
<a href="/users/1176/andrej-bauer">Andrej Bauer</a>
|
||
<div class="-flair">
|
||
<span class="reputation-score" title="reputation score 40,035" dir="ltr">40k</span><span title="9 gold badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">9</span></span><span class="v-visible-sr">9 gold badges</span><span title="102 silver badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">102</span></span><span class="v-visible-sr">102 silver badges</span><span title="193 bronze badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">193</span></span><span class="v-visible-sr">193 bronze badges</span>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="post-layout--right">
|
||
<div id="comments-376973" class="comments js-comments-container bt bc-black-075 mt12" data-post-id="376973" data-min-length="15">
|
||
<ul class="comments-list js-comments-list" data-remaining-comments-count="27" data-canpost="false" data-cansee="true" data-comments-unavailable="false" data-addlink-disabled="true">
|
||
<li id="comment-956078" class="comment js-comment" data-comment-id="956078">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">5</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">Very informative answer! But I don't understand the remark that "a proof assistant whose foundation $F$ is based on ZFC will accept the above definition as valid." Whether it gets accepted depends on the vernacular rather than the foundation, doesn't it? What's to stop someone from building a vernacular that is similar to type theory on top of a set-theoretic foundation? That seems to be the natural thing to do if we want to be able to calibrate logical strength in terms of set-theoretic axioms but want the advantages of type theory in the human interface.</span> – <a href="/users/3106/timothy-chow" title="54,451 reputation" class="comment-user">Timothy Chow</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956078_376973"><span title="2020-11-20 13:15:56Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 13:15</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956176" class="comment js-comment" data-comment-id="956176">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="cool">4</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">@TimothyChow Metamath in particular was designed with this use case in mind; the tool reports what axioms any particular theorem depends on, and there are a lot of redundant axioms specifically so that you can prove a theorem with the minimum axiomatic strength for which it holds; since the entire library is written that way you can both find out if a given proof is in ZF-replacement, and also a nontrivial fraction of theorems are in fact in that subset.</span> – <a href="/users/34444/mario-carneiro" title="1,002 reputation" class="comment-user">Mario Carneiro</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956176_376973"><span title="2020-11-20 18:28:32Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 18:28</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956218" class="comment js-comment" data-comment-id="956218">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">13</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">This is a really fantastic answer, MathOverflow at its best. Two questions/objections, though: (1) "A bug in the kernel allows invalid proofs to be accepted, whereas a bug in any other component is just an annoyance": what about a bug in the elaborator? Couldn't that be catastrophic too? (2) I see no implicit coercion in "let $U$ and $V$ be vector spaces and $f: U \to V$ a linear map". As a category theorist, I take you at your word. $f$ is a linear map between vector spaces, and that's that. It's an arrow in $\mathbf{Vect}$. Sets simply aren't mentioned here... right?</span> – <a href="/users/586/tom-leinster" title="23,461 reputation" class="comment-user">Tom Leinster</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956218_376973"><span title="2020-11-20 21:20:06Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 21:20</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956240" class="comment js-comment" data-comment-id="956240">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">12</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">@TomLeinster However, under that interpretation (which I would also favor), you then have to implicitly coerce your linear map to a set-function in order to write $f(x)$. (-:</span> – <a href="/users/49/mike-shulman" title="51,944 reputation" class="comment-user">Mike Shulman</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956240_376973"><span title="2020-11-20 22:20:27Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 22:20</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956314" class="comment js-comment" data-comment-id="956314">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">8</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">@CrabMan: That is a standard definition of natural numbers in set theory. However, how many number theorists do you know who write $2 \in 3$ instead of $2 < 3$?</span> – <a href="/users/1176/andrej-bauer" title="40,035 reputation" class="comment-user">Andrej Bauer</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956314_376973"><span title="2020-11-21 08:45:19Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 21 '20 at 8:45</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
</ul>
|
||
</div>
|
||
<div id="comments-link-376973" data-rep="50" data-anon="true">
|
||
<a class="js-show-link comments-link" title="expand to show all comments on this post" href="#" onclick="" role="button">show <b>27</b> more comments</a>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div><a name="376902" id="376902"></a>
|
||
<div id="answer-376902" class="answer" data-answerid="376902" itemprop="suggestedAnswer" itemscope="itemscope" itemtype="https://schema.org/Answer">
|
||
<div class="post-layout">
|
||
<div class="votecell post-layout--left">
|
||
<div class="js-voting-container grid jc-center fd-column ai-stretch gs4 fc-black-200" data-post-id="376902">
|
||
<button class="js-vote-up-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Up vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-6ke74cla"><svg aria-hidden="true" class="m0 svg-icon iconArrowUpLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 26h32L18 10 2 26z"></path></svg></button>
|
||
<div class="js-vote-count grid--cell fc-black-500 fs-title grid fd-column ai-center" itemprop="upvoteCount" data-value="30">
|
||
30
|
||
</div><button class="js-vote-down-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Down vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-spwznq1e"><svg aria-hidden="true" class="m0 svg-icon iconArrowDownLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 10h32L18 26 2 10z"></path></svg></button> <a class="js-post-issue grid--cell s-btn s-btn__unset c-pointer py6 mx-auto" href="/posts/376902/timeline" data-shortcut="T" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-label="Timeline" aria-describedby="--stacks-s-tooltip-ipud21td"><svg aria-hidden="true" class="mln2 mr0 svg-icon iconHistory" width="19" height="18" viewbox="0 0 19 18">
|
||
<path d="M3 9a8 8 0 113.73 6.77L8.2 14.3A6 6 0 105 9l3.01-.01-4 4-4-4h3L3 9zm7-4h1.01L11 9.36l3.22 2.1-.6.93L10 10V5z"></path></svg></a>
|
||
</div>
|
||
</div>
|
||
<div class="answercell post-layout--right">
|
||
<div class="s-prose js-post-body" itemprop="text">
|
||
<p>
|
||
<b>EDIT:</b> Since this question has gotten so much interest, I have decided to substantially rewrite my answer, stating explicitly here on MO some of the more important points rather than forcing the reader to follow links and chase down references.
|
||
</p>
|
||
<ol>
|
||
<li>To begin with, it is important to distinguish between <b>what currently existing proof assistants can do</b> versus <b>what they could do if we put in the necessary development work</b>. There is no doubt that existing type-theoretic proof assistants outperform existing set-theoretic proof assistants according to various important metrics, such as convenience, pre-existing libraries, etc. Someone who favors type-theoretic proof assistants therefore always has a trump card to play in these discussions—“What you say is nice in theory, but show me the money. How does your set-theoretic proof assistant perform in practice on real problems?” In an earlier version of this answer, I mentioned a talk by John Harrison entitled, “Let’s make set theory great again!” (<a href="https://www.youtube.com/watch?v=n0YNsJAoWQA" rel="noreferrer">part 1</a> <a href="https://www.youtube.com/watch?v=3jL8p9z86eg" rel="noreferrer">part 2</a> <a href="http://aitp-conference.org/2018/slides/JH.pdf" rel="noreferrer">slides</a>), and Andrej Bauer asked the reasonable question (in the comments below) whether Harrison had implemented his ideas. As <a href="https://cs.nyu.edu/pipermail/fom/2018-May/021026.html" rel="noreferrer">Jeremy Avigad</a> has said, even though he thinks that the “ideal proof assistant would be based on ZFC, with enough practical infrastructure to support all the things we need to do mathematics,” “it is easy to underestimate the difficulties involved in designing a useful and workable system.” At the same time, if we take the long view, we should be careful not to mistake what might be an artifact of our current implementations for a fundamental truth. <a href="https://cs.nyu.edu/pipermail/fom/2018-June/021032.html" rel="noreferrer">Larry Paulson</a> has in effect said “show me the money” in a more literal sense:
|
||
</li>
|
||
</ol>
|
||
<blockquote>
|
||
<p>
|
||
I would guess that the amount of effort and funding going into type theory exceeds the amount that went into set theory by an order of magnitude if not two. It's not unusual to encounter open hostility to set theory and classical logic combined with an air of moral superiority: “Oh, you aren’t constructive? And you don't store proof objects? Really?” And I have seen "proof assistant" actually DEFINED as "a software system for doing mathematics in a constructive type theory".<br />
|
||
<br />
|
||
The academic interest simply isn't there. Consider the huge achievements of the Mizar group and the minimal attention they have received. Also, I think that my 2002 paper on proving the reflection theorem (and presented at CADE, a high-profile conference) was really interesting, but it had been cited only six times, and two of those are by myself.<br />
|
||
<br />
|
||
I am certain that we would now have highly usable and flexible proof assistants based on some form of axiomatic set theory if this objective had enjoyed half the effort that has gone into type theory-based systems in the past 25 years.
|
||
</p>
|
||
</blockquote>
|
||
<ol start="2">
|
||
<li>
|
||
<p>
|
||
A second point is that everyone acknowledges that having a system where the computer can help you catch silly mistakes is a huge benefit, if not an absolute necessity. For this, some kind of type-theory-like mechanism is very useful. However, this is not as decisive an argument in favor of type theory and against set theory as it might seem at first glance. The “working mathematician” is often tempted to regard the absurdity of a statement such as <span class="math-container">$2\in 3$</span> as a strong argument against set theory, but the working mathematician also tends to balk at giving <span class="math-container">$0/0$</span> a concrete value (instead of declaring it to be “undefined”), which is the sort of thing that many proof assistants do. In both cases, there are known ways to block “fake theorems.” It is standard engineering practice to develop systems that contain multiple layers (the distinction between <i>vernacular</i> and <i>foundation</i> in Andrej Bauer’s excellent answer is an example), and the fact that <span class="math-container">$2\in 3$</span> might be a theorem at some low layer does not automatically mean that this is something a user will be able to enter from the keyboard and not get caught by the system. In principle, therefore—to return to the actual question being asked—set theory does not seem to pose any intrinsic barriers to automation. Indeed, other <a href="https://mathoverflow.net/a/377031">answers</a> and <a href="https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista#comment956156_376988">comments</a> have made this point, and explained how powerful automation tactics can and have been written in set-theoretic systems such as Metamath. Another example is the work of <a href="https://arxiv.org/abs/1707.04757" rel="noreferrer">Bohua Zhan</a> on auto2, which has shown that many of the alleged difficulties with untyped set theory can be overcome.
|
||
</p>
|
||
</li>
|
||
<li>
|
||
<p>
|
||
There remains the question, even if a set-theoretic proof assistant with the power and usability of Coq/Lean/Isabelle <i>could</i> be developed, what would be the point? Aren't the already existing type-theoretic assistants good enough? This is a much more “subjective and argumentative” point, but I would propose a couple of arguments in favor of set theory. The first is that set theory has a great deal of flexibility, and it is not an accident that historically, the first convincing demonstration that all of mathematics could be put on a single, common foundation was accomplished using set theory rather than type theory. With a relatively small amount of training, mathematicians can see how to formulate any concepts and proofs in their field of expertise in set-theoretic terms. In the language of Penelope Maddy’s paper, <a href="http://www.socsci.uci.edu/%7Epjmaddy/bio/What%20do%20we%20want%20-%20final" rel="noreferrer">What do we want a foundation to do?</a> set theory provides a <i>Generous Arena</i> and a <i>Shared Standard</i> for all of mathematics with minimal fuss. Of course, there is a price to be paid if we give someone enough rope—they might decide to hang themselves. But if we want to see widespread adoption of proof assistants by the mathematical community, then we should take seriously any opportunities we have to leverage mathematicians’ existing habits of thought. I do not think that it is an accident that set-theoretic proof assistants tend to produce more human-readable proofs than type-theoretic proof assistants do (though I will admit that this could be an artifact of existing systems, rather than a fundamental truth).<br />
|
||
<br />
|
||
Another argument is that if we are interested in reverse mathematics—which axioms are needed to prove which theorems—then there has been a lot more work done to calibrate mathematics against set-theoretic and arithmetical systems than against type-theoretic systems. In Maddy’s language, we might hope for a proof assistant to help us with <i>Risk Assessment</i> and <i>Metamathematical Corral</i>. This does not seem to be a priority with too many people at the present time, but again I am trying to take the long view here. The mathematical community already has a good grasp of how the mathematical universe can be built from the ground up using set theory, and exactly what ingredients are needed to achieve which results. It would be desirable for our proof assistants to be able to capture this global picture.<br />
|
||
<br />
|
||
One could point out that someone who is really interested in set theory can use something like Isabelle/ZF, which builds set theory on top of type theory. That is true. I am not trying to argue here that a set-theoretic foundation with some kind of type theory layered on top is necessarily better than a type-theoretic foundation with some kind of set theory layered on top. I am only trying to argue that set theory does enjoy some advantages over type theory, depending on what you are trying to achieve, and that the claim that “automation is very difficult with set theory,” or that there is nothing to be gained by using set theory as the basis for a proof assistant, should be taken with a grain of salt.
|
||
</p>
|
||
</li>
|
||
</ol>
|
||
<hr />
|
||
<p>
|
||
Let me conclude with a remark about Lean specifically. A couple of years ago, Tom Hales provided a <a href="https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/" rel="noreferrer">review of the Lean theorem prover</a> that spells out the pros and cons as he saw them at the time. Some of what he said may no longer be true today, but one thing that is true is that even Lean enthusiasts agree that there are flaws that they promise will be fixed in Lean Version 4 (which unfortunately is going to be incompatible with Lean 3, or so I hear).
|
||
</p>
|
||
</div>
|
||
<div class="mt24">
|
||
<div class="grid fw-wrap ai-start jc-end gs8 gsy">
|
||
<div class="grid--cell mr16" style="flex: 1 1 100px;">
|
||
<div class="js-post-menu pt2" data-post-id="376902">
|
||
<div class="grid d-flex gs8 s-anchors s-anchors__muted fw-wrap">
|
||
<div class="grid--cell">
|
||
<a href="/a/376902" rel="nofollow" itemprop="url" class="js-share-link js-gps-track" title="Short permalink to this answer" data-gps-track="post.click({ item: 2, priv: 0, post_type: 2 })" data-controller="se-share-sheet s-popover" data-se-share-sheet-title="Share a link to this answer" data-se-share-sheet-subtitle="" data-se-share-sheet-post-type="answer" data-se-share-sheet-social="facebook twitter" data-se-share-sheet-location="2" data-se-share-sheet-license-url="https%3a%2f%2fcreativecommons.org%2flicenses%2fby-sa%2f4.0%2f" data-se-share-sheet-license-name="CC BY-SA 4.0" data-s-popover-placement="bottom-start" aria-controls="se-share-sheet-2" data-action="s-popover#toggle se-share-sheet#preventNavigation s-popover:show->se-share-sheet#willShow s-popover:shown->se-share-sheet#didShow">Share</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" class="js-cite-link s-btn s-btn__link">Cite</button>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<a href="/posts/376902/edit" class="js-suggest-edit-post js-gps-track" data-gps-track="post.click({ item: 6, priv: 0, post_type: 2 })" title="">Improve this answer</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" id="btnFollowPost-376902" class="s-btn s-btn__link js-follow-post js-follow-answer js-gps-track" data-gps-track="post.click({ item: 14, priv: 0, post_type: 2 })" data-controller="s-tooltip" data-s-tooltip-placement="bottom" data-s-popover-placement="bottom" aria-controls="" aria-describedby="--stacks-s-tooltip-j3zheqzf">Follow</button>
|
||
</div>
|
||
</div>
|
||
<div class="js-menu-popup-container"></div>
|
||
</div>
|
||
</div>
|
||
<div class="post-signature grid--cell fl0">
|
||
<div class="user-info">
|
||
<div class="user-action-time">
|
||
<a href="/posts/376902/revisions" title="show all edits to this post" class="js-gps-track" data-gps-track="post.click({ item: 4, priv: 0, post_type: 2 })">edited <span title="2020-11-24 19:25:23Z" class="relativetime">Nov 24 '20 at 19:25</span></a>
|
||
</div>
|
||
<div class="user-gravatar32"></div>
|
||
<div class="user-details">
|
||
<div class="-flair"></div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="post-signature grid--cell fl0">
|
||
<div class="user-info">
|
||
<div class="user-action-time">
|
||
answered <span title="2020-11-19 18:49:07Z" class="relativetime">Nov 19 '20 at 18:49</span>
|
||
</div>
|
||
<div class="user-gravatar32">
|
||
<a href="/users/3106/timothy-chow">
|
||
<div class="gravatar-wrapper-32">
|
||
<img src="https://www.gravatar.com/avatar/349934205967b047f672663e52cfe80a?s=32&d=identicon&r=PG" alt="" width="32" height="32" class="bar-sm" />
|
||
</div></a>
|
||
</div>
|
||
<div class="user-details" itemprop="author" itemscope="itemscope" itemtype="https://schema.org/Person">
|
||
<a href="/users/3106/timothy-chow">Timothy Chow</a>
|
||
<div class="-flair">
|
||
<span class="reputation-score" title="reputation score 54,451" dir="ltr">54.5k</span><span title="18 gold badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">18</span></span><span class="v-visible-sr">18 gold badges</span><span title="244 silver badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">244</span></span><span class="v-visible-sr">244 silver badges</span><span title="415 bronze badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">415</span></span><span class="v-visible-sr">415 bronze badges</span>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="post-layout--right">
|
||
<div id="comments-376902" class="comments js-comments-container bt bc-black-075 mt12" data-post-id="376902" data-min-length="15">
|
||
<ul class="comments-list js-comments-list" data-remaining-comments-count="13" data-canpost="false" data-cansee="true" data-comments-unavailable="false" data-addlink-disabled="true">
|
||
<li id="comment-955882" class="comment js-comment" data-comment-id="955882">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">5</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">John Harrison's slides are a fine collection of suggestions, but there is a long way from having good ideas about theorem provers to implementing them and trying them out. Has Harisson worked on the ideas?</span> – <a href="/users/1176/andrej-bauer" title="40,035 reputation" class="comment-user">Andrej Bauer</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment955882_376902"><span title="2020-11-19 19:20:02Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 19 '20 at 19:20</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-955895" class="comment js-comment" data-comment-id="955895">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">9</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">What if they are also more natural for mathematicians?</span> – <a href="/users/1176/andrej-bauer" title="40,035 reputation" class="comment-user">Andrej Bauer</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment955895_376902"><span title="2020-11-19 20:24:51Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 19 '20 at 20:24</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-955982" class="comment js-comment" data-comment-id="955982">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="cool">3</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">Types are wonderful in both programming and mathematics.</span> – <a href="/users/613/deane-yang" title="23,582 reputation" class="comment-user">Deane Yang</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment955982_376902"><span title="2020-11-20 03:39:19Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 3:39</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956098" class="comment js-comment" data-comment-id="956098">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">5</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">When I am doing counting, I like my natural numbers to start at 0 (because some sets are empty). When I am doing primes and factoring, I like them to start at 1 (otherwise I have to continually have to write "if n isn't zero then..."). My feelings about sets and types are the same -- different foundational systems make different things easier/nicer.</span> – <a href="/users/1384/kevin-buzzard" title="37,243 reputation" class="comment-user">Kevin Buzzard</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956098_376902"><span title="2020-11-20 14:16:57Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 14:16</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956303" class="comment js-comment" data-comment-id="956303">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">5</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">There's also this article by Leslie Lamport and Larry Paulson: <a href="https://lamport.azurewebsites.net/pubs/lamport-types.pdf" rel="nofollow noreferrer">lamport.azurewebsites.net/pubs/lamport-types.pdf</a> The point is that just because a programming language is typed, that doesn't mean one should make the specification language typed, and types can cause problems as well as solve them. There is some rebuttal to the "$2 \in 3$ is gibberish" argument. My own is that I have never found any difficulty in writing gibberish in any typed language, especially by accident.</span> – <a href="/users/61785/robert-furber" title="2,856 reputation" class="comment-user">Robert Furber</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956303_376902"><span title="2020-11-21 06:53:09Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 21 '20 at 6:53</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
</ul>
|
||
</div>
|
||
<div id="comments-link-376902" data-rep="50" data-anon="true">
|
||
<a class="js-show-link comments-link" title="expand to show all comments on this post" href="#" onclick="" role="button">show <b>13</b> more comments</a>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div><a name="376988" id="376988"></a>
|
||
<div id="answer-376988" class="answer" data-answerid="376988" itemprop="suggestedAnswer" itemscope="itemscope" itemtype="https://schema.org/Answer">
|
||
<div class="post-layout">
|
||
<div class="votecell post-layout--left">
|
||
<div class="js-voting-container grid jc-center fd-column ai-stretch gs4 fc-black-200" data-post-id="376988">
|
||
<button class="js-vote-up-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Up vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-jdued8k9"><svg aria-hidden="true" class="m0 svg-icon iconArrowUpLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 26h32L18 10 2 26z"></path></svg></button>
|
||
<div class="js-vote-count grid--cell fc-black-500 fs-title grid fd-column ai-center" itemprop="upvoteCount" data-value="27">
|
||
27
|
||
</div><button class="js-vote-down-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Down vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-zjnoav1j"><svg aria-hidden="true" class="m0 svg-icon iconArrowDownLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 10h32L18 26 2 10z"></path></svg></button> <a class="js-post-issue grid--cell s-btn s-btn__unset c-pointer py6 mx-auto" href="/posts/376988/timeline" data-shortcut="T" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-label="Timeline" aria-describedby="--stacks-s-tooltip-6fvdehlq"><svg aria-hidden="true" class="mln2 mr0 svg-icon iconHistory" width="19" height="18" viewbox="0 0 19 18">
|
||
<path d="M3 9a8 8 0 113.73 6.77L8.2 14.3A6 6 0 105 9l3.01-.01-4 4-4-4h3L3 9zm7-4h1.01L11 9.36l3.22 2.1-.6.93L10 10V5z"></path></svg></a>
|
||
</div>
|
||
</div>
|
||
<div class="answercell post-layout--right">
|
||
<div class="s-prose js-post-body" itemprop="text">
|
||
<p>
|
||
I still find it very surprising that this random talk I gave attracts so much attention, especially as not everything I said was very well thought out. I am more than happy to engage with people in discussions about what I said and whether or not some things I said were ill-informed.
|
||
</p>
|
||
<p>
|
||
But onto my answer to your question: whilst I am not an expert in proof assistants in general (I have become knowledgeable at precisely <em>one</em> proof assistant and have limited experience with others), it is my empirical observation that high-level tactics like Lean's <code>ring</code> tactic, which will <a href="https://leanprover-community.github.io/lean-web-editor/#code=import%20tactic%0A%0Aexample%20%28R%20%3A%20Type%29%20%5Bcomm_ring%20R%5D%20%28x%20y%20%3A%20R%29%20%3A%0A%20%20%28x%2B2*y%29%5E3%3Dx%5E3%2B6*x%5E2*y%2B12*x*y%5E2%2B8*y%5E3%20%3A%3D%0Abegin%0A%20%20ring%0Aend" rel="noreferrer">prove results</a> like <span class="math-container">$(x+2y)^3=x^3+6x^2y+12xy^2+8y^3$</span> immediately -- and there are similar tactics in Coq and Isabelle/HOL, two more type theory systems -- do not seem to exist in the two main set theory formal proof systems, namely Metamath and Mizar. I don't really know why, but those are the facts. Note that the proof of this from the axioms of a ring is extremely long and uncomfortable, because you need to apply associativity and commutativity of addition and multiplication many times -- things mathematicians do almost without thinking.
|
||
</p>
|
||
</div>
|
||
<div class="mt24">
|
||
<div class="grid fw-wrap ai-start jc-end gs8 gsy">
|
||
<div class="grid--cell mr16" style="flex: 1 1 100px;">
|
||
<div class="js-post-menu pt2" data-post-id="376988">
|
||
<div class="grid d-flex gs8 s-anchors s-anchors__muted fw-wrap">
|
||
<div class="grid--cell">
|
||
<a href="/a/376988" rel="nofollow" itemprop="url" class="js-share-link js-gps-track" title="Short permalink to this answer" data-gps-track="post.click({ item: 2, priv: 0, post_type: 2 })" data-controller="se-share-sheet s-popover" data-se-share-sheet-title="Share a link to this answer" data-se-share-sheet-subtitle="" data-se-share-sheet-post-type="answer" data-se-share-sheet-social="facebook twitter" data-se-share-sheet-location="2" data-se-share-sheet-license-url="https%3a%2f%2fcreativecommons.org%2flicenses%2fby-sa%2f4.0%2f" data-se-share-sheet-license-name="CC BY-SA 4.0" data-s-popover-placement="bottom-start" aria-controls="se-share-sheet-3" data-action="s-popover#toggle se-share-sheet#preventNavigation s-popover:show->se-share-sheet#willShow s-popover:shown->se-share-sheet#didShow">Share</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" class="js-cite-link s-btn s-btn__link">Cite</button>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<a href="/posts/376988/edit" class="js-suggest-edit-post js-gps-track" data-gps-track="post.click({ item: 6, priv: 0, post_type: 2 })" title="">Improve this answer</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" id="btnFollowPost-376988" class="s-btn s-btn__link js-follow-post js-follow-answer js-gps-track" data-gps-track="post.click({ item: 14, priv: 0, post_type: 2 })" data-controller="s-tooltip" data-s-tooltip-placement="bottom" data-s-popover-placement="bottom" aria-controls="" aria-describedby="--stacks-s-tooltip-168s4a40">Follow</button>
|
||
</div>
|
||
</div>
|
||
<div class="js-menu-popup-container"></div>
|
||
</div>
|
||
</div>
|
||
<div class="post-signature grid--cell fl0">
|
||
<div class="user-info">
|
||
<div class="user-action-time">
|
||
<a href="/posts/376988/revisions" title="show all edits to this post" class="js-gps-track" data-gps-track="post.click({ item: 4, priv: 0, post_type: 2 })">edited <span title="2020-11-20 14:10:48Z" class="relativetime">Nov 20 '20 at 14:10</span></a>
|
||
</div>
|
||
<div class="user-gravatar32"></div>
|
||
<div class="user-details">
|
||
<div class="-flair"></div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="post-signature grid--cell fl0">
|
||
<div class="user-info user-hover">
|
||
<div class="user-action-time">
|
||
answered <span title="2020-11-20 13:59:36Z" class="relativetime">Nov 20 '20 at 13:59</span>
|
||
</div>
|
||
<div class="user-gravatar32">
|
||
<a href="/users/1384/kevin-buzzard">
|
||
<div class="gravatar-wrapper-32">
|
||
<img src="https://www.gravatar.com/avatar/b4221f647744a67d83ef518f7a894d61?s=32&d=identicon&r=PG" alt="" width="32" height="32" class="bar-sm" />
|
||
</div></a>
|
||
</div>
|
||
<div class="user-details" itemprop="author" itemscope="itemscope" itemtype="https://schema.org/Person">
|
||
<a href="/users/1384/kevin-buzzard">Kevin Buzzard</a>
|
||
<div class="-flair">
|
||
<span class="reputation-score" title="reputation score 37,243" dir="ltr">37.2k</span><span title="12 gold badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">12</span></span><span class="v-visible-sr">12 gold badges</span><span title="143 silver badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">143</span></span><span class="v-visible-sr">143 silver badges</span><span title="227 bronze badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">227</span></span><span class="v-visible-sr">227 bronze badges</span>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="post-layout--right">
|
||
<div id="comments-376988" class="comments js-comments-container bt bc-black-075 mt12" data-post-id="376988" data-min-length="15">
|
||
<ul class="comments-list js-comments-list" data-remaining-comments-count="0" data-canpost="false" data-cansee="true" data-comments-unavailable="false" data-addlink-disabled="true">
|
||
<li id="comment-956105" class="comment js-comment" data-comment-id="956105">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="cool">4</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">So echoing a comment that Andrej made -- as well as asking "what can be done in theory?", in this game an equally important question is "what can be done in practice?" Mario Carneiro is an expert in both Metamath and Lean, and he wrote Lean's ring tactic in just a few days as far as I could see, but Metamath still has no ring tactic.</span> – <a href="/users/1384/kevin-buzzard" title="37,243 reputation" class="comment-user">Kevin Buzzard</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956105_376988"><span title="2020-11-20 14:28:01Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 14:28</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956156" class="comment js-comment" data-comment-id="956156">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">8</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">Part of the reason I didn't write ring for Metamath is because there weren't that many examples that came up that couldn't be done manually with a better proof; in metamath a tactic that creates ugly proofs is a much harder sell because every single line of the proof is laid bare for everyone to read. The numeric evaluator (aka <code>norm_num</code> in lean) <i>was</i> written in metamath and contains the same techniques as a ring tactic would have.</span> – <a href="/users/34444/mario-carneiro" title="1,002 reputation" class="comment-user">Mario Carneiro</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956156_376988"><span title="2020-11-20 16:52:53Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 16:52</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956157" class="comment js-comment" data-comment-id="956157">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">5</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">... The current proof assistant I am working in, Metamath Zero, is based on peano arithmetic, not even set theory, and a ring tactic would be similarly easy to write as in lean. This has more to do with the framework around the language rather than the formal system (in Andrej's terminology: $M$ matters for writing automation, not $F$), and the problem with Metamath is that $M$ is in no way encoded in the "deliverables", so every author must discover it for themselves.</span> – <a href="/users/34444/mario-carneiro" title="1,002 reputation" class="comment-user">Mario Carneiro</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956157_376988"><span title="2020-11-20 16:55:51Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 16:55</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
</ul>
|
||
</div>
|
||
<div id="comments-link-376988" data-rep="50" data-anon="true">
|
||
<a class="js-add-link comments-link disabled-link" title="Use comments to ask for more information or suggest improvements. Avoid comments like “+1” or “thanks”." href="#" role="button">add a comment</a>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div><a name="377031" id="377031"></a>
|
||
<div id="answer-377031" class="answer" data-answerid="377031" itemprop="suggestedAnswer" itemscope="itemscope" itemtype="https://schema.org/Answer">
|
||
<div class="post-layout">
|
||
<div class="votecell post-layout--left">
|
||
<div class="js-voting-container grid jc-center fd-column ai-stretch gs4 fc-black-200" data-post-id="377031">
|
||
<button class="js-vote-up-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Up vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-0hmzev9r"><svg aria-hidden="true" class="m0 svg-icon iconArrowUpLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 26h32L18 10 2 26z"></path></svg></button>
|
||
<div class="js-vote-count grid--cell fc-black-500 fs-title grid fd-column ai-center" itemprop="upvoteCount" data-value="6">
|
||
6
|
||
</div><button class="js-vote-down-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Down vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-0z6z1yk6"><svg aria-hidden="true" class="m0 svg-icon iconArrowDownLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 10h32L18 26 2 10z"></path></svg></button> <a class="js-post-issue grid--cell s-btn s-btn__unset c-pointer py6 mx-auto" href="/posts/377031/timeline" data-shortcut="T" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-label="Timeline" aria-describedby="--stacks-s-tooltip-1deomp5o"><svg aria-hidden="true" class="mln2 mr0 svg-icon iconHistory" width="19" height="18" viewbox="0 0 19 18">
|
||
<path d="M3 9a8 8 0 113.73 6.77L8.2 14.3A6 6 0 105 9l3.01-.01-4 4-4-4h3L3 9zm7-4h1.01L11 9.36l3.22 2.1-.6.93L10 10V5z"></path></svg></a>
|
||
</div>
|
||
</div>
|
||
<div class="answercell post-layout--right">
|
||
<div class="s-prose js-post-body" itemprop="text">
|
||
<p>
|
||
I'll answer just the automation question since the other answers gave nice broad overview, but didn't seem focus on that narrow question. My own direct automation experience is wrt to ACL2, Lean and SMT-based solvers.
|
||
</p>
|
||
<p>
|
||
Strictly speaking, I don't know if there's any foundational argument for why set theory would be better or worse than the type theory-based approach in Lean.
|
||
</p>
|
||
<p>
|
||
The strengths that Lean have from my perspective are: an expressive explicit type system, a relatively simple core language for representing terms, and a attention to how terms are represented for efficient manipulation.
|
||
</p>
|
||
<p>
|
||
With regards to typed core logics, most automation in theorem provers is tailored to specific common theories that are widely used in mathematics. When writing such automation, it is important to know the types and operations involved. For example, in writing a decision procedure for linear arithmetic in an untyped language, one needs to carefully check that any transformations still make sense even if the expressions do not denote numbers. By having a typed and typechecked expression language, one gets from the theorem prover itself and does not have to pay the additional runtime and complexity costs.
|
||
</p>
|
||
<p>
|
||
A second strength of Lean is ensuring that the core language is simple, but expressive so that one can represent proofs compactly. When using automation such as SMT solvers, the "proof terms" generated as evidence can be very large and the core proof language needs to be designed to compactly represent proofs while still be amenably to efficient checking. I'm not sure if Lean has an advantage to Coq or other solvers here per se but it is a factor in Lean's design.
|
||
</p>
|
||
<p>
|
||
A third strength of Lean is that the language for writing tactics and creating definitions and theorems are one and the same. There is a bit of syntactic sugar for the tactic sequences and a tactic-specific library, but by having the same language one does not have to learn multiple languages just to get started writing tactics. Lean is also not unique here -- ACL2 is similar, but it is a strength of Lean still. It will also become even more relevant with Lean 4 thanks to the efficient compiler being developed.
|
||
</p>
|
||
</div>
|
||
<div class="mt24">
|
||
<div class="grid fw-wrap ai-start jc-end gs8 gsy">
|
||
<div class="grid--cell mr16" style="flex: 1 1 100px;">
|
||
<div class="js-post-menu pt2" data-post-id="377031">
|
||
<div class="grid d-flex gs8 s-anchors s-anchors__muted fw-wrap">
|
||
<div class="grid--cell">
|
||
<a href="/a/377031" rel="nofollow" itemprop="url" class="js-share-link js-gps-track" title="Short permalink to this answer" data-gps-track="post.click({ item: 2, priv: 0, post_type: 2 })" data-controller="se-share-sheet s-popover" data-se-share-sheet-title="Share a link to this answer" data-se-share-sheet-subtitle="" data-se-share-sheet-post-type="answer" data-se-share-sheet-social="facebook twitter" data-se-share-sheet-location="2" data-se-share-sheet-license-url="https%3a%2f%2fcreativecommons.org%2flicenses%2fby-sa%2f4.0%2f" data-se-share-sheet-license-name="CC BY-SA 4.0" data-s-popover-placement="bottom-start" aria-controls="se-share-sheet-4" data-action="s-popover#toggle se-share-sheet#preventNavigation s-popover:show->se-share-sheet#willShow s-popover:shown->se-share-sheet#didShow">Share</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" class="js-cite-link s-btn s-btn__link">Cite</button>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<a href="/posts/377031/edit" class="js-suggest-edit-post js-gps-track" data-gps-track="post.click({ item: 6, priv: 0, post_type: 2 })" title="">Improve this answer</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" id="btnFollowPost-377031" class="s-btn s-btn__link js-follow-post js-follow-answer js-gps-track" data-gps-track="post.click({ item: 14, priv: 0, post_type: 2 })" data-controller="s-tooltip" data-s-tooltip-placement="bottom" data-s-popover-placement="bottom" aria-controls="" aria-describedby="--stacks-s-tooltip-s6aq6meo">Follow</button>
|
||
</div>
|
||
</div>
|
||
<div class="js-menu-popup-container"></div>
|
||
</div>
|
||
</div>
|
||
<div class="post-signature grid--cell fl0">
|
||
<div class="user-info">
|
||
<div class="user-action-time">
|
||
answered <span title="2020-11-20 20:31:36Z" class="relativetime">Nov 20 '20 at 20:31</span>
|
||
</div>
|
||
<div class="user-gravatar32">
|
||
<a href="/users/169076/joe-hendrix">
|
||
<div class="gravatar-wrapper-32">
|
||
<img src="https://www.gravatar.com/avatar/59a42d941c5ab2d4cd4ce8172c61ec97?s=32&d=identicon&r=PG" alt="" width="32" height="32" class="bar-sm" />
|
||
</div></a>
|
||
</div>
|
||
<div class="user-details" itemprop="author" itemscope="itemscope" itemtype="https://schema.org/Person">
|
||
<a href="/users/169076/joe-hendrix">Joe Hendrix</a>
|
||
<div class="-flair">
|
||
<span class="reputation-score" title="reputation score " dir="ltr">61</span><span title="1 bronze badge" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">1</span></span><span class="v-visible-sr">1 bronze badge</span>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="post-layout--right">
|
||
<div id="comments-link-377031" data-rep="50" data-anon="true">
|
||
<a class="js-add-link comments-link disabled-link" title="Use comments to ask for more information or suggest improvements. Avoid comments like “+1” or “thanks”." href="#" role="button">add a comment</a>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div><a name="376936" id="376936"></a>
|
||
<div id="answer-376936" class="answer" data-answerid="376936" itemprop="suggestedAnswer" itemscope="itemscope" itemtype="https://schema.org/Answer">
|
||
<div class="post-layout">
|
||
<div class="votecell post-layout--left">
|
||
<div class="js-voting-container grid jc-center fd-column ai-stretch gs4 fc-black-200" data-post-id="376936">
|
||
<button class="js-vote-up-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Up vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-iuhithso"><svg aria-hidden="true" class="m0 svg-icon iconArrowUpLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 26h32L18 10 2 26z"></path></svg></button>
|
||
<div class="js-vote-count grid--cell fc-black-500 fs-title grid fd-column ai-center" itemprop="upvoteCount" data-value="-2">
|
||
-2
|
||
</div><button class="js-vote-down-btn grid--cell s-btn s-btn__unset c-pointer" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-pressed="false" aria-label="Down vote" data-selected-classes="fc-theme-primary" aria-describedby="--stacks-s-tooltip-4u0z9jjq"><svg aria-hidden="true" class="m0 svg-icon iconArrowDownLg" width="36" height="36" viewbox="0 0 36 36">
|
||
<path d="M2 10h32L18 26 2 10z"></path></svg></button> <a class="js-post-issue grid--cell s-btn s-btn__unset c-pointer py6 mx-auto" href="/posts/376936/timeline" data-shortcut="T" data-controller="s-tooltip" data-s-tooltip-placement="right" aria-label="Timeline" aria-describedby="--stacks-s-tooltip-mmgfimt9"><svg aria-hidden="true" class="mln2 mr0 svg-icon iconHistory" width="19" height="18" viewbox="0 0 19 18">
|
||
<path d="M3 9a8 8 0 113.73 6.77L8.2 14.3A6 6 0 105 9l3.01-.01-4 4-4-4h3L3 9zm7-4h1.01L11 9.36l3.22 2.1-.6.93L10 10V5z"></path></svg></a>
|
||
</div>
|
||
</div>
|
||
<div class="answercell post-layout--right">
|
||
<div class="s-prose js-post-body" itemprop="text">
|
||
<p>
|
||
Modern programming languages unlike older programming languages, or unlike assembly and machine code are typed. For example c++ with or without templates compared to c, or Java compared to Basic.
|
||
</p>
|
||
<p>
|
||
With typing, a compiler needs to check that all expressions have the correct type. Generally, this is done by telling the compiler what types are being used. However, we can attempt to automate this process and allow the compiler to work out what the types are by itself, given the base types under consideration. This is known as type inference.
|
||
</p>
|
||
<p>
|
||
Depending upon the language, type checking and inference can range from trivial to undecidable.
|
||
</p>
|
||
<p>
|
||
We also say it is sound iff it accepts correctly typed programs.
|
||
</p>
|
||
<p>
|
||
Now, type checking and inference in the simply typed Lambda Calculus with parametric polymorphism is decidable and one implementation of this is the Hindley-Milner Type Sysyem where complexity is linear in the size of the program; however, the problem is PSPACE hard and EXPTIME complete, meaning that in the worst case scenario it requires a polynomial worth of extra space and an exponential amount of extra time. Luckily, it happens to be linear when the nesting depth of polymorphic variables is bounded.
|
||
</p>
|
||
<p>
|
||
For example,
|
||
</p>
|
||
<blockquote>
|
||
<ol>
|
||
<li>C++ with templates is Turing complete by an informal proof by Veldhuizen '03. This means type checking and inference is undecidable.
|
||
</li>
|
||
</ol>
|
||
</blockquote>
|
||
<blockquote>
|
||
<ol start="2">
|
||
<li>In C#, both type checking and inference is undecidable. And it is unsound.
|
||
</li>
|
||
</ol>
|
||
</blockquote>
|
||
<blockquote>
|
||
<ol start="3">
|
||
<li>Similarly Java because Java Generics are Turing Complete. Amin and Tate '15 showed that Java 5 or later is unsound.
|
||
</li>
|
||
</ol>
|
||
</blockquote>
|
||
<blockquote>
|
||
<ol start="4">
|
||
<li>Haskell has decidable type checking and inference. But with enough extensions, that is to at least System F, then it becomes undecidable as System F is.
|
||
</li>
|
||
</ol>
|
||
</blockquote>
|
||
<p>
|
||
Dependent types allow types to depend upon their values and so give a finer control over types. For example, with ordinary types you cannot have a type for even numbers; with dependent types you can. Unfortunately, adding this capability generally renders type inference undecidable.
|
||
</p>
|
||
<p>
|
||
Lean is a programming language which is based upon Calculus of Constructions with Inductive Tupes. This calculus is a higher order typed Lambda Calculus and lies at the top node of Barendregt's Lambda Cube. This means it has polymorphism and dependent types.
|
||
</p>
|
||
<p>
|
||
It's main rival, is Martin Lof's Type Theory which is also dependent and inductive types. It comes in two main varieties, intensional and extensional. The intensional variety can be alternatively thought of as Homotopy Type Theory. In this variety, type inference is decidable whilst in the extensional variety it is not.
|
||
</p>
|
||
<p>
|
||
Set Theory like machine code, like assembly and like early programming languages are not typed. So type checking does not apply. As types allow us to program more safely, these languages are not as safe as typeful languages and hence, automation is more difficult here as we cannot prove they will act as we expect them to do so.
|
||
</p>
|
||
<p>
|
||
Typed languages does not mean that untyped languages will go away. After all, the languages at all in fact nested. Haskell, at bottom, is still executed by machine code and this is untyped. Hence, development of both is required for automation in all it's varieties.
|
||
</p>
|
||
<p>
|
||
After all, if I had to program the fastest loop to add as many consecutive integers in a second as I could on a particular machine I would choose to write it in machine code, I typed as it is - every time. More importantly, in my opinion it's makes one realise how the whole stack of languages from the editor through the compiler and then through the interface and interrupts down to the metal works. In this way, you learn more about how every works 'under the hood' - so to speak.
|
||
</p>
|
||
<p>
|
||
<strong>edit</strong>
|
||
</p>
|
||
<p>
|
||
@LSpice: It's written this way because the question itself is kind of vague. Why not ask the OP to tighten up the question? The proposed question is answered in the last paragraph. And the preceding paragraphs simply explains my terms and my thinking in a step-by-step pedagogical manner rather than a deus ex-machina manner ... or do you think explanatory text is a little too old-fashioned for the hyped up and glib virtual world?
|
||
</p>
|
||
</div>
|
||
<div class="mt24">
|
||
<div class="grid fw-wrap ai-start jc-end gs8 gsy">
|
||
<div class="grid--cell mr16" style="flex: 1 1 100px;">
|
||
<div class="js-post-menu pt2" data-post-id="376936">
|
||
<div class="grid d-flex gs8 s-anchors s-anchors__muted fw-wrap">
|
||
<div class="grid--cell">
|
||
<a href="/a/376936" rel="nofollow" itemprop="url" class="js-share-link js-gps-track" title="Short permalink to this answer" data-gps-track="post.click({ item: 2, priv: 0, post_type: 2 })" data-controller="se-share-sheet s-popover" data-se-share-sheet-title="Share a link to this answer" data-se-share-sheet-subtitle="" data-se-share-sheet-post-type="answer" data-se-share-sheet-social="facebook twitter" data-se-share-sheet-location="2" data-se-share-sheet-license-url="https%3a%2f%2fcreativecommons.org%2flicenses%2fby-sa%2f4.0%2f" data-se-share-sheet-license-name="CC BY-SA 4.0" data-s-popover-placement="bottom-start" aria-controls="se-share-sheet-5" data-action="s-popover#toggle se-share-sheet#preventNavigation s-popover:show->se-share-sheet#willShow s-popover:shown->se-share-sheet#didShow">Share</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" class="js-cite-link s-btn s-btn__link">Cite</button>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<a href="/posts/376936/edit" class="js-suggest-edit-post js-gps-track" data-gps-track="post.click({ item: 6, priv: 0, post_type: 2 })" title="">Improve this answer</a>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<button type="button" id="btnFollowPost-376936" class="s-btn s-btn__link js-follow-post js-follow-answer js-gps-track" data-gps-track="post.click({ item: 14, priv: 0, post_type: 2 })" data-controller="s-tooltip" data-s-tooltip-placement="bottom" data-s-popover-placement="bottom" aria-controls="" aria-describedby="--stacks-s-tooltip-m01vl7qp">Follow</button>
|
||
</div>
|
||
</div>
|
||
<div class="js-menu-popup-container"></div>
|
||
</div>
|
||
</div>
|
||
<div class="post-signature grid--cell fl0">
|
||
<div class="user-info">
|
||
<div class="user-action-time">
|
||
<a href="/posts/376936/revisions" title="show all edits to this post" class="js-gps-track" data-gps-track="post.click({ item: 4, priv: 0, post_type: 2 })">edited <span title="2020-11-20 02:42:42Z" class="relativetime">Nov 20 '20 at 2:42</span></a>
|
||
</div>
|
||
<div class="user-gravatar32"></div>
|
||
<div class="user-details">
|
||
<div class="-flair"></div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="post-signature grid--cell fl0">
|
||
<div class="user-info user-hover">
|
||
<div class="user-action-time">
|
||
answered <span title="2020-11-20 02:04:11Z" class="relativetime">Nov 20 '20 at 2:04</span>
|
||
</div>
|
||
<div class="user-gravatar32">
|
||
<a href="/users/35706/mozibur-ullah">
|
||
<div class="gravatar-wrapper-32">
|
||
<img src="https://i.stack.imgur.com/sw7YK.jpg?s=32&g=1" alt="" width="32" height="32" class="bar-sm" />
|
||
</div></a>
|
||
</div>
|
||
<div class="user-details" itemprop="author" itemscope="itemscope" itemtype="https://schema.org/Person">
|
||
<a href="/users/35706/mozibur-ullah">Mozibur Ullah</a>
|
||
<div class="-flair">
|
||
<span class="reputation-score" title="reputation score " dir="ltr">1,041</span><span title="6 silver badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">6</span></span><span class="v-visible-sr">6 silver badges</span><span title="15 bronze badges" aria-hidden="true"><img src="https://cdn.sstatic.net/Img/unified/sprites.svg?v=fcc0ea44ba27" /><span class="badgecount">15</span></span><span class="v-visible-sr">15 bronze badges</span>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="post-layout--right">
|
||
<div id="comments-376936" class="comments js-comments-container bt bc-black-075 mt12" data-post-id="376936" data-min-length="15">
|
||
<ul class="comments-list js-comments-list" data-remaining-comments-count="1" data-canpost="false" data-cansee="true" data-comments-unavailable="false" data-addlink-disabled="true">
|
||
<li id="comment-955971" class="comment js-comment" data-comment-id="955971">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="cool">2</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">This seems like a great answer to a question of "Typed programming languages: what and why?", but it seems too general to shed much light on this more focussed question.</span> – <a href="/users/2383/lspice" title="5,123 reputation" class="comment-user">LSpice</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment955971_376936"><span title="2020-11-20 02:26:36Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 2:26</span></a></span> <span title="this comment was edited 1 time"><svg aria-hidden="true" class="va-text-bottom o50 svg-icon iconPencilSm" width="14" height="14" viewbox="0 0 14 14">
|
||
<path d="M11.1 1.71l1.13 1.12c.2.2.2.51 0 .71L11.1 4.7 9.21 2.86l1.17-1.15c.2-.2.51-.2.71 0zM2 10.12l6.37-6.43 1.88 1.88L3.88 12H2v-1.88z"></path></svg></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-955977" class="comment js-comment" data-comment-id="955977">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="warm">8</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">I'd agree that this doesn't really answer the asked question. It also contains some errors/questionable statements. C has types. Type reconstruction for unannotated System F terms is undecidable, but (partially) annotated terms can be used instead. Intensional type theory is not necessarily the same as homotopy type theory. And merely saying that set theory is 'untyped' does not really explain why machine checking formal set theory proofs would be inferior to machine checking type theoretic constructions.</span> – <a href="/users/5880/dan-doel" title="285 reputation" class="comment-user">Dan Doel</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment955977_376936"><span title="2020-11-20 02:54:15Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 2:54</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-955979" class="comment js-comment" data-comment-id="955979">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="cool">2</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">Modulo some issues pointed out by Dan Doel, I think that this answer pretty accurately articulates what I'd call the "standard criticism of set theory" as a basis for proof assistants. In other words, it answers the closely related question, "If you ask people why dependent type theory is better than set theory for proof assistants, what kind of answer will you likely get?"</span> – <a href="/users/3106/timothy-chow" title="54,451 reputation" class="comment-user">Timothy Chow</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment955979_376936"><span title="2020-11-20 03:07:13Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 3:07</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956172" class="comment js-comment" data-comment-id="956172">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="cool">2</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">To own up entirely to my flaws here (or at least to my flaws as manifested here), I didn't read the whole answer before commenting, and I'm sorry. I saw that the beginning was generalities on typing, the end was focussed on machine language, and there was a highlighted comparison of non-proof assistant programming languages, and I missed the four paragraphs that really get at the question. The answer to "do you think explanatory text is a little too old-fashioned" is "no, but, for me, it distracted from the part of the text that answered the question."</span> – <a href="/users/2383/lspice" title="5,123 reputation" class="comment-user">LSpice</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956172_376936"><span title="2020-11-20 18:11:22Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 20 '20 at 18:11</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
<li id="comment-956412" class="comment js-comment" data-comment-id="956412">
|
||
<div class="js-comment-actions comment-actions">
|
||
<div class="comment-score js-comment-edit-hide">
|
||
<span title="number of 'useful comment' votes received" class="cool">1</span>
|
||
</div>
|
||
</div>
|
||
<div class="comment-text js-comment-text-and-form">
|
||
<div class="comment-body js-comment-edit-hide">
|
||
<span class="comment-copy">@none Well, I didn't say there are no reasons to prefer type theory over set theory. Personally I do (though I'm not a mathematician, so I guess I don't count). Andrej Bauer's answer is great, and explains some aspects of why type theory would be preferred. What I said is that <i>this</i> answer doesn't. I'm not sure how anyone would deduce the $3 \subset 5$ example from it without already knowing about that, for instance. Perhaps that was intended by talk of "safety," but that just comes off as one of the several erroneous analogies, since proof checking is analogous to type checking.</span> – <a href="/users/5880/dan-doel" title="285 reputation" class="comment-user">Dan Doel</a> <span class="comment-date" dir="ltr"><a class="comment-link" href="#comment956412_376936"><span title="2020-11-21 16:24:20Z, License: CC BY-SA 4.0" class="relativetime-clean">Nov 21 '20 at 16:24</span></a></span>
|
||
</div>
|
||
</div>
|
||
</li>
|
||
</ul>
|
||
</div>
|
||
<div id="comments-link-376936" data-rep="50" data-anon="true">
|
||
<a class="js-show-link comments-link" title="expand to show all comments on this post" href="#" onclick="" role="button">show <b>1</b> more comment</a>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div><a name="new-answer" id="new-answer"></a>
|
||
<form id="post-form" action="/questions/376839/answer/submit" method="post" class="js-add-answer-component post-form" name="post-form">
|
||
<h2 class="space">
|
||
Your Answer
|
||
</h2>
|
||
<script>
|
||
<![CDATA[
|
||
StackExchange.ready(function() {
|
||
var channelOptions = {
|
||
tags: "".split(" "),
|
||
id: "504"
|
||
};
|
||
initTagRenderer("".split(" "), "".split(" "), channelOptions);
|
||
|
||
StackExchange.using("externalEditor", function() {
|
||
// Have to fire editor after snippets, if snippets enabled
|
||
if (StackExchange.settings.snippets.snippetsEnabled) {
|
||
StackExchange.using("snippets", function() {
|
||
createEditor();
|
||
});
|
||
}
|
||
else {
|
||
createEditor();
|
||
}
|
||
});
|
||
|
||
function createEditor() {
|
||
StackExchange.prepareEditor({
|
||
useStacksEditor: false,
|
||
heartbeatType: 'answer',
|
||
autoActivateHeartbeat: false,
|
||
convertImagesToLinks: true,
|
||
noModals: true,
|
||
showLowRepImageUploadWarning: true,
|
||
reputationToPostImages: 10,
|
||
bindNavPrevention: true,
|
||
postfix: "",
|
||
imageUploader: {
|
||
brandingHtml: "Powered by \u003ca href=\"https://imgur.com/\"\u003e\u003csvg class=\"svg-icon\" width=\"50\" height=\"18\" viewBox=\"0 0 50 18\" fill=\"none\" xmlns=\"http://www.w3.org/2000/svg\"\u003e\u003cpath d=\"M46.1709 9.17788C46.1709 8.26454 46.2665 7.94324 47.1084 7.58816C47.4091 7.46349 47.7169 7.36433 48.0099 7.26993C48.9099 6.97997 49.672 6.73443 49.672 5.93063C49.672 5.22043 48.9832 4.61182 48.1414 4.61182C47.4335 4.61182 46.7256 4.91628 46.0943 5.50789C45.7307 4.9328 45.2525 4.66231 44.6595 4.66231C43.6264 4.66231 43.1481 5.28821 43.1481 6.59048V11.9512C43.1481 13.2535 43.6264 13.8962 44.6595 13.8962C45.6924 13.8962 46.1709 13.2535 46.1709 11.9512V9.17788Z\"/\u003e\u003cpath d=\"M32.492 10.1419C32.492 12.6954 34.1182 14.0484 37.0451 14.0484C39.9723 14.0484 41.5985 12.6954 41.5985 10.1419V6.59049C41.5985 5.28821 41.1394 4.66232 40.1061 4.66232C39.0732 4.66232 38.5948 5.28821 38.5948 6.59049V9.60062C38.5948 10.8521 38.2696 11.5455 37.0451 11.5455C35.8209 11.5455 35.4954 10.8521 35.4954 9.60062V6.59049C35.4954 5.28821 35.0173 4.66232 34.0034 4.66232C32.9703 4.66232 32.492 5.28821 32.492 6.59049V10.1419Z\" /\u003e\u003cpath fill-rule=\"evenodd\" clip-rule=\"evenodd\" d=\"M25.6622 17.6335C27.8049 17.6335 29.3739 16.9402 30.2537 15.6379C30.8468 14.7755 30.9615 13.5579 30.9615 11.9512V6.59049C30.9615 5.28821 30.4833 4.66231 29.4502 4.66231C28.9913 4.66231 28.4555 4.94978 28.1109 5.50789C27.499 4.86533 26.7335 4.56087 25.7005 4.56087C23.1369 4.56087 21.0134 6.57349 21.0134 9.27932C21.0134 11.9852 23.003 13.913 25.3754 13.913C26.5612 13.913 27.4607 13.4902 28.1109 12.6616C28.1109 12.7229 28.1161 12.7799 28.121 12.8346C28.1256 12.8854 28.1301 12.9342 28.1301 12.983C28.1301 14.4373 27.2502 15.2321 25.777 15.2321C24.8349 15.2321 24.1352 14.9821 23.5661 14.7787C23.176 14.6393 22.8472 14.5218 22.5437 14.5218C21.7977 14.5218 21.2429 15.0123 21.2429 15.6887C21.2429 16.7375 22.9072 17.6335 25.6622 17.6335ZM24.1317 9.27932C24.1317 7.94324 24.9928 7.09766 26.1024 7.09766C27.2119 7.09766 28.0918 7.94324 28.0918 9.27932C28.0918 10.6321 27.2311 11.5116 26.1024 11.5116C24.9737 11.5116 24.1317 10.6491 24.1317 9.27932Z\"/\u003e\u003cpath d=\"M16.8045 11.9512C16.8045 13.2535 17.2637 13.8962 18.2965 13.8962C19.3298 13.8962 19.8079 13.2535 19.8079 11.9512V8.12928C19.8079 5.82936 18.4879 4.62866 16.4027 4.62866C15.1594 4.62866 14.279 4.98375 13.3609 5.88013C12.653 5.05154 11.6581 4.62866 10.3573 4.62866C9.34336 4.62866 8.57809 4.89931 7.9466 5.5079C7.58314 4.9328 7.10506 4.66232 6.51203 4.66232C5.47873 4.66232 5.00066 5.28821 5.00066 6.59049V11.9512C5.00066 13.2535 5.47873 13.8962 6.51203 13.8962C7.54479 13.8962 8.0232 13.2535 8.0232 11.9512V8.90741C8.0232 7.58817 8.44431 6.91179 9.53458 6.91179C10.5104 6.91179 10.893 7.58817 10.893 8.94108V11.9512C10.893 13.2535 11.3711 13.8962 12.4044 13.8962C13.4375 13.8962 13.9157 13.2535 13.9157 11.9512V8.90741C13.9157 7.58817 14.3365 6.91179 15.4269 6.91179C16.4027 6.91179 16.8045 7.58817 16.8045 8.94108V11.9512Z\"/\u003e\u003cpath d=\"M3.31675 6.59049C3.31675 5.28821 2.83866 4.66232 1.82471 4.66232C0.791758 4.66232 0.313354 5.28821 0.313354 6.59049V11.9512C0.313354 13.2535 0.791758 13.8962 1.82471 13.8962C2.85798 13.8962 3.31675 13.2535 3.31675 11.9512V6.59049Z\" /\u003e\u003cpath d=\"M1.87209 0.400291C0.843612 0.400291 0 1.1159 0 1.98861C0 2.87869 0.822846 3.57676 1.87209 3.57676C2.90056 3.57676 3.7234 2.87869 3.7234 1.98861C3.7234 1.1159 2.90056 0.400291 1.87209 0.400291Z\" fill=\"#1BB76E\"/\u003e\u003c/svg\u003e\u003c/a\u003e",
|
||
contentPolicyHtml: "User contributions licensed under \u003ca href=\"https://stackoverflow.com/help/licensing\"\u003ecc by-sa\u003c/a\u003e \u003ca href=\"https://stackoverflow.com/legal/content-policy\"\u003e(content policy)\u003c/a\u003e",
|
||
allowUrls: true
|
||
},
|
||
noCode: true, onDemand: true,
|
||
discardSelector: ".discard-answer"
|
||
,immediatelyShowMarkdownHelp:true,enableTables:true
|
||
});
|
||
}
|
||
});
|
||
]]>
|
||
</script>
|
||
<div id="post-editor" class="post-editor js-post-editor">
|
||
<div class="ps-relative">
|
||
<div class="wmd-container mb8">
|
||
<div id="wmd-button-bar" class="wmd-button-bar btr-sm">
|
||
<ul id="wmd-button-row" class="wmd-button-row">
|
||
<li id="wmd-bold-button" class="wmd-button" style="left: 0px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
<li id="wmd-italic-button" class="wmd-button" style="left: 25px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
<li id="wmd-spacer1" class="wmd-spacer" style="left: 50px;"></li>
|
||
<li id="wmd-link-button" class="wmd-button" style="left: 75px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
<li id="wmd-quote-button" class="wmd-button" style="left: 100px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
<li id="wmd-code-button" class="wmd-button" style="left: 125px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
<li id="wmd-image-button" class="wmd-button" style="left: 150px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
<li id="wmd-spacer2" class="wmd-spacer" style="left: 175px;"></li>
|
||
<li id="wmd-olist-button" class="wmd-button" style="left: 200px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
<li id="wmd-ulist-button" class="wmd-button" style="left: 225px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
<li id="wmd-heading-button" class="wmd-button" style="left: 250px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
<li id="wmd-hr-button" class="wmd-button" style="left: 275px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
<li id="wmd-spacer3" class="wmd-spacer" style="left: 300px;"></li>
|
||
<li id="wmd-undo-button" class="wmd-button" style="left: 325px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
<li id="wmd-redo-button" class="wmd-button" style="left: 350px;">
|
||
<img src="https://cdn.sstatic.net/Img/unified/wmd-buttons.svg?v=c26278fc22d9" />
|
||
</li>
|
||
</ul>
|
||
</div>
|
||
<div class="js-stacks-validation">
|
||
<div class="ps-relative">
|
||
<textarea id="wmd-input" name="post-text" class="wmd-input s-input bar0 js-post-body-field" data-post-type-id="2" cols="92" rows="15" tabindex="101" data-min-length=""></textarea>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div id="wmd-preview" class="s-prose mb16 wmd-preview js-wmd-preview"></div>
|
||
</div>
|
||
<div class="ps-relative">
|
||
<div class="form-item new-post-login p0 my16">
|
||
<div class="grid gs16 md:fd-column new-login-form">
|
||
<div class="grid fd-column w50 md:w-auto gsy gs8 jc-space-between new-login-left">
|
||
<h3 class="grid--cell fs-title">
|
||
Sign up or <a id="login-link" href="/users/login?ssrc=question_page&returnurl=https%3a%2f%2fmathoverflow.net%2fquestions%2f376839%2fwhat-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista%23new-answer">log in</a>
|
||
</h3>
|
||
<script>
|
||
<![CDATA[
|
||
StackExchange.ready(function () {
|
||
StackExchange.helpers.onClickDraftSave('#login-link');
|
||
});
|
||
]]>
|
||
</script>
|
||
<div class="grid--cell s-btn s-btn__muted s-btn__outlined s-btn__icon google-login" data-ga="["sign up","Sign Up Started - Google","New Post",null,null]">
|
||
<svg aria-hidden="true" class="native svg-icon iconGoogle" width="18" height="18" viewbox="0 0 18 18">
|
||
<path d="M16.51 8H8.98v3h4.3c-.18 1-.74 1.48-1.6 2.04v2.01h2.6a7.8 7.8 0 002.38-5.88c0-.57-.05-.66-.15-1.18z" fill="#4285F4"></path>
|
||
<path d="M8.98 17c2.16 0 3.97-.72 5.3-1.94l-2.6-2a4.8 4.8 0 01-7.18-2.54H1.83v2.07A8 8 0 008.98 17z" fill="#34A853"></path>
|
||
<path d="M4.5 10.52a4.8 4.8 0 010-3.04V5.41H1.83a8 8 0 000 7.18l2.67-2.07z" fill="#FBBC05"></path>
|
||
<path d="M8.98 4.18c1.17 0 2.23.4 3.06 1.2l2.3-2.3A8 8 0 001.83 5.4L4.5 7.49a4.77 4.77 0 014.48-3.3z" fill="#EA4335"></path></svg> Sign up using Google
|
||
</div>
|
||
<div class="grid--cell s-btn s-btn__muted s-btn__icon facebook-login" data-ga="["sign up","Sign Up Started - Facebook","New Post",null,null]">
|
||
<svg aria-hidden="true" class="svg-icon iconFacebook" width="18" height="18" viewbox="0 0 18 18">
|
||
<path d="M3 1a2 2 0 00-2 2v12c0 1.1.9 2 2 2h12a2 2 0 002-2V3a2 2 0 00-2-2H3zm6.55 16v-6.2H7.46V8.4h2.09V6.61c0-2.07 1.26-3.2 3.1-3.2.88 0 1.64.07 1.87.1v2.16h-1.29c-1 0-1.19.48-1.19 1.18V8.4h2.39l-.31 2.42h-2.08V17h-2.5z" fill="#4167B2"></path></svg> Sign up using Facebook
|
||
</div>
|
||
<div class="grid--cell s-btn s-btn__muted s-btn__outlined s-btn__icon stackexchange-login" data-ga="["sign up","Sign Up Navigation","New Post",null,null]">
|
||
<svg aria-hidden="true" class="native svg-icon iconLogoGlyphXSm" width="18" height="18" viewbox="0 0 18 18">
|
||
<path d="M14 16v-5h2v7H2v-7h2v5h10z" fill="#BCBBBB"></path>
|
||
<path d="M12.09.72l-1.21.9 4.5 6.07 1.22-.9L12.09.71zM5 15h8v-2H5v2zm9.15-5.87L8.35 4.3l.96-1.16 5.8 4.83-.96 1.16zm-7.7-1.47l6.85 3.19.63-1.37-6.85-3.2-.63 1.38zm6.53 5L5.4 11.39l.38-1.67 7.42 1.48-.22 1.46z" fill="#F48024"></path></svg> Sign up using Email and Password
|
||
</div>
|
||
</div>
|
||
<div class="grid gsy gs8 fd-column w50 md:w-auto new-login-right form-item p0">
|
||
<h3 class="grid--cell fs-title">
|
||
Post as a guest
|
||
</h3>
|
||
<div class="grid--cell">
|
||
<div class="grid gs4 gsy fd-column">
|
||
<label class="s-label" for="display-name">Name</label>
|
||
<div class="grid ps-relative">
|
||
<input class="s-input" id="display-name" name="display-name" maxlength="30" type="text" value="" tabindex="105" placeholder="" />
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<div class="grid gs4 gsy fd-column">
|
||
<div class="grid--cell">
|
||
<div class="grid gs2 gsy fd-column">
|
||
<label class="grid--cell s-label" for="m-address">Email</label>
|
||
<p class="grid--cell s-description">
|
||
Required, but never shown
|
||
</p>
|
||
</div>
|
||
</div>
|
||
<div class="grid ps-relative">
|
||
<input class="s-input js-post-email-field" id="m-address" name="m-address" type="text" value="" size="40" tabindex="106" placeholder="" />
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<script>
|
||
<![CDATA[
|
||
StackExchange.ready(
|
||
function () {
|
||
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f376839%2fwhat-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista%23new-answer', 'question_page');
|
||
}
|
||
);
|
||
]]>
|
||
</script> <noscript>
|
||
<h3 class="grid--cell fs-title">
|
||
Post as a guest
|
||
</h3>
|
||
<div class="grid--cell">
|
||
<div class="grid gs4 gsy fd-column">
|
||
<label class="s-label" for="display-name">Name</label>
|
||
<div class="grid ps-relative">
|
||
<input class="s-input" id="display-name" name="display-name" maxlength="30" type="text" value="" tabindex="105" placeholder="" />
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="grid--cell">
|
||
<div class="grid gs4 gsy fd-column">
|
||
<div class="grid--cell">
|
||
<div class="grid gs2 gsy fd-column">
|
||
<label class="grid--cell s-label" for="m-address">Email</label>
|
||
<p class="grid--cell s-description">
|
||
Required, but never shown
|
||
</p>
|
||
</div>
|
||
</div>
|
||
<div class="grid ps-relative">
|
||
<input class="s-input js-post-email-field" id="m-address" name="m-address" type="text" value="" size="40" tabindex="106" placeholder="" />
|
||
</div>
|
||
</div>
|
||
</div></noscript>
|
||
</div>
|
||
<div class="form-submit cbt grid gsx gs4">
|
||
<button id="submit-button" class="grid--cell s-btn s-btn__primary s-btn__icon" type="submit" tabindex="120" autocomplete="off">Post Your Answer</button>
|
||
<p class="privacy-policy-agreement">
|
||
By clicking “Post Your Answer”, you agree to our <a href="https://stackoverflow.com/legal/terms-of-service/public" name="tos" target="_blank" class="-link" id="tos">terms of service</a>, <a href="https://stackoverflow.com/legal/privacy-policy" name="privacy" target="_blank" class="-link" id="privacy">privacy policy</a> and <a href="https://stackoverflow.com/legal/cookie-policy" name="cookie" target="_blank" class="-link" id="cookie">cookie policy</a>
|
||
</p>
|
||
</div>
|
||
</form>
|
||
<h2 class="bottom-notice" data-loc="1">
|
||
Not the answer you're looking for? Browse other questions tagged <a href="/questions/tagged/set-theory" class="post-tag" title="show questions tagged 'set-theory'" rel="tag">set-theory</a> <a href="/questions/tagged/soft-question" class="post-tag" title="show questions tagged 'soft-question'" rel="tag">soft-question</a> <a href="/questions/tagged/foundations" class="post-tag" title="show questions tagged 'foundations'" rel="tag">foundations</a> <a href="/questions/tagged/type-theory" class="post-tag" title="show questions tagged 'type-theory'" rel="tag">type-theory</a> <a href="/questions/tagged/proof-assistants" class="post-tag" title="show questions tagged 'proof-assistants'" rel="tag">proof-assistants</a> or <a href="/questions/ask">ask your own question</a>.
|
||
</h2>
|
||
</div>
|
||
</div>
|
||
<div id="sidebar" class="show-votes" role="complementary" aria-label="sidebar">
|
||
<div class="js-sidebar-zone"></div>
|
||
<div class="module sidebar-linked">
|
||
<h4 id="h-linked">
|
||
Linked
|
||
</h4>
|
||
<div class="linked" data-tracker="lq=1">
|
||
<div class="spacer js-gps-track" data-gps-track="linkedquestion.click({ source_post_id: 376839, target_question_id: 199926, position: 0 })">
|
||
<a href="https://mathoverflow.net/q/199926?lq=1" title="Vote score (upvotes - downvotes)">
|
||
<div class="answer-votes answered-accepted default">
|
||
81
|
||
</div></a> <a href="https://mathoverflow.net/questions/199926/parodies-of-abstruse-mathematical-writing?noredirect=1&lq=1" class="question-hyperlink">Parodies of abstruse mathematical writing</a>
|
||
</div>
|
||
<div class="spacer js-gps-track" data-gps-track="linkedquestion.click({ source_post_id: 376839, target_question_id: 311071, position: 1 })">
|
||
<a href="https://mathoverflow.net/q/311071?lq=1" title="Vote score (upvotes - downvotes)">
|
||
<div class="answer-votes large">
|
||
122
|
||
</div></a> <a href="https://mathoverflow.net/questions/311071/which-mathematical-definitions-should-be-formalised-in-lean?noredirect=1&lq=1" class="question-hyperlink">Which mathematical definitions should be formalised in Lean?</a>
|
||
</div>
|
||
<div class="spacer js-gps-track" data-gps-track="linkedquestion.click({ source_post_id: 376839, target_question_id: 378473, position: 2 })">
|
||
<a href="https://mathoverflow.net/q/378473?lq=1" title="Vote score (upvotes - downvotes)">
|
||
<div class="answer-votes default">
|
||
24
|
||
</div></a> <a href="https://mathoverflow.net/questions/378473/what-is-the-endgoal-of-formalising-mathematics?noredirect=1&lq=1" class="question-hyperlink">What is the endgoal of formalising mathematics?</a>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div class="module sidebar-related">
|
||
<h4 id="h-related">
|
||
Related
|
||
</h4>
|
||
<div class="related js-gps-related-questions" data-tracker="rq=1">
|
||
<div class="spacer js-gps-track">
|
||
<a href="https://mathoverflow.net/q/8260?rq=1" title="Vote score (upvotes - downvotes)">
|
||
<div class="answer-votes answered-accepted default">
|
||
40
|
||
</div></a> <a href="https://mathoverflow.net/questions/8260/proof-assistants-for-mathematics?rq=1" class="question-hyperlink">Proof assistants for mathematics</a>
|
||
</div>
|
||
<div class="spacer js-gps-track">
|
||
<a href="https://mathoverflow.net/q/19070?rq=1" title="Vote score (upvotes - downvotes)">
|
||
<div class="answer-votes answered-accepted default">
|
||
15
|
||
</div></a> <a href="https://mathoverflow.net/questions/19070/reference-request-for-type-theory?rq=1" class="question-hyperlink">Reference request for type theory</a>
|
||
</div>
|
||
<div class="spacer js-gps-track">
|
||
<a href="https://mathoverflow.net/q/152497?rq=1" title="Vote score (upvotes - downvotes)">
|
||
<div class="answer-votes default">
|
||
38
|
||
</div></a> <a href="https://mathoverflow.net/questions/152497/formalizations-of-category-theory-in-proof-assistants?rq=1" class="question-hyperlink">Formalizations of category theory in proof assistants</a>
|
||
</div>
|
||
<div class="spacer js-gps-track">
|
||
<a href="https://mathoverflow.net/q/235534?rq=1" title="Vote score (upvotes - downvotes)">
|
||
<div class="answer-votes default">
|
||
7
|
||
</div></a> <a href="https://mathoverflow.net/questions/235534/identity-types-what-makes-intuitionistic-type-theory-intuitionistic?rq=1" class="question-hyperlink">Identity types: What makes Intuitionistic Type Theory *intuitionistic*?</a>
|
||
</div>
|
||
<div class="spacer js-gps-track">
|
||
<a href="https://mathoverflow.net/q/286874?rq=1" title="Vote score (upvotes - downvotes)">
|
||
<div class="answer-votes answered-accepted default">
|
||
54
|
||
</div></a> <a href="https://mathoverflow.net/questions/286874/in-what-respect-are-univalent-foundations-better-than-set-theory?rq=1" class="question-hyperlink">In what respect are univalent foundations “better” than set theory?</a>
|
||
</div>
|
||
<div class="spacer js-gps-track">
|
||
<a href="https://mathoverflow.net/q/322020?rq=1" title="Vote score (upvotes - downvotes)">
|
||
<div class="answer-votes answered-accepted default">
|
||
6
|
||
</div></a> <a href="https://mathoverflow.net/questions/322020/how-can-the-simply-typed-lambda-calculus-be-turing-incomplete-yet-stronger-than?rq=1" class="question-hyperlink">How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?</a>
|
||
</div>
|
||
<div class="spacer js-gps-track">
|
||
<a href="https://mathoverflow.net/q/346225?rq=1" title="Vote score (upvotes - downvotes)">
|
||
<div class="answer-votes answered-accepted default">
|
||
3
|
||
</div></a> <a href="https://mathoverflow.net/questions/346225/why-bourbakis-epsilon-calculus-is-not-suitable-for-set-theory?rq=1" class="question-hyperlink">Why Bourbaki's epsilon-calculus is not suitable for set theory?</a>
|
||
</div>
|
||
<div class="spacer js-gps-track">
|
||
<a href="https://mathoverflow.net/q/353178?rq=1" title="Vote score (upvotes - downvotes)">
|
||
<div class="answer-votes default">
|
||
7
|
||
</div></a> <a href="https://mathoverflow.net/questions/353178/what-types-are-to-mathematical-proofs-as-types-%c3%a0-la-martin-l%c3%b6f-are-to-constructi?rq=1" class="question-hyperlink">What types are to mathematical proofs as types à la Martin-Löf are to constructive proofs, and what's wrong with them?</a>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<div id="feed-link" class="js-feed-link">
|
||
<a href="/feeds/question/376839" title="Feed of this question and its answers"><svg aria-hidden="true" class="fc-orange-400 svg-icon iconRss" width="18" height="18" viewbox="0 0 18 18">
|
||
<path d="M1 3c0-1.1.9-2 2-2h12a2 2 0 012 2v12a2 2 0 01-2 2H3a2 2 0 01-2-2V3zm14.5 12C15.5 8.1 9.9 2.5 3 2.5V5a10 10 0 0110 10h2.5zm-5 0A7.5 7.5 0 003 7.5V10a5 5 0 015 5h2.5zm-5 0A2.5 2.5 0 003 12.5V15h2.5z"></path></svg> Question feed</a>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<script>
|
||
<![CDATA[
|
||
StackExchange.ready(function(){$.get('/posts/376839/ivc/8b30');});
|
||
]]>
|
||
</script> <noscript>
|
||
<div>
|
||
<img src="/posts/376839/ivc/8b30" class="dno" alt="" width="0" height="0" />
|
||
</div></noscript>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
<footer id="footer" class="site-footer js-footer" role="contentinfo">
|
||
<div class="site-footer--container">
|
||
<nav class="site-footer--nav">
|
||
<div class="site-footer--col site-footer--col__visible js-footer-col" data-name="default">
|
||
<h5 class="-title">
|
||
<a href="/">MathOverflow</a>
|
||
</h5>
|
||
<ul class="-list js-primary-footer-links">
|
||
<li class="-item">
|
||
<a class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 2 })" href="/tour">Tour</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="/help" class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 3 })">Help</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 5 })" href="https://chat.stackexchange.com?tab=site&host=mathoverflow.net">Chat</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 13 })" href="/contact">Contact</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 14 })" href="https://meta.mathoverflow.net">Feedback</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a onclick="StackExchange.switchMobile("on")" class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 12 })">Mobile</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a class="-link" role="button">Disable Responsiveness</a>
|
||
</li>
|
||
</ul>
|
||
</div>
|
||
<div class="site-footer--col site-footer--col__visible js-footer-col" data-name="default">
|
||
<h5 class="-title">
|
||
<a class="js-gps-track" data-gps-track="footer.click({ location: 2, link: 1 })" href="https://stackoverflow.com/company">Company</a>
|
||
</h5>
|
||
<ul class="-list">
|
||
<li class="-item">
|
||
<a href="https://stackoverflow.com" class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 15})">Stack Overflow</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="https://stackoverflow.com/teams" class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 29 })">For Teams</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="https://stackoverflow.com/advertising" class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 21 })">Advertise With Us</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="https://stackoverflow.com/talent" class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 20 })">Hire a Developer</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="https://stackoverflow.com/jobs" class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 17})">Developer Jobs</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 1 })" href="https://stackoverflow.com/company">About</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 27 })" href="https://stackoverflow.com/company/press">Press</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 7 })" href="https://stackoverflow.com/legal">Legal</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 8 })" href="https://stackoverflow.com/legal/privacy-policy">Privacy Policy</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link: 37 })" href="https://stackoverflow.com/legal/terms-of-service">Terms of Service</a>
|
||
</li>
|
||
</ul>
|
||
</div>
|
||
<div class="site-footer--col site-footer--categories-nav site-footer--col__visible">
|
||
<div>
|
||
<h5 class="-title">
|
||
<a href="https://stackexchange.com" data-gps-track="footer.click({ location: 2, link: 30 })">Stack Exchange<br />
|
||
Network</a>
|
||
</h5>
|
||
<ul class="-list">
|
||
<li class="-item">
|
||
<a href="#" class="-link _expandable js-footer-category-trigger js-gps-track" data-gps-track="footer.click({ location: 2, link: 24 })" data-target="Technology">Technology</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="#" class="-link _expandable js-footer-category-trigger js-gps-track" data-gps-track="footer.click({ location: 2, link: 24 })" data-target="Life / Arts">Life / Arts</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="#" class="-link _expandable js-footer-category-trigger js-gps-track" data-gps-track="footer.click({ location: 2, link: 24 })" data-target="Culture / Recreation">Culture / Recreation</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="#" class="-link _expandable js-footer-category-trigger js-gps-track" data-gps-track="footer.click({ location: 2, link: 24 })" data-target="Science">Science</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="#" class="-link _expandable js-footer-category-trigger js-gps-track" data-gps-track="footer.click({ location: 2, link: 24 })" data-target="Other">Other</a>
|
||
</li>
|
||
</ul>
|
||
</div>
|
||
</div>
|
||
</nav>
|
||
<div class="site-footer--copyright fs-fine">
|
||
<ul class="-list">
|
||
<li class="-item">
|
||
<a class="js-gps-track -link" data-gps-track="footer.click({ location: 2, link:4 })" href="https://stackoverflow.blog?blb=1">Blog</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="https://www.facebook.com/officialstackoverflow/" class="-link js-gps-track" data-gps-track="footer.click({ location: 2, link: 31 })">Facebook</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="https://twitter.com/stackoverflow" class="-link js-gps-track" data-gps-track="footer.click({ location: 2, link: 32 })">Twitter</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="https://linkedin.com/company/stack-overflow" class="-link js-gps-track" data-gps-track="footer.click({ location: 2, link: 33 })">LinkedIn</a>
|
||
</li>
|
||
<li class="-item">
|
||
<a href="https://www.instagram.com/thestackoverflow" class="-link js-gps-track" data-gps-track="footer.click({ location: 2, link: 36 })">Instagram</a>
|
||
</li>
|
||
</ul>
|
||
<p class="mt-auto mb24">
|
||
site design / logo © 2021 Stack Exchange Inc; user contributions licensed under <a href="https://stackoverflow.com/help/licensing">cc by-sa</a>. <span id="svnrev">rev 2021.1.25.38392</span>
|
||
</p>
|
||
</div>
|
||
</div>
|
||
</footer>
|
||
<script>
|
||
<![CDATA[
|
||
StackExchange.ready(function () { StackExchange.responsiveness.addSwitcher(); })
|
||
]]>
|
||
</script> <noscript>
|
||
<div id="noscript-warning">
|
||
MathOverflow works best with JavaScript enabled <img src="https://pixel.quantserve.com/pixel/p-c1rF4kxgLUzNc.gif" alt="" class="dno" />
|
||
</div></noscript>
|
||
<script>
|
||
<![CDATA[
|
||
|
||
(function(i, s, o, g, r, a, m) {
|
||
i['GoogleAnalyticsObject'] = r; i[r] = i[r] || function() { (i[r].q = i[r].q || []).push(arguments) }, i[r].l = 1 * new Date(); a = s.createElement(o),
|
||
m = s.getElementsByTagName(o)[0]; a.async = 1; a.src = g; m.parentNode.insertBefore(a, m);
|
||
})(window, document, 'script', 'https://www.google-analytics.com/analytics.js', 'ga');
|
||
|
||
StackExchange.ready(function () {
|
||
|
||
StackExchange.ga.init({
|
||
autoLink: ["stackoverflow.blog","info.stackoverflowsolutions.com","stackoverflowsolutions.com"],
|
||
sendTitles: true,
|
||
tracker: window.ga,
|
||
trackingCodes: [
|
||
'UA-108242619-5'
|
||
],
|
||
checkDimension: 'dimension42'
|
||
});
|
||
|
||
|
||
|
||
StackExchange.ga.setDimension('dimension2', '|set-theory|soft-question|foundations|type-theory|proof-assistants|');
|
||
|
||
StackExchange.ga.setDimension('dimension3', 'Questions/Show');
|
||
|
||
|
||
StackExchange.ga.trackPageView();
|
||
});
|
||
|
||
var _qevents = _qevents || [],
|
||
_comscore = _comscore || [];
|
||
(function() {
|
||
var s = document.getElementsByTagName('script')[0],
|
||
qc = document.createElement('script');
|
||
qc.async = true;
|
||
qc.src = 'https://secure.quantserve.com/quant.js';
|
||
s.parentNode.insertBefore(qc, s);
|
||
_qevents.push({ qacct: "p-c1rF4kxgLUzNc" }); var sc = document.createElement('script');
|
||
sc.async = true;
|
||
sc.src = 'https://sb.scorecardresearch.com/beacon.js';
|
||
s.parentNode.insertBefore(sc, s);
|
||
_comscore.push({ c1: "2", c2: "17440561" }); })();
|
||
]]>
|
||
</script>
|
||
</body>
|
||
</html>
|