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> predicative 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> predicative 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/15265/#Item_10" 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>Predicative 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+inequality+spaces">axiom of inequality spaces</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> </div> </div> <h1 id="predicative_mathematics">Predicative mathematics</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <ul> <li><a href='#power_classes_vs_no_power_sets_at_all'>Power classes vs no power sets at all</a></li> </ul> <li><a href='#impredicative_axioms'>Impredicative axioms</a></li> <ul> <li><a href='#infinity'>Infinity</a></li> <li><a href='#power_set'>Power set</a></li> <li><a href='#unbounded_separation'>Unbounded separation</a></li> <li><a href='#function_sets'>Function sets</a></li> <li><a href='#bijection_sets'>Bijection sets</a></li> <li><a href='#univalence_axiom'>Univalence axiom</a></li> <li><a href='#excluded_middle'>Excluded middle</a></li> <li><a href='#the_axiom_of_choice'>The axiom of choice</a></li> <li><a href='#propositional_resizing'>Propositional resizing</a></li> <li><a href='#illfounded_structures'>Ill-founded structures</a></li> <li><a href='#impredicative_polymorphism'>Impredicative polymorphism</a></li> </ul> <li><a href='#the_category_of_sets'>The category of sets</a></li> <li><a href='#the_real_numbers'>The real numbers</a></li> <li><a href='#formalising_mathematics'>Formalising mathematics</a></li> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> <li><a href='#discussion'>Discussion</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p><strong>Predicative mathematics</strong> is a way of doing <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a> without allowing impredicative definitions.</p> <p>Informally, a definition is <em>impredicative</em> if it refers to a totality which includes the thing being defined. For example, the definition of a particular real number <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> as the least upper bound of a given set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is impredicative, because it characterizes <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> as a particular element of some set (the upper bounds of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>) which includes <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>. Possibly <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> can be defined in some other way and then proved to be the least upper bound of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, but to define it thus by fiat is impredicative.</p> <p>There are (at least) two broad schools of the <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> of predicative mathematics that don't talk much to each other: one school that uses lower-order forms of <a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a> (or the <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> that this justifies) and <a class="existingWikiWord" href="/nlab/show/classical+logic">classical logic</a>, and a <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive</a> school that uses first-order <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> (or the set theory that this justifies) and <a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic logic</a>. The common ground is that both schools reject <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a>; other axioms may vary. Here we tend to think of what predicative mathematics allows <a class="existingWikiWord" href="/nlab/show/Set">the category of sets</a> to be.</p> <p>Constructive predicativists sometimes accept principles (such as <a class="existingWikiWord" href="/nlab/show/function+sets">function sets</a> and the <a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a>) that classical predicativists must reject because they imply impredicative results using <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>. Such mathematics may be called <em>weakly predicative</em>.</p> <h3 id="power_classes_vs_no_power_sets_at_all">Power classes vs no power sets at all</h3> <p>Another division within predicative mathematics is whether <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a> can be formed but are <a class="existingWikiWord" href="/nlab/show/proper+classes">proper classes</a> instead of sets or <a class="existingWikiWord" href="/nlab/show/large+sets">large sets</a> instead of <a class="existingWikiWord" href="/nlab/show/small+sets">small sets</a>, or whether <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a> simply cannot be formed at all.</p> <p>In the former case, almost everything which could be done in impredicative mathematics could be done in predicative mathematics, only with the requirement that size issues have to be taken into consideration at all times. This is the case with predicative constructive <a class="existingWikiWord" href="/nlab/show/dependent+type+theories">dependent type theories</a> which have <a class="existingWikiWord" href="/nlab/show/type+universes">type universes</a>, where given the type universe <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> one could construct a large <a class="existingWikiWord" href="/nlab/show/type+of+propositions">type of propositions</a> by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ω</mi><mo>≔</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>A</mi><mo>:</mo><mi>U</mi></mrow></msub><mi mathvariant="normal">isProp</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\Omega \coloneqq \sum_{A:U} \mathrm{isProp}(A)</annotation></semantics></math> with power sets as function sets with codomain <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ω</mi></mrow><annotation encoding="application/x-tex">\Omega</annotation></semantics></math>, as well as various notions of <a class="existingWikiWord" href="/nlab/show/class+theory">class theory</a> such as <a class="existingWikiWord" href="/nlab/show/Morse-Kelley+class+theory">Morse-Kelley class theory</a>, where power sets exist as <a class="existingWikiWord" href="/nlab/show/power+classes">power classes</a>. Sometimes, one would have an entire hierarchy of power sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>𝒫</mi> <mi>n</mi></msub><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{P}_n(S)</annotation></semantics></math> for hierarchy level <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>, as is common in <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> with a cumulative hierarchy of universes, with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>𝒫</mi> <mrow><mi>n</mi><mo>+</mo><mn>1</mn></mrow></msub><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{P}_{n + 1}(S)</annotation></semantics></math> larger than <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>𝒫</mi> <mi>n</mi></msub><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{P}_n(S)</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>. This is also the case with <a class="existingWikiWord" href="/nlab/show/Bertrand+Russell">Bertrand Russell</a>‘s original predicative ramified hierarchy of types in <a class="existingWikiWord" href="/nlab/show/Principia+Mathematica">Principia Mathematica</a>. However, there are a few things in mathematics where the hierarchy of power sets isn’t enough to construct or prove them, and one actually needs full impredicativity.</p> <p>When power sets don’t exist at all, whether as a set or a proper class, this results in significantly weaker foundations, since in this case one simply cannot form various mathematical structures which require the use of <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a>, such as the <a class="existingWikiWord" href="/nlab/show/Dedekind+real+numbers">Dedekind real numbers</a>, <a class="existingWikiWord" href="/nlab/show/topological+spaces">topological spaces</a>, <a class="existingWikiWord" href="/nlab/show/frames">frames</a>, and <a class="existingWikiWord" href="/nlab/show/locales">locales</a>. This is usually the case for predicative mathematics done internally in a <a class="existingWikiWord" href="/nlab/show/Heyting+pretopos">Heyting</a> or <a class="existingWikiWord" href="/nlab/show/Boolean+pretopos">Boolean pretopos</a>, as well as for predicative <a class="existingWikiWord" href="/nlab/show/material+set+theories">material set theories</a> like <span class="newWikiWord">Kripke–Platek set theory<a href="/nlab/new/Kripke%E2%80%93Platek+set+theory">?</a></span> which do not have an internal notion of <a class="existingWikiWord" href="/nlab/show/class">class</a>. In <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, this notion of predicativity requires not having any <a class="existingWikiWord" href="/nlab/show/type+universes">type universes</a> in the type theory itself, since otherwise <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>A</mi><mo>:</mo><mi>U</mi></mrow></msub><mi mathvariant="normal">isProp</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{A:U} \mathrm{isProp}(A)</annotation></semantics></math> is a large <a class="existingWikiWord" href="/nlab/show/type+of+propositions">type of propositions</a>. In addition, unlike for <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, not having power sets in <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> results in additional structure like <a class="existingWikiWord" href="/nlab/show/formal+topologies">formal topologies</a> or <a class="existingWikiWord" href="/nlab/show/inductive+covers">inductive covers</a> not being definable in the type theory, since without universes or types of propositions one cannot define relations between elements and subtypes.</p> <h2 id="impredicative_axioms">Impredicative axioms</h2> <p>Not all of these axioms are rejected by all predicativists, but they at least come under some suspicion.</p> <h3 id="infinity">Infinity</h3> <p>The <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a> is not usually considered impredicative, but we list it anyway, as it is needed for the others to have force. Mathematics that does not require this axiom, <a class="existingWikiWord" href="/nlab/show/finite+mathematics">finite mathematics</a>, can be interpreted in a predicative framework even if it uses many of the axioms below.</p> <h3 id="power_set">Power set</h3> <p>The axiom that any set has a <a class="existingWikiWord" href="/nlab/show/power+set">power set</a> is perhaps the fundamental feature missing from predicative mathematics. In particular, the sequence</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi><mo>,</mo><mi>𝒫</mi><mi>ℕ</mi><mo>,</mo><mi>𝒫</mi><mi>𝒫</mi><mi>ℕ</mi><mo>,</mo><mi>…</mi></mrow><annotation encoding="application/x-tex"> \mathbb{N}, \mathcal{P}\mathbb{N}, \mathcal{P}\mathcal{P}\mathbb{N}, \ldots </annotation></semantics></math></div> <p>may be accepted in part, but not forever.</p> <p>The failure of the power set axiom means that the category of sets is not an <a class="existingWikiWord" href="/nlab/show/elementary+topos">elementary topos</a>.</p> <h3 id="unbounded_separation">Unbounded separation</h3> <p>The constructive school generally accepts the <a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a> but not unbounded forms of the <a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a>. (This choice is not available to the classical school, since replacement and <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a> together imply full separation.)</p> <p>Naïvely, the axiom of separation says that, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a set and <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 <a class="existingWikiWord" href="/nlab/show/function">function</a> from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> to the set of <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a>s, then there is a set</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>A</mi><mo stretchy="false">|</mo><mi>P</mi><mo stretchy="false">}</mo><mo>=</mo><mo stretchy="false">{</mo><mi>x</mi><mo>∈</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mo stretchy="false">|</mo><mspace width="thickmathspace"></mspace><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">}</mo><mo>.</mo></mrow><annotation encoding="application/x-tex"> \{ A | P \} = \{ x \in A \;|\; P(x) \} .</annotation></semantics></math></div> <p>To be precise, however, this <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> should be written as a <a class="existingWikiWord" href="/nlab/show/predicate">predicate</a> in the language of set theory. The form of separation justified by type theory and such structural set theories as <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> requires the <a class="existingWikiWord" href="/nlab/show/quantifiers">quantifiers</a> in this predicate to be guarded by sets; unbounded separation is the generalisation of this to arbitrary quantifiers.</p> <p>Arguably, the impredicative core of both separation and power sets (in the presence of bounded separation) is <a class="existingWikiWord" href="/nlab/show/limited+separation">limited separation</a>: separation in which the quantifiers in <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 guarded by power classes.</p> <p><em>We need more on this, particularly with regards to the classical school and replacement.</em></p> <h3 id="function_sets">Function sets</h3> <p>One sometimes speaks of forbidding <a class="existingWikiWord" href="/nlab/show/function+set">function set</a>s instead of power sets. That is, it is the sequence</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi><mo>,</mo><msup><mi>ℕ</mi> <mi>ℕ</mi></msup><mo>,</mo><msup><mi>ℕ</mi> <mrow><msup><mi>ℕ</mi> <mi>ℕ</mi></msup></mrow></msup><mo>,</mo><mi>…</mi></mrow><annotation encoding="application/x-tex"> \mathbb{N}, \mathbb{N}^{\mathbb{N}}, \mathbb{N}^{\mathbb{N}^{\mathbb{N}}}, \ldots </annotation></semantics></math></div> <p>that is avoided.</p> <p>Of course, function sets can be constructed out of power sets (using <em>bounded</em> separation), so forbidding function sets certainly forbids power sets. The converse holds if there is 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">\Omega</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a>s.</p> <p>With <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>, the set of truth values is easy to achieve, as <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></mrow><annotation encoding="application/x-tex">\{0,1\}</annotation></semantics></math>; in particular, if you have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math>, then you certainly have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ω</mi></mrow><annotation encoding="application/x-tex">\Omega</annotation></semantics></math>. So the classical school of predicativism rejects function sets.</p> <p>The constructive school, however, often accepts function sets (thus being <em>weakly</em> predicative). In this school, the sequence above is fine. Actually, the slightly stronger axiom of <a class="existingWikiWord" href="/nlab/show/subset+collection">subset collection</a> is adopted by <a class="existingWikiWord" href="/nlab/show/Peter+Aczel">Peter Aczel</a>'s <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>CZF</mi></mrow><annotation encoding="application/x-tex">CZF</annotation></semantics></math> and justified by <a class="existingWikiWord" href="/nlab/show/Per+Martin-L%C3%B6f">Per Martin-Löf</a>'s <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ITT</mi></mrow><annotation encoding="application/x-tex">ITT</annotation></semantics></math>.</p> <p><a class="existingWikiWord" href="/nlab/show/Brouwer">Brouwer</a>, on the other hand, did not accept the sequence above, although his followers differ on when (if ever) it stops.</p> <h3 id="bijection_sets">Bijection sets</h3> <p>In the presence of the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>, <a class="existingWikiWord" href="/nlab/show/bijection+sets">bijection sets</a> are in bijection with <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a>, and so are impredicative.</p> <h3 id="univalence_axiom">Univalence axiom</h3> <p>One consequence of the rejection of <a class="existingWikiWord" href="/nlab/show/bijection+sets">bijection sets</a> in predicative mathematics with the axiom of choice is that the univalence axiom of a universe of sets is no longer available, since it postulates a bijection between equality and bijection sets.</p> <h3 id="excluded_middle">Excluded middle</h3> <p>Classical predicativists of course accept <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>; otherwise they would be <a class="existingWikiWord" href="/nlab/show/constructivism">constructivists</a>. But from the perspective of weakly predicative constructive mathematics, excluded middle is impredicative, since it implies power sets (given function sets) and unbounded separation (given replacement).</p> <h3 id="the_axiom_of_choice">The axiom of choice</h3> <p>Some classical predicativists accept the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>. But from the perspective of weakly predicative constructive mathematics, the axiom of choice is impredicative, since it implies excluded middle, and thus power sets (given function sets) and unbounded separation (given replacement).</p> <h3 id="propositional_resizing">Propositional resizing</h3> <p>In the constructive school, one would sometimes have multiple sets of propositions, but those only represent the set of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math>-small <a class="existingWikiWord" href="/nlab/show/propositions">propositions</a> or <a class="existingWikiWord" href="/nlab/show/subsingletons">subsingletons</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Ω</mi> <mi>U</mi></msub></mrow><annotation encoding="application/x-tex">\Omega_U</annotation></semantics></math>, given a <a class="existingWikiWord" href="/nlab/show/universe">universe</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math>, rather than the set of all propositions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ω</mi></mrow><annotation encoding="application/x-tex">\Omega</annotation></semantics></math>. In general, given any two universes <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math>, one cannot prove that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Ω</mi> <mi>U</mi></msub></mrow><annotation encoding="application/x-tex">\Omega_U</annotation></semantics></math> is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Ω</mi> <mi>V</mi></msub></mrow><annotation encoding="application/x-tex">\Omega_V</annotation></semantics></math>. This is common in type theoretic models of constructive mathematics.</p> <p>The axiom of <a class="existingWikiWord" href="/nlab/show/propositional+resizing">propositional resizing</a> is then statement that given any two universes <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math>, the sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Ω</mi> <mi>U</mi></msub></mrow><annotation encoding="application/x-tex">\Omega_U</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Ω</mi> <mi>V</mi></msub></mrow><annotation encoding="application/x-tex">\Omega_V</annotation></semantics></math> of propositions in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> respectively are in <a class="existingWikiWord" href="/nlab/show/bijection">bijection</a> with each other <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Ω</mi> <mi>U</mi></msub><mo>≅</mo><msub><mi>Ω</mi> <mi>V</mi></msub></mrow><annotation encoding="application/x-tex">\Omega_U \cong \Omega_V</annotation></semantics></math>. This axiom implies that there is only one set of propositions up to bijection, which in combination with the existence of <a class="existingWikiWord" href="/nlab/show/function+sets">function sets</a> imply <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a>, so is impredicative.</p> <h3 id="illfounded_structures">Ill-founded structures</h3> <p>Most foundations of mathematics are predicative in one sense: no set may belong to itself. This (or rather, a certain strengthening of this) is the <a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a>. An alternative is the axiom of antifoundation, which explicitly allows for and tames such sets as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>•</mo></mrow><annotation encoding="application/x-tex">\bullet</annotation></semantics></math>, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>•</mo><mo>=</mo><mo stretchy="false">{</mo><mo>•</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\bullet = \{\bullet\}</annotation></semantics></math>. Indeed, this equation is a perfectly good way to <em>define</em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>•</mo></mrow><annotation encoding="application/x-tex">\bullet</annotation></semantics></math> using antifoundation, yet this is about as impredicative as a definition can get.</p> <p>Once one accepts the <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a>, there's not much objection to accepting more general <a class="existingWikiWord" href="/nlab/show/inductive+type">inductive type</a>s such as <a class="existingWikiWord" href="/nlab/show/inductive-inductive+types">inductive-inductive types</a> and <a class="existingWikiWord" href="/nlab/show/quotient+inductive+types">quotient inductive types</a>; these are sets that are defined recursively much like a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a>. Categorially, we may see these as <a class="existingWikiWord" href="/nlab/show/initial+algebra">initial algebra</a>s of certain functors on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>. <a class="existingWikiWord" href="/nlab/show/coinductive+type">Coinductive types</a>, which are the <a class="existingWikiWord" href="/nlab/show/terminal+coalgebra">final coalgebra</a>s of these functors, also exist in impredicative theories, but not predicatively.</p> <h3 id="impredicative_polymorphism">Impredicative polymorphism</h3> <p>A different sort of impredicativity, called <a class="existingWikiWord" href="/nlab/show/impredicative+polymorphism">impredicative polymorphism</a> is to be found in some <a class="existingWikiWord" href="/nlab/show/type+theory">type theories</a>, in which, roughly speaking, one is allowed to define “functions” whose “domain” is the class of all types in a <a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a> or a <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>. For instance, one might be able to form a type called <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∀</mo><mi>α</mi><mo>:</mo><mi>Type</mi><mo>,</mo><mi>α</mi><mo>→</mo><mi>α</mi></mrow><annotation encoding="application/x-tex">\forall \alpha:Type, \alpha\to\alpha</annotation></semantics></math>, which has the property that an inhabitant of that type is a “function” which assigns to <em>every</em> type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>, an endomorphism of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>. This is clearly impredicative, since the type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∀</mo><mi>α</mi><mo>:</mo><mi>Type</mi><mo>,</mo><mi>α</mi><mo>→</mo><mi>α</mi></mrow><annotation encoding="application/x-tex">\forall \alpha:Type, \alpha\to\alpha</annotation></semantics></math> is also a possible value of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>.</p> <p>The philosophy behind this sort of impredicative definition is that any inhabitant of such a type must be defined “uniformly” enough that it uses no details about the type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>, and thus can equally well be applied to any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>. For instance, consider the operation which assigns to every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math> the identity <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>id</mi><mo lspace="verythinmathspace">:</mo><mi>α</mi><mo>→</mo><mi>α</mi></mrow><annotation encoding="application/x-tex">id\colon \alpha\to\alpha</annotation></semantics></math>; this is defined in exactly the same way for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>, and hence inhabits the type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∀</mo><mi>α</mi><mo>:</mo><mi>Type</mi><mo>,</mo><mi>α</mi><mo>→</mo><mi>α</mi></mrow><annotation encoding="application/x-tex">\forall \alpha:Type, \alpha\to\alpha</annotation></semantics></math>.</p> <p>This sort of impredicativism can be shown to be incompatible with impredicative set-theoretic axioms such as power sets; see <a href="https://www.cl.cam.ac.uk/~amp12/papers/nontpt/nontpt.pdf">this paper</a> of Andy Pitts. Since such type theories generally do have function types, it follows that they cannot be classical.</p> <p>However, the <a class="existingWikiWord" href="/nlab/show/type+universes">type universes</a> as talked about in the previous paragraphs usually have non-propositional types. There do exist <a class="existingWikiWord" href="/nlab/show/type+universes">type universes</a> which have impredicative polymorphism and are consistent with power sets: these are the <a class="existingWikiWord" href="/nlab/show/universes+of+propositions">universes of propositions</a>, the universes <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ω</mi></mrow><annotation encoding="application/x-tex">\Omega</annotation></semantics></math> where every type is a <a class="existingWikiWord" href="/nlab/show/mere+proposition">mere proposition</a>, and <a class="existingWikiWord" href="/nlab/show/impredicative+polymorphism">impredicative polymorphism</a> says that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ω</mi></mrow><annotation encoding="application/x-tex">\Omega</annotation></semantics></math> is closed under <a class="existingWikiWord" href="/nlab/show/dependent+product+types">dependent product types</a> of <a class="existingWikiWord" href="/nlab/show/predicates">predicates</a> valued in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ω</mi></mrow><annotation encoding="application/x-tex">\Omega</annotation></semantics></math>.</p> <p>In particular, the condition of having a <a class="existingWikiWord" href="/nlab/show/universe+of+all+propositions">universe of all propositions</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">Prop</mi></mrow><annotation encoding="application/x-tex">\mathrm{Prop}</annotation></semantics></math> is exactly that of having <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a> in the type theory, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">Prop</mi></mrow><annotation encoding="application/x-tex">\mathrm{Prop}</annotation></semantics></math> has <a class="existingWikiWord" href="/nlab/show/impredicative+polymorphism">impredicative polymorphism</a> if and only if <a class="existingWikiWord" href="/nlab/show/weak+function+extensionality">weak function extensionality</a> holds, which is equivalent to <a class="existingWikiWord" href="/nlab/show/function+extensionality">function extensionality</a>.</p> <h2 id="the_category_of_sets">The category of sets</h2> <p>So what is the category of sets in predicative mathematics?</p> <p>At bottom, let us suppose that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/Heyting+category">Heyting</a> <a class="existingWikiWord" href="/nlab/show/pretopos">pretopos</a>; this is a category whose <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> is first-order and contains only constructions that don't require any of the above axioms.</p> <p>Since we're not doing finite mathematics, we may also include a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a>. In fact, we could include more general <a class="existingWikiWord" href="/nlab/show/inductive+type">inductive type</a>s, since these are no harder to justify philosophically than <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math>, although the proofs that these exist if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math> does rely on possibly impredicative axioms. Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is a Heyting <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math>-pretopos.</p> <p>If you accept function sets, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/locally+cartesian+closed+category">locally cartesian closed</a> and thus a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Π</mi></mrow><annotation encoding="application/x-tex">\Pi</annotation></semantics></math>-pretopos. In this case, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="0em" rspace="thinmathspace">mathb</mo><mi>N</mi></mrow><annotation encoding="application/x-tex">\mathb{N}</annotation></semantics></math> is enough to get all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/W-type">types</a>, so we have a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Π</mi></mrow><annotation encoding="application/x-tex">\Pi</annotation></semantics></math>-<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math>-pretopos. If you accept excluded middle, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/Boolean+category">Boolean</a> pretopos or even a Boolean <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math>-pretopos. But a Boolean <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Π</mi></mrow><annotation encoding="application/x-tex">\Pi</annotation></semantics></math>-pretopos is necessarily a <a class="existingWikiWord" href="/nlab/show/topos">topos</a>, which would make the theory impredicative.</p> <p>However, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is still a <a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a>, defined as a category of sheaves or in terms of Giraud's characterisation. We require the existence of power sets to prove the theorem that such a category is an elementary topos, so predicatively a Grothendieck topos may not be an elementary topos at all.</p> <h2 id="the_real_numbers">The real numbers</h2> <p>An important question in predicative mathematics is the status of the 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">\mathbb{R}</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/real+number">real number</a>s. This set is often constructed as a subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>R</mi> <mi>D</mi></msub></mrow><annotation encoding="application/x-tex">R_D</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒫</mi><mo stretchy="false">(</mo><mi>ℕ</mi><mo stretchy="false">)</mo><mo>×</mo><mi>𝒫</mi><mo stretchy="false">(</mo><mi>ℕ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{P}(\mathbb{N}) \times \mathcal{P}(\mathbb{N})</annotation></semantics></math> or as a <a class="existingWikiWord" href="/nlab/show/subquotient">subquotient</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>R</mi> <mi>C</mi></msub></mrow><annotation encoding="application/x-tex">R_C</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>ℕ</mi> <mi>ℕ</mi></msup></mrow><annotation encoding="application/x-tex">\mathbb{N}^{\mathbb{N}}</annotation></semantics></math>, neither of which can be formed in an arbitrary Heyting <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math>-pretopos. The latter can be formed in a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Π</mi></mrow><annotation encoding="application/x-tex">\Pi</annotation></semantics></math>-<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math>-pretopos, but it is not necessarily correct.</p> <p>The constructive school of predicativism can construct <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> in various ways. One method is to use <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>R</mi> <mi>C</mi></msub></mrow><annotation encoding="application/x-tex">R_C</annotation></semantics></math> directly, but this will only go so far unless something is done to prove that it is Dedekind-complete. This will follow from <a class="existingWikiWord" href="/nlab/show/weak+countable+choice">weak countable choice</a> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>WCC</mi></mrow><annotation encoding="application/x-tex">WCC</annotation></semantics></math>), which is accepted by some constructive schools. Using <a class="existingWikiWord" href="/nlab/show/subset+collection">subset collection</a>, a variation on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>R</mi> <mi>C</mi></msub></mrow><annotation encoding="application/x-tex">R_C</annotation></semantics></math> is possible which can be proved Dedekind-complete <em>without</em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>WCC</mi></mrow><annotation encoding="application/x-tex">WCC</annotation></semantics></math>.</p> <p>However, not all constructive predicative mathematics accept <a class="existingWikiWord" href="/nlab/show/subset+collection">subset collection</a> or <a class="existingWikiWord" href="/nlab/show/weak+countable+choice">weak countable choice</a>. Another method is to use a predicative version of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>R</mi> <mi>D</mi></msub></mrow><annotation encoding="application/x-tex">R_D</annotation></semantics></math>, where given a <a class="existingWikiWord" href="/nlab/show/sigma-frame"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"> <semantics> <mrow> <mi>σ</mi> </mrow> <annotation encoding="application/x-tex">\sigma</annotation> </semantics> </math>-frame</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/Dedekind+cuts">Dedekind cuts</a> are defined as pairs of functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi><mo>,</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">L, U</annotation></semantics></math> from the <a class="existingWikiWord" href="/nlab/show/rational+numbers">rational numbers</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℚ</mi></mrow><annotation encoding="application/x-tex">\mathbb{Q}</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>, which represent the open subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℚ</mi></mrow><annotation encoding="application/x-tex">\mathbb{Q}</annotation></semantics></math>, rather than pairs of functions into the class of propositions. <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>R</mi> <mi>D</mi></msub></mrow><annotation encoding="application/x-tex">R_D</annotation></semantics></math> is defined as the set of all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>-Dedekind cuts, or as the <a class="existingWikiWord" href="/nlab/show/sigma-Dedekind+complete"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"> <semantics> <mrow> <mi>Σ</mi> </mrow> <annotation encoding="application/x-tex">\Sigma</annotation> </semantics> </math>-Dedekind complete</a> <a class="existingWikiWord" href="/nlab/show/archimedean+field">archimedean field</a>. This will ensure that the set of real numbers is a set rather than a <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a>, at the cost of Dedekind completeness, which always results in a proper class in constructive predicative mathematics. Nevertheless, a significant portion of <a class="existingWikiWord" href="/nlab/show/real+analysis">real analysis</a> could be developed using this approach, such as <a class="existingWikiWord" href="/nlab/show/differential+calculus">differential calculus</a>, <a class="existingWikiWord" href="/nlab/show/integral+calculus">integral calculus</a>, and <a class="existingWikiWord" href="/nlab/show/differential+geometry">differential geometry</a>.</p> <p>It is also possible to assert the existence of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> by fiat, much like <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math> exists by the axiom of infinity. This is the approach taken by the classical school; they use <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒫</mi><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathcal{P}\mathbb{N}</annotation></semantics></math> instead of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> directly, but these are isomorphic by excluded middle. This is natural from the perspective of predicative set theory as a weak form of higher-order logic; you assert the existence of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒫</mi><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathcal{P}\mathbb{N}</annotation></semantics></math>, and maybe <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒫</mi><mi>𝒫</mi><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathcal{P}\mathcal{P}\mathbb{N}</annotation></semantics></math>, then stop.</p> <p>One could also assert <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> by fiat via the <a class="existingWikiWord" href="/nlab/show/universal+property">universal property</a> of the real numbers as the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal</a> <a class="existingWikiWord" href="/nlab/show/Archimedean+ordered+field">Archimedean ordered field</a>. From this characterization, the real numbers are a <a class="existingWikiWord" href="/nlab/show/terminal+coalgebra">terminal coalgebra</a> of the <a class="existingWikiWord" href="/nlab/show/identity+functor">identity endofunctor</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↦</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">X \mapsto X</annotation></semantics></math> on the <a class="existingWikiWord" href="/nlab/show/category">category</a> of <a class="existingWikiWord" href="/nlab/show/Archimedean+ordered+fields">Archimedean ordered fields</a>, and in a sense is impredicative, since coinductively defined sets are impredicative.</p> <p>If <a class="existingWikiWord" href="/nlab/show/quotient+sets">quotient sets</a> exist and <a class="existingWikiWord" href="/nlab/show/sequence+algebras">sequence algebras</a> of Archimedean ordered fields exist, then it is provable that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> is Cauchy complete. From the definition of terminal object, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> is an algebra of the endofunctor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↦</mo><mi>𝒞</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">X \mapsto \mathcal{C}(X)</annotation></semantics></math> in the category of Archimedean ordered fields which takes Archimedean ordered fields <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> to the Archimedean ordered field <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒞</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{C}(X)</annotation></semantics></math> of equivalence classes of Cauchy sequences in <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>. Every algebra of the endofunctor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↦</mo><mi>𝒞</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">X \mapsto \mathcal{C}(X)</annotation></semantics></math> in the category of Archimedean ordered fields is a Cauchy complete Archimedean ordered field.</p> <p>Similarly, if <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a> of Archimedean ordered fields exist, then it is provable that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> is Dedekind complete. From the definition of terminal object, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> is an algebra of the endofunctor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↦</mo><mi>𝒟</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">X \mapsto \mathcal{D}(X)</annotation></semantics></math> in the category of Archimedean ordered fields which takes Archimedean ordered fields <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> to the Archimedean ordered field <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒞</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{C}(X)</annotation></semantics></math> of two-sided Dedekind cuts in <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>. Every algebra of the endofunctor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↦</mo><mi>𝒟</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">X \mapsto \mathcal{D}(X)</annotation></semantics></math> in the category of Archimedean ordered fields is a Dedekind complete Archimedean ordered field.</p> <p>There is also the question of what exactly it means to say that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> exists; is it a set or a <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a>? Without function sets, the distinction between these is not clear-cut; higher-order logic suggests a hierarchy of more and more proper (less and less <a class="existingWikiWord" href="/nlab/show/small+category">small</a>) classes rather than a single unified notion of set and class, which is similar to the concept of a <a class="existingWikiWord" href="/nlab/show/universe+in+a+topos">universe in a topos</a> for impredicative set theory. If you allow <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> only as a proper class, then you are doing predicative mathematics so long as you don’t have <a class="existingWikiWord" href="/nlab/show/power+classes">power classes</a>, if you allow <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> as a set, then as long as you don’t allow all <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a> or <a class="existingWikiWord" href="/nlab/show/power+classes">power classes</a>, you are still doing predicative mathematics in the same sense that foundations in which only the <a class="existingWikiWord" href="/nlab/show/limited+principle+of+omniscience">limited principle of omniscience</a> holds but not full <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a> is still constructive mathematics.</p> <h2 id="formalising_mathematics">Formalising mathematics</h2> <p>How much of mathematics can be done predicatively?</p> <p>A surprisingly large amount of mathematics can be formalised, using various coding tricks, in a theory in which <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math> is a set but <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒫</mi><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathcal{P}\mathbb{N}</annotation></semantics></math> is a proper class. This is somewhat easier in <a class="existingWikiWord" href="/nlab/show/Nik+Weaver">Nik Weaver</a>'s ‘conceptualist’ approach, which accepts <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒫</mi><mi>𝒫</mi><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathcal{P}\mathcal{P}\mathbb{N}</annotation></semantics></math> as a proper class (so that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒫</mi><mi>N</mi></mrow><annotation encoding="application/x-tex">\mathcal{P}N</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> are small); the encoding is not really more complicated than what is usually done in <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> for ordered pairs and the like. Note that these are conservative over <a class="existingWikiWord" href="/nlab/show/Peano+arithmetic">Peano arithmetic</a> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>PA</mi></mrow><annotation encoding="application/x-tex">PA</annotation></semantics></math>); that is, anything expressible in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>PA</mi></mrow><annotation encoding="application/x-tex">PA</annotation></semantics></math> and provable in these systems is provable in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>PA</mi></mrow><annotation encoding="application/x-tex">PA</annotation></semantics></math> (which certainly cannot be said of <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> or <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>, which prove the consistency of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>PA</mi></mrow><annotation encoding="application/x-tex">PA</annotation></semantics></math>).</p> <p>Constructive mathematics generally requires great care with anything after the middle of the 19th century other than basic <a class="existingWikiWord" href="/nlab/show/discrete+mathematics">discrete mathematics</a>, but requiring it to be predicative does not usually add much difficulty, as long as function sets are allowed. This even extends to <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>, which is not usually contemplated in the classical approach. (However, the internal logic of a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Π</mi></mrow><annotation encoding="application/x-tex">\Pi</annotation></semantics></math>-<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math>-pretopos is certainly not conservative over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>PA</mi></mrow><annotation encoding="application/x-tex">PA</annotation></semantics></math>; it already proves consistency of the latter.)</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/predicative+topos">predicative topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/impredicative+dependent+type+theory">impredicative dependent type theory</a></p> </li> </ul> <h2 id="references">References</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Solomon+Feferman">Solomon Feferman</a>; <a href="http://hlombardi.free.fr/FefermanRelationships.pdf">Relationships between Constructive, Predicative and Classical Systems of Analysis</a> (PDF).</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Nik+Weaver">Nik Weaver</a>, <a href="https://web.archive.org/web/20100616093000/https://www.math.wustl.edu/~nweaver/conceptualism.html">papers on conceptualism</a>.</p> </li> <li> <p>from the Standford Encyclopedia of Philosophy:</p> <ul> <li><a href="http://plato.stanford.edu/entries/set-theory-constructive/#PreConSetThe">Predicativity in constructive set theory</a>.</li> <li><a href="http://plato.stanford.edu/entries/philosophy-mathematics/index.html#Pre">Predicativism</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Nik+Weaver">Nik Weaver</a>, <em>Predicativity beyond Gamma_0</em> (<a href="https://arxiv.org/abs/math/0509244">arXiv:math/0509244</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Nik+Weaver">Nik Weaver</a>, <em>Predicative well-ordering</em> (<a href="https://arxiv.org/abs/1811.03543">arXiv:1811.03543</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Nik+Weaver">Nik Weaver</a>, <em>Hierarchies of Tarskian truth predicates</em> (<a href="https://arxiv.org/abs/2202.00851">arXiv:2202.00851</a>)</p> </li> </ul> <p>Discussion of <a class="existingWikiWord" href="/nlab/show/predicative+toposes">predicative toposes</a> is in</p> <ul id="vdBerg"> <li> <p><a class="existingWikiWord" href="/nlab/show/Ieke+Moerdijk">Ieke Moerdijk</a>, <a class="existingWikiWord" href="/nlab/show/Erik+Palmgren">Erik Palmgren</a>, <em>Type theories, toposes and constructive set theory: predicative aspects of <a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></em> Ann. Pure Appl. Logic, 114(1-3):155–201, 2002</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Benno+van+den+Berg">Benno van den Berg</a>, <em>Predicative toposes</em> (<a href="http://arxiv.org/abs/1207.0959">arXiv:1207.0959</a>)</p> </li> </ul> <p>Constructive predicative definitions of the real numbers are discussed in</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Paul+Taylor">Paul Taylor</a>'s <a href="http://www.paultaylor.eu/ASD/dedras/classical">page on Dedekind cuts</a></p> </li> <li> <p>Univalent Foundations Project, <a class="existingWikiWord" href="/nlab/show/HoTT+book">Homotopy Type Theory – Univalent Foundations of Mathematics</a> (2013)</p> </li> </ul> <h2 id="discussion">Discussion</h2> <p>A discussion was had on this page, now <a href="https://nforum.ncatlab.org/discussion/15265/predicative-mathematics/?Focus=103587#Comment_103587">archived at the nForum</a></p> </body></html> </div> <div class="revisedby"> <p> Last revised on September 19, 2024 at 18:37:47. See the <a href="/nlab/history/predicative+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/predicative+mathematics" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/15265/#Item_10">Discuss</a><span class="backintime"><a href="/nlab/revision/predicative+mathematics/38" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/predicative+mathematics" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/predicative+mathematics" accesskey="S" class="navlink" id="history" rel="nofollow">History (38 revisions)</a> <a href="/nlab/show/predicative+mathematics/cite" style="color: black">Cite</a> <a href="/nlab/print/predicative+mathematics" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/predicative+mathematics" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>