CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> constructive mathematics in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> constructive mathematics </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/13375/#Item_13" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Constructive mathematics</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="foundations">Foundations</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundations">foundations</a></strong></p> <h2 id="the_basis_of_it_all">The basis of it all</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/mathematical+logic">mathematical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/deduction+system">deduction system</a>, <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a>, <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>, <a class="existingWikiWord" href="/nlab/show/lambda-calculus">lambda-calculus</a>, <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/simple+type+theory">simple type theory</a>, <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/collection">collection</a>, <a class="existingWikiWord" href="/nlab/show/object">object</a>, <a class="existingWikiWord" href="/nlab/show/type">type</a>, <a class="existingWikiWord" href="/nlab/show/term">term</a>, <a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equality">equality</a>, <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a>, <a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a></p> </li> </ul> <h2 id="set_theory"> Set theory</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></strong></p> <ul> <li>fundamentals of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/typed+predicate+logic">typed predicate logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></li> <li><a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a>, <a class="existingWikiWord" href="/nlab/show/function">function</a>, <a class="existingWikiWord" href="/nlab/show/relation">relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/small+set">small set</a>, <a class="existingWikiWord" href="/nlab/show/large+set">large set</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a>, <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/pairing+structure">pairing structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/union+structure">union structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> <li><a class="existingWikiWord" href="/nlab/show/powerset+structure">powerset structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/natural+numbers+structure">natural numbers structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> </ul> </li> <li>presentations of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+set+theory">first-order set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/one-sorted+set+theory">one-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/two-sorted+set+theory">two-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/three-sorted+set+theory">three-sorted set theory</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a></li> </ul> </li> <li>structuralism in set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></li> <li><a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/New+Foundations">New Foundations</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/categorical+set+theory">categorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">Trimble on ETCS I</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">Trimble on ETCS II</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">Trimble on ETCS III</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/allegorical+set+theory">allegorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a></li> </ul> </li> </ul> </li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/class-set+theory">class-set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/class">class</a>, <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a></li> <li><a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a>, <a class="existingWikiWord" href="/nlab/show/universe">universe</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/constructive+set+theory">constructive set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></li> </ul> </div> <h2 id="foundational_axioms">Foundational axioms</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundational+axiom">foundational</a> <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a></strong></p> <ul> <li> <p>basic constructions:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+cartesian+products">axiom of cartesian products</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+disjoint+unions">axiom of disjoint unions</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+the+empty+set">axiom of the empty set</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+fullness">axiom of fullness</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+function+sets">axiom of function sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+quotient+sets">axiom of quotient sets</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material+set+theory">material axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski%27s+axiom">Mostowski's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+transitive+closure">axiom of transitive closure</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+materialization">axiom of materialization</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theoretic axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axioms+of+set+truncation">axioms of set truncation</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a></li> <li><a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/equality+reflection">equality reflection</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+circle+type+localization">axiom of circle type localization</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theoretic axioms</a>: <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+principle">Whitehead's principle</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axioms+of+choice">axioms of choice</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+countable+choice">axiom of countable choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+dependent+choice">axiom of dependent choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+existence">axiom of existence</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/Markov%27s+axiom">Markov's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/small+cardinality+selection+axiom">small cardinality selection axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+small+violations+of+choice">axiom of small violations of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+weakly+initial+sets+of+covers">axiom of weakly initial sets of covers</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/large+cardinal+axioms">large cardinal axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+universes">axiom of universes</a></li> <li><a class="existingWikiWord" href="/nlab/show/regular+extension+axiom">regular extension axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/measurable+cardinal">measurable cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/elementary+embedding">elementary embedding</a></li> <li><a class="existingWikiWord" href="/nlab/show/supercompact+cardinal">supercompact cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/Vop%C4%9Bnka%27s+principle">Vopěnka's principle</a></li> </ul> </li> <li> <p>strong axioms</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a></li> </ul> </li> <li> <p>further</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/reflection+principle">reflection principle</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+tight+apartness">axiom of tight apartness</a></p> </li> </ul> </div> <h2 id="removing_axioms">Removing axioms</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> </ul> <div> <p> <a href="/nlab/edit/foundations+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="mathematics">Mathematics</h4> <div class="hide"><div> <ul> <li> <p><strong><a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/math+resources">math resources</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/history+of+mathematics">history of mathematics</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/foundations">Structural Foundations</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/logic">logic</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/internal+language">internal language</a></li> <li><a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> <li><a href="http://ncatlab.org/nlab/list/foundational+axiom">category:foundational axiom</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Categories+and+Sheaves">Categories and Sheaves</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topos+theory">topos theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Sheaves+in+Geometry+and+Logic">Sheaves in Geometry and Logic</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+topos+theory">higher topos theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Higher+Topos+Theory">(∞,1)-topos theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/models+for+%E2%88%9E-stack+%28%E2%88%9E%2C1%29-toposes">models for ∞-stack (∞,1)-toposes</a></li> <li><a class="existingWikiWord" href="/nlab/show/cohomology">cohomology</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/stable+homotopy+theory">stable homotopy theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/rational+homotopy+theory">rational homotopy theory</a></li> </ul> </li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topology+and+geometry">Topology and Geometry</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/geometry">geometry</a> (general list), <a class="existingWikiWord" href="/nlab/show/topology">topology</a> (general list)</li> <li><a class="existingWikiWord" href="/nlab/show/general+topology">general topology</a></li> <li><a class="existingWikiWord" href="/nlab/show/differential+topology">differential topology</a></li> <li><a class="existingWikiWord" href="/nlab/show/differential+geometry">differential geometry</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/synthetic+differential+geometry">synthetic differential geometry</a></li> <li><a class="existingWikiWord" href="/nlab/show/symplectic+geometry">symplectic geometry</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+geometry">algebraic geometry</a></li> <li><a class="existingWikiWord" href="/nlab/show/noncommutative+algebraic+geometry">noncommutative algebraic geometry</a></li> <li><a class="existingWikiWord" href="/nlab/show/noncommutative+geometry">noncommutative geometry</a> (general flavour)</li> <li><a class="existingWikiWord" href="/nlab/show/higher+geometry">higher geometry</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/algebra">Algebra</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/universal+algebra">universal algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+algebra">higher algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homological+algebra">homological algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/group+theory">group theory</a>, <a class="existingWikiWord" href="/nlab/show/ring+theory">ring theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/representation+theory">representation theory</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/algebraic+approaches+to+differential+calculus">algebraic approaches to differential calculus</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/counterexamples+in+algebra">counterexamples in algebra</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/analysis">analysis</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/nonstandard+analysis">nonstandard analysis</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functional+analysis">functional analysis</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/operator+algebras">operator algebras</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Fourier+transform">Fourier transform</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Lie+theory">Lie theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/infinity-Lie+theory+-+contents">higher Lie theory</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/probability+theory">probability theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/discrete+mathematics">discrete mathematics</a></p> </li> </ul> </div></div> <h4 id="constructivism_realizability_computability">Constructivism, Realizability, Computability</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></strong>, <strong><a class="existingWikiWord" href="/nlab/show/realizability">realizability</a></strong>, <strong><a class="existingWikiWord" href="/nlab/show/computability">computability</a></strong></p> <p><a class="existingWikiWord" href="/nlab/show/intuitionistic+mathematics">intuitionistic mathematics</a></p> <p><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>, <a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>, <a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></p> <h3 id="constructive_mathematics">Constructive mathematics</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/topos">topos</a>, <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-topos">homotopy topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/canonical+form">canonical form</a>, <a class="existingWikiWord" href="/nlab/show/univalence">univalence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>, <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/decidable+equality">decidable equality</a>, <a class="existingWikiWord" href="/nlab/show/decidable+subset">decidable subset</a>, <a class="existingWikiWord" href="/nlab/show/inhabited+set">inhabited set</a>, <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></p> </li> </ul> <h3 id="realizability">Realizability</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+topos">realizability topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+model">realizability model</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+interpretation">realizability interpretation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/effective+topos">effective topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kleene%27s+first+algebra">Kleene's first algebra</a>, <a class="existingWikiWord" href="/nlab/show/Kleene%27s+second+algebra">Kleene's second algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/function+realizability">function realizability</a></p> </li> </ul> <h3 id="computability">Computability</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/computability">computability</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computation">computation</a>, <a class="existingWikiWord" href="/nlab/show/computational+type+theory">computational type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+function">computable function</a>, <a class="existingWikiWord" href="/nlab/show/partial+recursive+function">partial recursive function</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+analysis">computable analysis</a>, <a class="existingWikiWord" href="/nlab/show/constructive+analysis">constructive analysis</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Type+Two+Theory+of+Effectivity">Type Two Theory of Effectivity</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+function+%28analysis%29">computable function (analysis)</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/exact+real+computer+arithmetic">exact real computer arithmetic</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+set">computable set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/persistent+homology">persistent homology</a>, <a class="existingWikiWord" href="/nlab/show/effective+homology">effective homology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+physics">computable physics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Church-Turing+thesis">Church-Turing thesis</a></p> </li> </ul> </div></div> </div> </div> <h1 id="constructive_mathematics">Constructive mathematics</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#OriginsAndSchools'>Origins and schools</a></li> <li><a href='#topos_theory'>Topos theory</a></li> <li><a href='#some_features_of_constructive_mathematics'>Some features of constructive mathematics</a></li> <ul> <li><a href='#rephrasing_of_classical_ideas'>Rephrasing of classical ideas</a></li> <li><a href='#bifurcation_of_notions'>Bifurcation of notions</a></li> <li><a href='#negative_translation'>Negative translation</a></li> <li><a href='#truevassert'>Truth versus assertability</a></li> </ul> <li><a href='#prehistory'>Prehistory</a></li> <li><a href='#related_entries'>Related entries</a></li> <li><a href='#References'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>Broadly speaking, <strong>constructive mathematics</strong> is <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a> done without the <a class="existingWikiWord" href="/nlab/show/principle+of+excluded+middle">principle of excluded middle</a>, or other principles, such as the full <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>, that imply it, hence without “non-constructive” methods of <a class="existingWikiWord" href="/nlab/show/formal+proof">formal proof</a>, such as <a class="existingWikiWord" href="/nlab/show/proof+by+contradiction">proof by contradiction</a>. This is in contrast to <em><a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a></em>, where such principles are taken to hold.</p> <p>There are variations of what exactly is regarded as constructive mathematics, for instance <a class="existingWikiWord" href="/nlab/show/intuitionistic+mathematics">intuitionism</a> or <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicativism</a>, see the list of schools <a href="#OriginsAndSchools">below</a>. But beware the ambiguity in terminology: In <a class="existingWikiWord" href="/nlab/show/Brouwer">Brouwer</a>-style <a class="existingWikiWord" href="/nlab/show/intuitionistic+mathematics">intuitionistic mathematics</a> one includes <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a> that <em><a class="existingWikiWord" href="/nlab/show/contradiction">contradict</a></em> <a class="existingWikiWord" href="/nlab/show/classical+logic">classical logic</a>, while other authors use “intuitionistic” to mean what elsewhere is called “constructive”, and referring only to rejection of <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a> and <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">choice</a>. Some authors (particularly <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theorists</a>) use “constructive” to mean <em><a class="existingWikiWord" href="/nlab/show/predicative">predicative</a></em> constructive and “intuitionistic” to mean impredicative constructive. Other authors emphasize the necessity that constructive theories be <a class="existingWikiWord" href="/nlab/show/proof+relevance">proof relevant</a>, with denial of the excluded middle’s universality subordinate to this requirement; see (<a href="#Harper13">Harper 2013</a>).</p> <p><strong>Constructivism</strong> is the philosophy that such mathematics is useful, or (more strongly) that non-constructive mathematics is wrong. Historically, constructive mathematics was first pursued explicitly by mathematicians who believed the latter. However, many modern mathematicians who do constructive mathematics do it not because of any philosophical belief about the wrongness of non-constructive mathematics, but because constructive mathematics is interesting in its own right. In the ‘<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.93.9892">pluralist</a>’ approach to the <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> of mathematics, a constructive proof (when it exists) is better because it is valid in more versions of mathematics, but a classical proof remains valid for <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a>.</p> <p>Another motivation for modern mathematicians —especially category theorists like those on the nLab— is that the study of constructive mathematics has potential applications to non-constructive mathematics. For example, even if one believes the principle of excluded middle to be true, the “<a class="existingWikiWord" href="/nlab/show/internal+logic">internal</a>” version of excluded middle in many interesting <a class="existingWikiWord" href="/nlab/show/category">categories</a> is still false; thus constructive mathematics can be useful in the study of such categories, even if mathematics is “globally” non-constructive. This is the neutral motivation for constructive mathematics from the <a href="/nlab/show/nPOV#Logic">nPOV</a>.</p> <p>Here we write mostly about the mathematics, trying to be mostly neutral philosophically.</p> <h2 id="OriginsAndSchools">Origins and schools</h2> <p>During the “<a class="existingWikiWord" href="/nlab/show/foundations">foundational</a> crisis” in mathematics around the beginning of the 20th century, a number of mathematicians espoused philosophies that are generally grouped together and labeled <strong>constructivist</strong>. The common feature of these philosophies was a rejection of axioms and principles of logic that lead to nonconstructive proofs. There was much talk at the time about potential vs absolute infinity, but from an axiomatic perspective, it turns out that (if one stops short of finitism) the two main culprits are</p> <ul> <li> <p>the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> and</p> </li> <li> <p>the principle of <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>.</p> </li> </ul> <p>Thus, constructivists (including many still active today) reject proofs that make use of either of these. (In fact, it was realized in 1975 by Diaconescu that the axiom of choice implies the principle of excluded middle. Excluded middle is precisely the “finitely indexed” axiom of choice; see <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a> for a proof.)</p> <p>There are, however, differences among constructivists as well, even discounting the pluralists.</p> <ul> <li> <p>Some, like <a class="existingWikiWord" href="/nlab/show/Fred+Richman">Fred Richman</a> (see (Richman 2000)), simply remove choice and excluded middle from <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a> with nothing to replace them. This is called <a class="existingWikiWord" href="/nlab/show/neutral+constructive+mathematics">neutral constructive mathematics</a>. However, this makes it difficult to define a satisfactory notion of <a class="existingWikiWord" href="/nlab/show/continuous+function">continuous function</a>, even from the <a class="existingWikiWord" href="/nlab/show/real+line">real line</a> to itself, without using <a class="existingWikiWord" href="/nlab/show/locales">locales</a>; see (Waaldijk 2003).</p> </li> <li> <p>Others accept weaker versions of choice, such as <a class="existingWikiWord" href="/nlab/show/countable+choice">countable choice</a> or even <a class="existingWikiWord" href="/nlab/show/dependent+choice">dependent choice</a>. <a class="existingWikiWord" href="/nlab/show/Toby+Bartels">Toby Bartels</a> argues that the intuition behind accepting these justifies the (yet stronger) <a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a> (that <a class="existingWikiWord" href="/nlab/show/the+category+of+sets">the category of sets</a> has <a class="existingWikiWord" href="/nlab/show/enough+projectives">enough projectives</a>).</p> </li> <li> <p>Others add “non-classical” axioms which contradict choice or excluded middle, but which are consistent in their absence, such as “all total functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">]</mo><mo>→</mo><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">[0,1] \to \mathbb{R}</annotation></semantics></math> are continuous” (the <a class="existingWikiWord" href="/nlab/show/continuity+axiom">continuity axiom</a> of the “<a class="existingWikiWord" href="/nlab/show/intuitionism">intuitionistic</a>” school of <a class="existingWikiWord" href="/nlab/show/L.+E.+J.+Brouwer">L. E. J. Brouwer</a>) or “all partial functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi><mo>→</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N} \to \mathbb{N}</annotation></semantics></math> are computable” (the <span class="newWikiWord">computability axiom<a href="/nlab/new/computability+axiom">?</a></span> of the “<a class="existingWikiWord" href="/nlab/show/Russian+constructivism">Russian</a>” school of <a class="existingWikiWord" href="/nlab/show/Andrey+Markov+Jr">A. A. Markov</a>, which is also called “constructive recursive analysis”).</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Errett+Bishop">Errett Bishop</a> had his own branch of constructive mathematics, known as <a class="existingWikiWord" href="/nlab/show/Bishop%27s+constructive+mathematics">Bishop's constructive mathematics</a> or <a class="existingWikiWord" href="/nlab/show/BISH">BISH</a>, where <a class="existingWikiWord" href="/nlab/show/equality">equality</a> and <a class="existingWikiWord" href="/nlab/show/sets">sets</a> are defined notion rather than a primitive on <a class="existingWikiWord" href="/nlab/show/sets">sets</a>.</p> </li> <li> <p>Still others, following <a class="existingWikiWord" href="/nlab/show/Hermann+Weyl">Hermann Weyl</a>, go even further and refuse to allow “impredicative” constructions; see <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a>. Most of the work done by the schools of Brouwer, Bishop, and Markov (but not Richman) is also predicative, even though those founders were not adamant about it; as a result, predicativism often appears in the <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> of constructive mathematics (in particular, in those of <a class="existingWikiWord" href="/nlab/show/Peter+Aczel">Aczel</a> and <a class="existingWikiWord" href="/nlab/show/Per+Martin-L%C3%B6f">Martin-Löf</a>, but not those of <a class="existingWikiWord" href="/nlab/show/Harvey+Friedman">Friedman</a> or <a class="existingWikiWord" href="/nlab/show/Thierry+Coquand">Coquand</a>).</p> </li> <li> <p>An extreme form of constructive <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a> is to reject the use of <a class="existingWikiWord" href="/nlab/show/implication">implication</a> and the <a class="existingWikiWord" href="/nlab/show/universal+quantifier">universal quantifier</a> completely and work in <a class="existingWikiWord" href="/nlab/show/coherent+logic">coherent logic</a>, resulting in <a class="existingWikiWord" href="/nlab/show/coherent+mathematics">coherent mathematics</a>. Excluded middle and double negation cannot be formed, since negation can only be formed as a <a class="existingWikiWord" href="/nlab/show/sequent">sequent</a> rather than a <a class="existingWikiWord" href="/nlab/show/formula">formula</a> in the <a class="existingWikiWord" href="/nlab/show/coherent+logic">coherent logic</a>. Examples of <a class="existingWikiWord" href="/nlab/show/coherent+mathematics">coherent mathematics</a> include <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> which does not make use of <a class="existingWikiWord" href="/nlab/show/function+types">function types</a> and <a class="existingWikiWord" href="/nlab/show/dependent+function+types">dependent function types</a>, as well as mathematics done inside an <a class="existingWikiWord" href="/nlab/show/arithmetic+pretopos">arithmetic pretopos</a>.</p> </li> <li> <p>One also has <a class="existingWikiWord" href="/nlab/show/geometric+mathematics">geometric mathematics</a>, which is coherent mathematics with all <a class="existingWikiWord" href="/nlab/show/colimits">colimits</a> but no <a class="existingWikiWord" href="/nlab/show/function+sets">function sets</a>.</p> </li> <li> <p>Very extreme constructivists, like <a class="existingWikiWord" href="/nlab/show/Doron+Zeilberger">Doron Zeilberger</a>, reject the existence of infinite sets; see <a class="existingWikiWord" href="/nlab/show/finitism">finitism</a>. (Kronecker, the ‘father of constructivism’, is often considered a finitist, but as he came before the foundational crisis, it is difficult to classify him accurately.) Ironically, this means that excluded middle and choice, in their naïve forms, may become acceptable, or even true. (Even constructivists believe that they are true <a class="existingWikiWord" href="/nlab/show/internal+logic">in</a> the category <a class="existingWikiWord" href="/nlab/show/FinSet">FinSet</a> of <a class="existingWikiWord" href="/nlab/show/finite+sets">finite sets</a>.)</p> </li> <li> <p>The most extreme position of all is to deny even the existence of very large finite sets. This is called <a class="existingWikiWord" href="/nlab/show/ultrafinitism">ultrafinitism</a>. This has been studied largely by <span class="newWikiWord">Alexander Yesenin-Volpin<a href="/nlab/new/Alexander+Yesenin-Volpin">?</a></span> and (more recently) <a class="existingWikiWord" href="/nlab/show/Edward+Nelson">Edward Nelson</a>; foundational systems such as <a class="existingWikiWord" href="/nlab/show/soft+linear+logic">soft linear logic</a> can also be argued to have an ultrafinitist flavor. Zeilberger also claims sympathy with ultrafinitist philosophy, although his actual work fits well into a (merely) finitist framework.</p> </li> </ul> <p>Many constructivists (like many classical mathematicians) believe in an absolute mathematical sense of “truth,” and that in this sense choice and excluded middle are simply <em>wrong</em>. (Some constructivists, using classically false axioms, can even refute them; others merely claim that no possible correct reasoning could ever prove them. See <a href="#truevassert">Truth versus assertability</a> below.) To most mathematicians, this makes them seem quite strange. Other constructivists adopt a wait-and-see attitude, or even a relative notion of truth (which can seem strange in another way).</p> <p>The following is a partial list of schools and subtheories of constructive mathematics:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/neutral+constructive+mathematics">neutral constructive mathematics</a></p> </li> <li> <p>Brouwer’s <a class="existingWikiWord" href="/nlab/show/intuitionistic+mathematics">intuitionistic mathematics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Russian+constructivism">Russian constructivism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Bishop%27s+constructive+mathematics">Bishop's constructive mathematics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/constructive+reverse+mathematics">constructive reverse mathematics</a></p> </li> <li> <p>(at least related) <a class="existingWikiWord" href="/nlab/show/explicit+mathematics">explicit mathematics</a></p> </li> </ul> <h2 id="topos_theory">Topos theory</h2> <p>With the invention of <a class="existingWikiWord" href="/nlab/show/topos">topos theory</a> in the second half of the 20th century, a new sort of constructivism arose. It was observed (by <a class="existingWikiWord" href="/nlab/show/Bill+Lawvere">Lawvere</a> and others) that any topos with a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a> has an <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> which is powerful enough to interpret most of mathematics, but that this logic in general fails to satisfy choice and excluded middle. This meant that even for a mathematican who likes to use choice and excluded middle (and <em>a fortiori</em> for one who believes them to be “true”), there is a reason to care about what can be proven without them, because only if a proof is constructive can it be interpreted in an arbitrary topos with NNO.</p> <p>Even starting from a “completely classical” world of mathematics, many interesting toposes arise naturally (such as the category of <a class="existingWikiWord" href="/nlab/show/sheaf">sheaves</a> on any <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a>, or more generally any <a class="existingWikiWord" href="/nlab/show/site">site</a>) whose internal logic is not <a class="existingWikiWord" href="/nlab/show/classical+logic">classical logic</a>. Then by internal reasoning in such a topos (which is constructive reasoning), one can prove various useful facts, which can then be reinterpreted as external statements about the behavior of the topos itself. For example, the constructive theorem that every <a class="existingWikiWord" href="/nlab/show/one-sided+real+number">one-sided real number</a> that is both a lower real and an upper real must be located (which, classically, is an utter triviality) becomes the theorem that any <a class="existingWikiWord" href="/nlab/show/semicontinuous+function">semicontinuous function</a> (from any <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a> to the <a class="existingWikiWord" href="/nlab/show/real+line">real line</a>) that is both upper and lower semicontinuous must be <a class="existingWikiWord" href="/nlab/show/continuous+map">continuous</a> (which is at least somewhat nontrivial).</p> <p>By now it is known that many of the non-classical axioms used by the early constructivists have natural models in particular toposes. For instance, in the topos of sheaves on the real numbers <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math>, the <a class="existingWikiWord" href="/nlab/show/continuity+axiom">continuity axiom</a> that “all total functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo>→</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">R \to R</annotation></semantics></math> are continuous” holds. And in the <a class="existingWikiWord" href="/nlab/show/effective+topos">effective topos</a>, the <span class="newWikiWord">computability axiom<a href="/nlab/new/computability+axiom">?</a></span> that “all partial functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi><mo>→</mo><mi>N</mi></mrow><annotation encoding="application/x-tex">N\to N</annotation></semantics></math> are computable” holds.</p> <p>However, there are no non-classical (or classical) axioms beyond “pure constructivism” that are true in <em>all</em> toposes with NNO. In particular, there is a <a class="existingWikiWord" href="/nlab/show/free+topos">free topos</a> with NNO such that a statement is true in the free topos precisely when it is provable in pure (Richman-school) constructive mathematics. This means that for an argument to apply in all toposes, even mild assumptions such as countable or dependent choice are unacceptable (but impredicativity is fine). However, topos theory has also provided ideas that solve many of the problems with pure constructivism. For example, a well-behaved notion of “continuous function” can be recovered by using <a class="existingWikiWord" href="/nlab/show/locale">locales</a> instead of topological spaces, which was first discovered in the context of toposes and is closely related to them in any case.</p> <h2 id="some_features_of_constructive_mathematics">Some features of constructive mathematics</h2> <h3 id="rephrasing_of_classical_ideas">Rephrasing of classical ideas</h3> <p>Sometimes, all that is necessary to make a piece of mathematics constructive is careful use of language. It is common in <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a> to define things with an unnecessary amount of <a class="existingWikiWord" href="/nlab/show/negation">negation</a>. This doesn’t work so well constructively, since a statement can be not false without being true, but we can sometimes do perfectly well by just removing unnecessary <a class="existingWikiWord" href="/nlab/show/double+negations">double negations</a>.</p> <p>For example, classically one often speaks about “nonempty” sets, meaning a set which “does <em>not</em> have <em>no</em> elements.” Constructively it is much better to say that a set “<em>does</em> have at least one element”; constructivists often call such a set <em><a class="existingWikiWord" href="/nlab/show/inhabited+set">inhabited</a></em> to remind themselves that it is a “positive” notion to replace the negative one of “nonempty”. Others continue to use the word “non-empty” but understand it as a term of art that really means “inhabited”.</p> <h3 id="bifurcation_of_notions">Bifurcation of notions</h3> <p>On the other hand, differences in axiomatization or definition that make no difference classically can result in actual differences in behavior constructively. Therefore, classically equivalent notions often “bifurcate” (or “trifurcate” or worse) into multiple inequivalent constructive ones. This tends to happen whenever a concept involves <em><a class="existingWikiWord" href="/nlab/show/negation">negation</a></em> and, to a lesser degree, <em><a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a></em> and <em><a class="existingWikiWord" href="/nlab/show/existential+quantification">existential quantification</a></em>. In some cases there is a “correct” constructive version of the definition, although it may take some thought to uncover it, but in many cases more than one of the resulting concepts is important and useful. For example:</p> <ul> <li> <p>There are multiple inequivalent notions of a <a class="existingWikiWord" href="/nlab/show/set">set</a>, because <a class="existingWikiWord" href="/nlab/show/denial+inequality">denial inequality</a> does not have the same properties in constructive mathematics that it does in <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a>. These include objects such as sets with <a class="existingWikiWord" href="/nlab/show/stable+equality">stable equality</a>, sets with <a class="existingWikiWord" href="/nlab/show/decidable+equality">decidable equality</a>, sets with <a class="existingWikiWord" href="/nlab/show/tight+apartness+relations">tight apartness relations</a>, and finally <a class="existingWikiWord" href="/nlab/show/classical+sets">classical sets</a>, the last of which are precisely the sets in constructive mathematics whose denial inequality has all the same properties as it does in classical mathematics.</p> </li> <li> <p>There are multiple inequivalent constructive definitions of a <a class="existingWikiWord" href="/nlab/show/field">field</a>, because of the axioms “every <em>nonzero</em> element has an inverse” and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn><mo>≠</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">0 \neq 1</annotation></semantics></math>.</p> </li> <li> <p>More generally, the <a class="existingWikiWord" href="/nlab/show/antithesis+interpretation">antithesis interpretation</a> of constructive mathematics leads to a generalised notion of <a class="existingWikiWord" href="/nlab/show/negation">negation</a> as two <a class="existingWikiWord" href="/nlab/show/mutually+exclusive+propositions">mutually exclusive propositions</a>. This results in the bifurcation of basic mathematical objects, such as <a class="existingWikiWord" href="/nlab/show/set">set</a> (<a class="existingWikiWord" href="/nlab/show/A-set"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"> <semantics> <mrow> <mi>𝒜</mi> </mrow> <annotation encoding="application/x-tex">\mathcal{A}</annotation> </semantics> </math>-set</a>), <a class="existingWikiWord" href="/nlab/show/monoid">monoid</a> (<a class="existingWikiWord" href="/nlab/show/A-monoid"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"> <semantics> <mrow> <mi>𝒜</mi> </mrow> <annotation encoding="application/x-tex">\mathcal{A}</annotation> </semantics> </math>-monoid</a>), <a class="existingWikiWord" href="/nlab/show/group">group</a> (<a class="existingWikiWord" href="/nlab/show/A-group"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"> <semantics> <mrow> <mi>𝒜</mi> </mrow> <annotation encoding="application/x-tex">\mathcal{A}</annotation> </semantics> </math>-group</a>), <a class="existingWikiWord" href="/nlab/show/ring">ring</a> (<a class="existingWikiWord" href="/nlab/show/A-ring"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"> <semantics> <mrow> <mi>𝒜</mi> </mrow> <annotation encoding="application/x-tex">\mathcal{A}</annotation> </semantics> </math>-ring</a>), and <a class="existingWikiWord" href="/nlab/show/partial+order">partial order</a> (<a class="existingWikiWord" href="/nlab/show/antithesis+partial+order"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"> <semantics> <mrow> <mi>𝒜</mi> </mrow> <annotation encoding="application/x-tex">\mathcal{A}</annotation> </semantics> </math>-partial order</a>) into at least five concepts each, depending on the relation between the pointwise mutually exclusive relations and their intuitionistic <a class="existingWikiWord" href="/nlab/show/denial+negation">denial negation</a>.</p> </li> <li> <p>There are multiple inequivalent definitions of <a class="existingWikiWord" href="/nlab/show/real+numbers">real numbers</a>.</p> <ul> <li>the <a class="existingWikiWord" href="/nlab/show/Dedekind+real+numbers">Dedekind real numbers</a> and the <a class="existingWikiWord" href="/nlab/show/Cauchy+real+numbers">Cauchy real numbers</a> need no longer coincide. The Cauchy reals sit inside the Dedekind reals, but in general not every Dedekind real need be approximable by a <em><a class="existingWikiWord" href="/nlab/show/sequence">sequence</a></em> of rationals. From a topos-theoretic viewpoint, the Dedekind reals are usually the “correct” notion to study (if not the <a class="existingWikiWord" href="/nlab/show/locale+of+real+numbers">locale of real numbers</a> as a whole). However, the weak <a class="existingWikiWord" href="/nlab/show/limited+principle+of+omniscience">limited principle of omniscience</a> suffices to ensure that every Dedekind real is a Cauchy real, and hence that the two notions coincide; see (<a class="existingWikiWord" href="/nlab/show/Univalent+Foundations+Project">Univalent Foundations Project</a> 2013) and (Booij 2020). Weak countable choice implies the weak limited principle of omniscience, which in turn is implied by excluded middle and the axiom of choice; see (Bridges et al. 1993).</li> <li>Similarly, the <a class="existingWikiWord" href="/nlab/show/Cauchy+real+numbers">Cauchy real numbers</a> are not sequentially <a class="existingWikiWord" href="/nlab/show/Cauchy+complete">Cauchy complete</a>. There is an intermediate set of <a class="existingWikiWord" href="/nlab/show/real+numbers">real numbers</a> between the Cauchy reals and the Dedekind reals that are sequentially Cauchy complete called the <a class="existingWikiWord" href="/nlab/show/HoTT+book+real+numbers">HoTT book real numbers</a>, such that there are embeddings from the Cauchy reals to the HoTT reals, and from the HoTT reals to the Dedekind reals, but there are no embeddings in the reverse direction.</li> <li>The lower, upper, and two-sided <a class="existingWikiWord" href="/nlab/show/Dedekind+real+numbers">Dedekind real numbers</a> do not coincide with each other. That they do coincide is equivalent to <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>, as shown <a href="https://categorytheory.zulipchat.com/#narrow/stream/229136-theory.3A-category-theory/topic/One.20universe.20as.20a.20foundation.20.26.20friends/near/465219817">here</a> by <a class="existingWikiWord" href="/nlab/show/James+Hanson">James Hanson</a>.</li> <li>A real number with a <a class="existingWikiWord" href="/nlab/show/locator">locator</a> is equivalent to a real number represented by a <a class="existingWikiWord" href="/nlab/show/Cauchy+sequence">Cauchy sequence</a> with <a class="existingWikiWord" href="/nlab/show/modulus+of+convergence">modulus of convergence</a>, which implies that it is <a class="existingWikiWord" href="/nlab/show/sequentially+complete">sequentially complete</a>. That every <a class="existingWikiWord" href="/nlab/show/modulated+Cauchy+real+number">modulated Cauchy real number</a> has a <a class="existingWikiWord" href="/nlab/show/locator">locator</a> or is a <a class="existingWikiWord" href="/nlab/show/Cauchy+sequence">Cauchy sequence</a> with <a class="existingWikiWord" href="/nlab/show/modulus+of+convergence">modulus of convergence</a> implies that the Cauchy real numbers coincide with the HoTT real numbers.</li> <li>That every real number with a locator in the <a class="existingWikiWord" href="/nlab/show/unit+interval">unit interval</a> can be represented by a <a class="existingWikiWord" href="/nlab/show/sequence">sequence</a> of (positive) digits is equivalent to the lesser <a class="existingWikiWord" href="/nlab/show/limited+principle+of+omniscience">limited principle of omniscience</a>, so it is no longer true that every such real number has an infinite decimal representation. The set of all real numbers with infinite decimal representations are called <a class="existingWikiWord" href="/nlab/show/prealgebra+real+numbers">prealgebra real numbers</a>.</li> </ul> </li> <li> <p>There are at least three different constructive notions of <a class="existingWikiWord" href="/nlab/show/ordinal+number">ordinal number</a>; see (Taylor 1996) and (Joyal–Moerdijk 1995).</p> </li> <li> <p>Without the axiom of choice, <a class="existingWikiWord" href="/nlab/show/functor">functors</a> and <a class="existingWikiWord" href="/nlab/show/anafunctor">anafunctors</a> become distinct, and often the latter is more appropriate; see (Makkai, 1996).</p> </li> <li> <p>Perhaps most disturbingly of all to the classical mathematician, one must distinguish between <em>finite sets</em>, <em>subfinite sets</em>, <em>finitely-indexed sets</em>, and even <em>subfinitely indexed sets</em>; see <a class="existingWikiWord" href="/nlab/show/finite+set">finite set</a> for definitions. However, in practice it is usually either finite or finitely-indexed sets that are important, and with practice a little bit of thought suffices to show which is the relevant concept.</p> </li> </ul> <h3 id="negative_translation">Negative translation</h3> <p>This allows one to translate classically valid theorems into intuitionistically valid theorems. See <a class="existingWikiWord" href="/nlab/show/double+negation+translation">double negation translation</a>.</p> <h3 id="truevassert">Truth versus assertability</h3> <p>Already in <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a>, there is a difference between saying that something is true and saying that something is <a class="existingWikiWord" href="/nlab/show/proof">provable</a>. If you adopt <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> because you believe it correct, then presumably you believe that ZFC is consistent even though (assuming that you're aware of certain theorems) you also know that you cannot prove it so. In that case, you also believe that the <a class="existingWikiWord" href="/nlab/show/continuum+hypothesis">continuum hypothesis</a> (for example) is either true or false; you may or may not have an opinion on which it is, but in any case again you know that you cannot prove it either way.</p> <p>A constructive mathematician can be even subtler. If you belong to the Bishop school, then you accept no classically false axioms, and anything that you can prove is valid also in classical mathematics. Even so, you can believe that the principle of excluded middle is false (even though, of course, you know that you cannot prove it false). So you can really confuse the classical mathematicians by saying, on the one hand, that they can safely accept all of your theorems as valid, and then saying, on the other hand, that you know excluded middle to be false. The resolution, of course, is that you never claimed that this was a <em>theorem</em>.</p> <p>This way of talking has even been formalised in (Bishop, 1967) with a convention adopted by many (but not all) of his followers. In this convention, the word ‘not’, used normally in a vernacular sentence whose mathematical content would otherwise be the proposition <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math>, changes to the content to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mi>p</mi></mrow><annotation encoding="application/x-tex">\neg p</annotation></semantics></math>, or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>→</mo><mo>⊥</mo></mrow><annotation encoding="application/x-tex">p \to \bot</annotation></semantics></math>, as usual. (This follows all of the rules of <a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic logic</a>; in particular, any statement that is ‘not’ true is false (just as in <a class="existingWikiWord" href="/nlab/show/classical+logic">classical logic</a>).) However, the word ‘<i>not</i>’, in italics as shown here, changes the content to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>→</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">p \to x</annotation></semantics></math>, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> is some statement that is known (although not proved!), according to Bishop, to be false. Now a statement that is ‘<i>not</i>’ true may be false, but this may be unknown, and it is even possible that it is also ‘<i>not</i>’ false (so <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mi>p</mi><mo>→</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">\neg p \to x</annotation></semantics></math>, possibly for a different <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>).</p> <p>Bishop gives in his introduction several statements, suitable for use as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> above, including:</p> <ul> <li>excluded middle itself, which Bishop call the ‘principle of omniscience’;</li> <li>the ‘<a class="existingWikiWord" href="/nlab/show/limited+principle+of+omniscience">limited principle of omniscience</a>’: any infinite sequence in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mn>0</mn><mo>,</mo><mn>1</mn><msup><mo stretchy="false">}</mo> <mi>N</mi></msup></mrow><annotation encoding="application/x-tex">\{0,1\}^N</annotation></semantics></math> is either all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math> or has at least one <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math>;</li> <li>the ‘<a class="existingWikiWord" href="/nlab/show/lesser+limited+principle+of+omniscience">lesser limited principle of omniscience</a>’: for any two infinite sequence in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mn>0</mn><mo>,</mo><mn>1</mn><msup><mo stretchy="false">}</mo> <mi>N</mi></msup></mrow><annotation encoding="application/x-tex">\{0,1\}^N</annotation></semantics></math> that do not both have at least one <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math>, at least one of these sequences does not have at least one <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math>;</li> <li>others.</li> </ul> <p>At one point in his book, while discussing the possibility of a pointwise-continuous function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">]</mo><mo>→</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">[0,1] \to R</annotation></semantics></math> that is not uniformly continuous (a <span class="newWikiWord">Specker function<a href="/nlab/new/Specker+function">?</a></span>, whose existence Markov's school claims as a theorem), Bishop seems to assert that this theorem is both <i>not</i> true and <i>not</i> false; he does not put it this way, so this may not be exactly what he meant, but there is no contradiction if it is. (But it <em>is</em> a contradiction, even in intuitionistic logic, if a statment is both not true and not false; indeed, a definition of ‘false’ may be taken to be ‘not true’.)</p> <p>This practice can be understood through a careful distinction between <a class="existingWikiWord" href="/nlab/show/object+language">object language</a> and <a class="existingWikiWord" href="/nlab/show/metalanguage">metalanguage</a>. A mathematical statement <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math> (such as the continuum hypothesis, or that a Specker function exists) belongs to the object language, as does <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mi>p</mi></mrow><annotation encoding="application/x-tex">\neg p</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>→</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">p \to x</annotation></semantics></math> for any specific mathematical statement <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>. But the statement that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math> is provable in some formal system belongs to the metalanguage (although it can also phrased internal to any object language suitable for mathematics), and as such may be written <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mi>p</mi></mrow><annotation encoding="application/x-tex">\vdash p</annotation></semantics></math>. The metalanguage has its own logic (the metalogic, which for the sake of argument we may even assume to be classical), but notice that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mo>⊢</mo><mi>p</mi></mrow><annotation encoding="application/x-tex">\neg \vdash p</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mo>¬</mo><mi>p</mi></mrow><annotation encoding="application/x-tex">\vdash \neg p</annotation></semantics></math> are different; the first claims that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math> cannot be proved, while the second claims that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math> can be refuted, which (in any <span class="newWikiWord">consistent<a href="/nlab/new/consistent+logic">?</a></span> formal system, even a classical one) is strictly stronger. Although Bishop did not commit to any formal system, if we assume for the sake of argument that he settled on one, then we may write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mo>¬</mo><mi>p</mi></mrow><annotation encoding="application/x-tex">\vdash \neg p</annotation></semantics></math> as our interpretation of his meaning when he asserts ‘not <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math>’ but <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mo>⊢</mo><mi>p</mi></mrow><annotation encoding="application/x-tex">\neg \vdash p</annotation></semantics></math> as his meaning when he asserts ‘<i>not</i> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math>’.</p> <p>Even without the notational convention of the Bishop school, it is important when reading constructive mathematics to remember the difference between what can be refuted (proved false) and what merely cannot be proved true. Although Brouwer's and Markov's schools will sometimes claim to prove statements that are (classically) outright false (such as that every function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">]</mo><mo>→</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">[0,1] \to R</annotation></semantics></math> is pointwise-continuous), it is more common (and can happen in any school) that a constructive mathematician makes a claim that merely <em>sounds</em> false, when what they really mean is only that they don't accept what you say as true. Often modal phrases like ‘not necessarily’ will be used where Bishop would use ‘<i>not</i>’, as a clue that we're shifting to a metalanguage, or at least merely remaining agnostic rather than outright disagreeing.</p> <p>The distinction between object language and metalanguage exists even in <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a>, but it seems that most classical mathematicians are not used to remembering it, although it is not entirely clear why this should be so. One possibly relevant observation is that even if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> is a statement which is neither provable nor disprovable (like the continuum hypothesis), in classical mathematics it is still provable that “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> is either true or false.” Moreover, classical <a class="existingWikiWord" href="/nlab/show/model+theory">model theory</a> often restricts itself to <span class="newWikiWord">two-valued models<a href="/nlab/new/two-valued+model">?</a></span> in which the only truth values are “true” and “false,” although classical logic still holds in <a class="existingWikiWord" href="/nlab/show/Boolean+algebra">Boolean-valued</a> models, and in such a case the truth value of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> may be neither “true” nor “false,” although the truth value of “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> or not <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>” is still “true.” Certainly when talking about classical truths which fail constructively, such as excluded middle, it is important to remember that “fails to be provable” is different from “is provably false.”</p> <h2 id="prehistory">Prehistory</h2> <p>In</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Georg+Hegel">Georg Hegel</a>, <em><a class="existingWikiWord" href="/nlab/show/Phenomenology+of+Spirit">Phenomenology of Spirit</a></em> (1807)</li> </ul> <p>the following comment about mathematical proof (in section <em><a href="https://www.marxists.org/reference/archive/hegel/works/ph/phprefac.htm#12">12 Historical and mathematical proof</a></em> of the Preface) might be read as being a complaint about the traditional non-constructive concept of proof and about the traditional lack of <a class="existingWikiWord" href="/nlab/show/proof+relevance">proof relevance</a>:</p> <blockquote> <p id="PoSOnProofRelevance"> All the same, while proof is essential in the case of mathematical knowledge, it still does not have the significance and nature of being a moment in the result itself; the proof is over when we get the result, and has disappeared. The process of mathematical proof does not belong to the object; it is a function that takes place outside the matter in hand.</p> <p><a href="https://www.marxists.org/reference/archive/hegel/help/finpref.htm#m042">footnote 42</a>: Mathematical truths are not thought to be known unless proved true. Their demonstrations are not, however, kept as parts of what they prove, but are only our subjective means towards knowing the latter. In philosophy, however, consequences always form part of the essence made manifest in them, which returns to itself in such expressions.</p> </blockquote> <p>See also earlier conceptions of proofs expressing the ‘cause’ of a theorem, where <em>reductio</em> proofs in particular were taken generally to fail. Such an idea goes back to Aristotle for whom a proper answer to the question “Why is the angle in a semicircle a right-angle?” gives its cause.</p> <ul> <li>Paolo Mancosu, <em>Philosophy of Mathematics and Mathematical Practice in the Seventeenth Century</em>, OUP, 1996.</li> </ul> <h2 id="related_entries">Related entries</h2> <p>See also</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/intuitionistic+mathematics">intuitionistic mathematics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability">realizability</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computability">computability</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/constructive+set+theory">constructive set theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/constructive+analysis">constructive analysis</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/constructive+algebraic+topology">constructive algebraic topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/taboo">taboo</a></p> </li> </ul> <p>Concepts that usually arise in constructive mathematics, often because they are classically trivial:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/proof+relevance">proof relevance</a></li> <li><a class="existingWikiWord" href="/nlab/show/anafunctor">anafunctor</a> (classically equivalent to a <a class="existingWikiWord" href="/nlab/show/functor">functor</a>)</li> <li><a class="existingWikiWord" href="/nlab/show/apartness+relation">apartness relation</a> (classically complementary to an <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a>)</li> <li><a class="existingWikiWord" href="/nlab/show/comparison">comparison</a> (classically complementary to a <a class="existingWikiWord" href="/nlab/show/transitive+relation">transitive relation</a>)</li> <li><a class="existingWikiWord" href="/nlab/show/decidable+equality">decidable equality</a> (classically trivial)</li> <li><a class="existingWikiWord" href="/nlab/show/decidable+subset">decidable subset</a> (classically trivial)</li> <li><a class="existingWikiWord" href="/nlab/show/inhabited+set">inhabited set</a> (classically equivalent to a non-<a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a>)</li> <li><a class="existingWikiWord" href="/nlab/show/pseudo-order">pseudo-order</a> (classically complementary to a <a class="existingWikiWord" href="/nlab/show/total+order">total order</a>)</li> <li><a class="existingWikiWord" href="/nlab/show/locale">locale</a> (classically similar to but not equivalent to a <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a>)</li> <li><a class="existingWikiWord" href="/nlab/show/connected+irreflexive+comparison">connected irreflexive comparison</a> (classically complementary to a <a class="existingWikiWord" href="/nlab/show/partial+order">partial order</a>)</li> <li><a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a> (classically equivalent to the empty set or a <a class="existingWikiWord" href="/nlab/show/singleton">singleton</a>)</li> <li><a class="existingWikiWord" href="/nlab/show/Heyting+field">Heyting field</a>, <a class="existingWikiWord" href="/nlab/show/weak+Heyting+field">weak Heyting field</a>, <a class="existingWikiWord" href="/nlab/show/discrete+field">discrete field</a> (classically all equivalent to a <a class="existingWikiWord" href="/nlab/show/field">field</a>)</li> <li><a class="existingWikiWord" href="/nlab/show/weak+local+ring">weak local ring</a>, <a class="existingWikiWord" href="/nlab/show/local+ring">local ring</a>, <a class="existingWikiWord" href="/nlab/show/residually+discrete+local+ring">residually discrete local ring</a> (classically equivalent to a <a class="existingWikiWord" href="/nlab/show/local+ring">local ring</a>)</li> <li><a class="existingWikiWord" href="/nlab/show/Cantor+real+numbers">Cantor real numbers</a>, <a class="existingWikiWord" href="/nlab/show/HoTT+book+real+numbers">HoTT book real numbers</a>, <a class="existingWikiWord" href="/nlab/show/Dedekind+real+numbers">Dedekind real numbers</a> (classically all equivalent as the <a class="existingWikiWord" href="/nlab/show/real+numbers">real numbers</a>)</li> </ul> <p>Some of these are also useful internally or even classically.</p> <p>Topics relevant to the foundations of constructive mathematics:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a></li> <li><a class="existingWikiWord" href="/nlab/show/centipede+mathematics">centipede mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/choice+object">choice object</a></li> <li><a class="existingWikiWord" href="/nlab/show/COSHEP">COSHEP</a></li> <li><a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a></li> <li><a class="existingWikiWord" href="/nlab/show/finite+mathematics">finite mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/internalization">internalization</a></li> <li><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/Markov%27s+principle">Markov's principle</a></li> <li><a class="existingWikiWord" href="/nlab/show/power+set">power set</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/pretopos">pretopos</a></li> <li><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/topos">topos</a></li> <li><a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a></li> <li><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/intuitionistic+type+theory">intuitionistic type theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a></li> </ul> </li> </ul> <p>Other articles with content relating to constructive mathematics (rather incomplete):</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/biproduct">biproduct</a></li> <li><a class="existingWikiWord" href="/nlab/show/Cantor%27s+theorem">Cantor's theorem</a></li> <li><a class="existingWikiWord" href="/nlab/show/cardinal+number">cardinal number</a></li> <li><a class="existingWikiWord" href="/nlab/show/complement">complement</a></li> <li><a class="existingWikiWord" href="/nlab/show/complete+lattice">complete lattice</a></li> <li><a class="existingWikiWord" href="/nlab/show/countable+set">countable set</a></li> <li><a class="existingWikiWord" href="/nlab/show/cyclic+order">cyclic order</a></li> <li><a class="existingWikiWord" href="/nlab/show/direct+sum">direct sum</a></li> <li><a class="existingWikiWord" href="/nlab/show/extended+natural+number+system">extended natural number system</a></li> <li><a class="existingWikiWord" href="/nlab/show/field">field</a></li> <li><a class="existingWikiWord" href="/nlab/show/filter">filter</a></li> <li><a class="existingWikiWord" href="/nlab/show/finite+set">finite set</a></li> <li><a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a></li> <li><a class="existingWikiWord" href="/nlab/show/Hausdorff+space">Hausdorff space</a></li> <li><a class="existingWikiWord" href="/nlab/show/hereditarily+finite+set">hereditarily finite set</a></li> <li><a class="existingWikiWord" href="/nlab/show/infinite+set">infinite set</a></li> <li><a class="existingWikiWord" href="/nlab/show/injection">injection</a></li> <li><a class="existingWikiWord" href="/nlab/show/local+ring">local ring</a></li> <li><a class="existingWikiWord" href="/nlab/show/metric+space">metric space</a></li> <li><a class="existingWikiWord" href="/nlab/show/partial+function">partial function</a></li> <li><a class="existingWikiWord" href="/nlab/show/pure+set">pure set</a></li> <li><a class="existingWikiWord" href="/nlab/show/real+number">real number</a></li> <li><a class="existingWikiWord" href="/nlab/show/sequence">sequence</a></li> <li><a class="existingWikiWord" href="/nlab/show/Set">Set</a></li> <li><a class="existingWikiWord" href="/nlab/show/Sierpinski+space">Sierpinski space</a></li> <li><a class="existingWikiWord" href="/nlab/show/simple+object">simple object</a></li> <li><a class="existingWikiWord" href="/nlab/show/sober+space">sober space</a></li> <li><a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a></li> <li><a class="existingWikiWord" href="/nlab/show/Tychonoff+theorem">Tychonoff theorem</a></li> <li><a class="existingWikiWord" href="/nlab/show/uniform+space">uniform space</a></li> <li><a class="existingWikiWord" href="/nlab/show/well-founded+relation">well-founded relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/well-order">well-order</a></li> <li><a class="existingWikiWord" href="/nlab/show/well-ordering+theorem">well-ordering theorem</a></li> <li><a class="existingWikiWord" href="/nlab/show/well-pointed+topos">well-pointed topos</a></li> <li><a class="existingWikiWord" href="/nlab/show/Zorn%27s+lemma">Zorn's lemma</a></li> </ul> <p>In principle, every article could explain how it applies to constructive mathematics, but that will probably never happen.</p> <p>There is also</p> <ul> <li><span class="newWikiWord">constructivism and idealism<a href="/nlab/new/constructivism+and+idealism">?</a></span></li> </ul> <h2 id="References">References</h2> <p>See also the references at <em><a class="existingWikiWord" href="/nlab/show/intuitionistic+mathematics">intuitionistic mathematics</a></em> for more.</p> <p>Original texts:</p> <ul> <li id="Bishop"><a class="existingWikiWord" href="/nlab/show/Errett+Bishop">Errett Bishop</a>, <em><a class="existingWikiWord" href="/nlab/show/Foundations+of+Constructive+Analysis">Foundations of Constructive Analysis</a></em>, McGraw-Hill (1967)</li> </ul> <p>rewritten as:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Errett+Bishop">Errett Bishop</a>, <a class="existingWikiWord" href="/nlab/show/Douglas+Bridges">Douglas Bridges</a> <em><a class="existingWikiWord" href="/nlab/show/Constructive+Analysis">Constructive Analysis</a></em>, Grundlehren der mathematischen Wissenschaften <strong>279</strong>, Springer (1985) [<a href="https://doi.org/10.1007/978-3-642-61667-9">doi:10.1007/978-3-642-61667-9</a>]</li> </ul> <p>Early monographs:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Anne+Sjerp+Troelstra">Anne Sjerp Troelstra</a>, <a class="existingWikiWord" href="/nlab/show/Dirk+van+Dalen">Dirk van Dalen</a>: <em>Constructivism in Mathematics – An introduction</em>, Volume I, Studies in Logic and the Foundations of Mathematics <strong>121</strong>, North Holland (1988) [<a href="https://www.elsevier.com/books/constructivism-in-mathematics-vol-1/troelstra/978-0-444-70266-1">ISBN:9780444702661</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Anne+Sjerp+Troelstra">Anne Sjerp Troelstra</a>, <a class="existingWikiWord" href="/nlab/show/Dirk+van+Dalen">Dirk van Dalen</a>, <em>Constructivism in Mathematics – An introduction</em>, Volume II, Studies in Logic and the Foundations of Mathematics <strong>123</strong>: North Holland (1988) [<a href="https://shop.elsevier.com/books/constructivism-in-mathematics-vol-2/troelstra/978-0-444-70358-3">ISBN:9780444703583</a>]</p> </li> </ul> <p>Gentle introductions:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Douglas+Bridges">Douglas Bridges</a>: <em>Introducing constructive mathematics</em>, talk notes (~2015) [<a class="existingWikiWord" href="/nlab/files/Bridges-IntroducingConstructiveMath.pdf" title="pdf">pdf</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Andrej+Bauer">Andrej Bauer</a>: <em>Five Stages of Accepting Constructive Mathematics</em>, Bull. Amer. Math. Soc. <strong>54</strong> (2017) 481-498 [<a href="http://dx.doi.org/10.1090/bull/1556">doi:10.1090/bull/1556</a>, <a href="https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf">pdf</a>]</p> <p>based on a talk at IAS (March 18, 2013) [<a href="http://video.ias.edu/members/1213/0318-AndrejBauer">video</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Fred+Richman">Fred Richman</a>, <em><a href="https://projecteuclid.org/journals/modern-logic/volume-6/issue-3/Interview-with-a-constructive-mathematician/rml/1204835729.full">Interview with a constructive mathematician</a></em>, Modern Logic <strong>6</strong> 3 (1996) 247-271 [<a href="http://www.ams.org/mathscinet-getitem?mr=1400617">MathSciNet</a>]</p> </li> <li id="Blechschmidt15"> <p><a class="existingWikiWord" href="/nlab/show/Ingo+Blechschmidt">Ingo Blechschmidt</a>, <em>Double-negation translation and CPS transforms</em>, 2015 (<a href="http://rawgit.com/iblech/talk-constructive-mathematics/master/negneg-translation-notes.pdf">pdf</a>)</p> </li> <li> <p>Stanford Encyclopedia of Philosophy, <em><a href="http://plato.stanford.edu/entries/mathematics-constructive/">Constructive mathematics</a></em></p> </li> </ul> <p>An more technical introduction to constructive reasoning in mathematics is (with an eye towards <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>) in the introduction of:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Univalent+Foundations+Project">Univalent Foundations Project</a>, <em><a class="existingWikiWord" href="/nlab/show/Homotopy+Type+Theory+--+Univalent+Foundations+of+Mathematics">Homotopy Type Theory – Univalent Foundations of Mathematics</a></em></li> </ul> <p>Other accounts:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Michael+J.+Beeson">Michael J. Beeson</a>, <em>Foundations of Constructive Mathematics</em>, Ergebnisse der Mathematik und ihrer Grenzgebiete <strong>3</strong> 6, Springer 1985 (<a href="https://link.springer.com/book/10.1007/978-3-642-68952-9">doi:10.1007/978-3-642-68952-9</a>, <a href="https://link.springer.com/content/pdf/10.1007%2F978-3-642-68952-9.pdf">pdf</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Douglas+Bridges">Douglas Bridges</a> and <a class="existingWikiWord" href="/nlab/show/Fred+Richman">Fred Richman</a>, <em>Varieties of constructive mathematics</em> (1987)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Fred+Richman">Fred Richman</a>, <a class="existingWikiWord" href="/nlab/show/Douglas+Bridges">Douglas Bridges</a>, Peter Schuster, <em>A weak countable choice principle</em>. Proceedings of the American Mathematical Society 128(9):2749-2752, March 2000. [<a href="http://dx.doi.org/10.1090/S0002-9939-00-05327-2">doi:10.1090/S0002-9939-00-05327-2</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Michael+Makkai">Michael Makkai</a> (1996). <a href="http://www.math.mcgill.ca/makkai/anafun/">Avoiding the axiom of choice in general category theory</a>.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Fred+Richman">Fred Richman</a>, <em>Constructive Mathematics without Choice</em>,</p> <p>in: <em>Reuniting the Antipodes – Constructive and Nonstandard Views of the Continuum</em>, Synthese Library <strong>306</strong>, Springer (2001) 199-206 [<a href="https://doi.org/10.1007/978-94-015-9757-9_17">doi:10.1007/978-94-015-9757-9_17</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Paul+Taylor">Paul Taylor</a> (1996). Intuitionistic Sets and Ordinals. Available (with several other references) at <a href="http://www.PaulTaylor.EU/ordinals/index.php">Induction, recursion, replacement and the ordinals</a>.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Andr%C3%A9+Joyal">André Joyal</a> and <a class="existingWikiWord" href="/nlab/show/Ieke+Moerdijk">Ieke Moerdijk</a> (1995). <em>Algebraic set theory</em>.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Frank+Waaldijk">Frank Waaldijk</a> (2003). <a href="http://www.fwaaldijk.nl/foundations%20of%20constructive%20mathematics.pdf">On the foundations of constructive mathematics - especially in relation to the theory of continuous functions</a> (PDF).</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Auke+B.+Booij">Auke B. Booij</a>, Analysis in univalent type theory (<a href="https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf">pdf</a>)</p> </li> </ul> <p>On constructive mathematics applied to <a class="existingWikiWord" href="/nlab/show/physics">physics</a> (cf. <em><a class="existingWikiWord" href="/nlab/show/computable+physics">computable physics</a></em>):</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Douglas+S.+Bridges">Douglas S. Bridges</a>: <em>Can Constructive Mathematics Be Applied in Physics?</em>, Journal of Philosophical Logic <strong>28</strong> 5 (1999) 439-453 [<a href="https://www.jstor.org/stable/30226680">jstor:30226680</a>, <a href="https://doi.org/10.1023/A:1004420413391">doi:10.1023/A:1004420413391</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Andrej+Bauer">Andrej Bauer</a>: <em>Intuitionistic Mathematics and Realizability in the Physical World</em>, in <em>A Computable Universe</em> (2012) 143-157 [<a href="https://doi.org/10.1142/9789814374309_0008">doi:10.1142/9789814374309_0008</a>, <a href="https://math.andrej.com/wp-content/uploads/2014/03/real-world-realizability.pdf">pdf</a>, <a href="https://math.andrej.com/2014/03/04/intuitionistic-mathematics-and-realizability-in-the-physical-world/">webpage</a>]</p> </li> </ul> <p>In view of <a class="existingWikiWord" href="/nlab/show/reverse+mathematics">reverse mathematics</a>:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Hajime+Ishihara">Hajime Ishihara</a>, <em>Reverse Mathematics in Bishop’s Constructive Mathematics</em>, Philosophia Scientiæ, CS 6 (2006) (<a href="https://doi.org/10.4000/philosophiascientiae.406">doi:10.4000/philosophiascientiae.406</a>, <a href="https://philosophiascientiae.revues.org/pdf/406">pdf</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Hannes+Diener">Hannes Diener</a>, <em>Constructive Reverse Mathematics</em>, 2018 (<a href="https://arxiv.org/abs/1804.05495">arXiv:1804.05495</a>, <a href="https://dspace.ub.uni-siegen.de/handle/ubsi/1306">dspace:ubsi/1306</a>)</p> </li> </ul> <p>General comments on intuitionistic mathematics/logic as the natural language for <a class="existingWikiWord" href="/nlab/show/physics">physics</a> are in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Andrej+Bauer">Andrej Bauer</a>, <em><a href="http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/">Intuitionistic mathematics for physics</a></em>, August 2008</li> </ul> <p>For more on <a class="existingWikiWord" href="/nlab/show/physics">physics</a> formalized in intuitionistic mathematics (notably in <a class="existingWikiWord" href="/nlab/show/topos+theory">topos theory</a>) see at <em><a class="existingWikiWord" href="/nlab/show/geometry+of+physics">geometry of physics</a></em>.</p> <p>For an emphasis on <a class="existingWikiWord" href="/nlab/show/proof+relevance">proof relevance</a>, see:</p> <ul> <li id="Harper13"><a class="existingWikiWord" href="/nlab/show/Robert+Harper">Robert Harper</a>, <em><a href="https://existentialtype.wordpress.com/2013/07/10/constructive-mathematics-is-not-meta-mathematics/">Constructive Mathematics is not Metamathematics</a></em> (2013)</li> </ul> <p>Most books on <a class="existingWikiWord" href="/nlab/show/topos+theory">topos theory</a> include some discussion of toposes' <a class="existingWikiWord" href="/nlab/show/internal+logic">internal</a> constructive logic. One good reference is:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Peter+Johnstone">Peter Johnstone</a> (2003). <em><a class="existingWikiWord" href="/nlab/show/Elephant">Sketches of an elephant</a></em>. Part D (in volume 2).</li> </ul> <p>A historical account is in</p> <ul> <li id="Troelstra91"><a class="existingWikiWord" href="/nlab/show/Anne+Sjerp+Troelstra">Anne Sjerp Troelstra</a>, <em>History of Constructivism in the Twentieth Century</em> (1991) [<a href="https://www.illc.uva.nl/Research/Publications/Reports/ML-1991-05.text.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Troelstra-HistoryOfConstructivism.pdf" title="pdf">pdf</a>]</li> </ul> <p>The relation to <a class="existingWikiWord" href="/nlab/show/realizability">realizability</a> and <a class="existingWikiWord" href="/nlab/show/computability">computability</a> is discussed in</p> <ul> <li id="Bauer05"><a class="existingWikiWord" href="/nlab/show/Andrej+Bauer">Andrej Bauer</a>, <em>Realizability as connection between constructive and computable mathematics</em>, in T. Grubba, P. Hertling, H. Tsuiki, and <a class="existingWikiWord" href="/nlab/show/Klaus+Weihrauch">Klaus Weihrauch</a>, (eds.) <em>CCA 2005 - Second International Conference on Computability and Complexity in Analysis</em>, August 25-29,2005, Kyoto, Japan, ser. Informatik Berichte, vol. 326-7/2005. FernUniversität Hagen, Germany, 2005, pp. 378–379. (<a href="http://math.andrej.com/data/c2c.pdf">pdf</a>)</li> </ul> <p>On <a class="existingWikiWord" href="/nlab/show/commutative+algebra">commutative algebra</a> with constructive methods:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Henri+Lombardi">Henri Lombardi</a>, <a class="existingWikiWord" href="/nlab/show/Claude+Quitt%C3%A9">Claude Quitté</a> (2010): <em>Commutative algebra: Constructive methods (Finite projective modules)</em> Translated by Tania K. Roblo, Springer (2015) (<a href="https://link.springer.com/book/10.1007/978-94-017-9944-7">doi:10.1007/978-94-017-9944-7</a>, <a href="http://hlombardi.free.fr/CACM.pdf">pdf</a>)</li> </ul> <p>On the <a class="existingWikiWord" href="/nlab/show/antithesis+interpretation">antithesis interpretation</a> of <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a>:</p> <ul> <li id="Shulman2022"><a class="existingWikiWord" href="/nlab/show/Michael+Shulman">Michael Shulman</a>, <em>Affine logic for constructive mathematics</em>. Bulletin of Symbolic Logic, Volume 28, Issue 3, September 2022. pp. 327 - 386 (<a href="https://doi.org/10.1017/bsl.2022.28">doi:10.1017/bsl.2022.28</a>, <a href="https://arxiv.org/abs/1805.07518">arXiv:1805.07518</a>)</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on January 21, 2025 at 16:58:42. See the <a href="/nlab/history/constructive+mathematics" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/constructive+mathematics" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/13375/#Item_13">Discuss</a><span class="backintime"><a href="/nlab/revision/constructive+mathematics/96" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/constructive+mathematics" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/constructive+mathematics" accesskey="S" class="navlink" id="history" rel="nofollow">History (96 revisions)</a> <a href="/nlab/show/constructive+mathematics/cite" style="color: black">Cite</a> <a href="/nlab/print/constructive+mathematics" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/constructive+mathematics" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>