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> foundation of 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> foundation of 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/4172/#Item_29" 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>Contents</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="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#Idea'>Idea</a></li> <li><a href='#deductive_systems'>Deductive systems</a></li> <ul> <li><a href='#dependent_type_theory'>Dependent type theory</a></li> </ul> <li><a href='#basic_notions'>Basic notions</a></li> <ul> <li><a href='#objects_and_collections'> Objects and collections</a></li> <li><a href='#membership_and_typing'>Membership and typing</a></li> <li><a href='#equality_and_equivalence'>Equality and equivalence</a></li> <li><a href='#size_issues_universes_and_classes'>Size issues, universes, and classes</a></li> </ul> <li><a href='#Concrete'>Effect of foundations on concrete problems</a></li> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#section_Philosophical_musings'>Philosophical musings</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="Idea">Idea</h2> <p>In the context of <em>foundations of mathematics</em> or <em><a class="existingWikiWord" href="/nlab/show/mathematical+logic">mathematical logic</a></em> one studies formal systems – <a class="existingWikiWord" href="/nlab/show/theories">theories</a> – that allow us to formalize much if not all of <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a> (and hence, by extension, at least aspects of mathematical fields such as fundamental <a class="existingWikiWord" href="/nlab/show/physics">physics</a>).</p> <p>There are two different attitudes to what a desirable or interesting foundation should achieve:</p> <ol> <li> <p>In <strong><a class="existingWikiWord" href="/nlab/show/proof+theory">proof-theoretic</a> foundations</strong> the emphasis is on seeing which formal systems, however convoluted they may be conceptually, allow us to formalize and prove which <a class="existingWikiWord" href="/nlab/show/theorems">theorems</a>.</p> <p>The archetypical such system is <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>. Other formal systems of interest here are <a class="existingWikiWord" href="/nlab/show/elementary+function+arithmetic">elementary function arithmetic</a> and <a class="existingWikiWord" href="/nlab/show/second+order+arithmetic">second order arithmetic</a>, because they are <a class="existingWikiWord" href="/nlab/show/proof+theory">proof-theoretically</a> weak, and still can derive “almost all of undergraduate mathematics” (<a href="#Harrington">Harrington</a>).</p> </li> <li> <p>In <strong><a class="existingWikiWord" href="/nlab/show/practical+foundations">practical foundations</a></strong> (following a term introduced in (<a href="#Taylor">Taylor</a>)) the emphasis is on conceptually natural formalizations that <em>concentrate the essence of practice and in turn use the result to guide practice</em> (<a href="#Lawvere">Lawvere</a>), as in (<a href="#EilenbergSteenrod">Eilenberg-Steenrod</a>, <a href="#Harper">Harper</a>).</p> <p>Formal systems of interest here are <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> or flavors of <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, which allow natural expressions for central concepts in mathematics (notably via their <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> and the conceptual strength of <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>).</p> </li> </ol> <p>For a philosophical treatment of foundations see <a class="existingWikiWord" href="/nlab/show/foundations+and+philosophy">foundations and philosophy</a>.</p> <h2 id="deductive_systems">Deductive systems</h2> <p>Almost all <a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a> are expressed in some foundational <a class="existingWikiWord" href="/nlab/show/deductive+system">deductive system</a>.</p> <p>One versatile deductive system <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a>, which could be used to define certain foundation of mathematics using <a class="existingWikiWord" href="/nlab/show/logic+over+type+theory">logic over type theory</a>, such as all <a class="existingWikiWord" href="/nlab/show/set+theories">set theories</a>, including <a class="existingWikiWord" href="/nlab/show/categorical+set+theories">categorical set theories</a> like <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>, as well as the foundations of mathematics using only <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, including <a class="existingWikiWord" href="/nlab/show/set-level+type+theories">set-level type theories</a> as well as <a class="existingWikiWord" href="/nlab/show/higher+foundations">higher foundations</a> such as <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, as well as typed <a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a>.</p> <p>Alternatives include <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a> for logic over untyped theories, such as <a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a> and untyped higher-order logic, as well as <a class="existingWikiWord" href="/nlab/show/lambda-calculus">lambda-calculus</a> for <a class="existingWikiWord" href="/nlab/show/type+theories">type theories</a>.</p> <h3 id="dependent_type_theory">Dependent type theory</h3> <p>Dependent type theory itself supports various <a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a> via the <a class="existingWikiWord" href="/nlab/show/propositions+as+some+types">propositions as some types</a> interpretation of <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>. Suppose that a dependent type theory has a separate type judgment as well as <a class="existingWikiWord" href="/nlab/show/dependent+product+types">dependent product types</a>, <a class="existingWikiWord" href="/nlab/show/dependent+sum+types">dependent sum types</a>, <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a>, <a class="existingWikiWord" href="/nlab/show/weak+function+extensionality">weak function extensionality</a>, <a class="existingWikiWord" href="/nlab/show/propositional+truncations">propositional truncations</a>, <a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a>, <a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a>, <a class="existingWikiWord" href="/nlab/show/sum+types">sum types</a>. All the operations in <a class="existingWikiWord" href="/nlab/show/predicate+logic">predicate logic</a> are derivable from said type formers. Then:</p> <ul> <li> <p>One can add a <a class="existingWikiWord" href="/nlab/show/cumulative+hierarchy">cumulative hierarchy</a> to the dependent type theory and work entirely in the cumulative hierarchy for <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a></p> </li> <li> <p>One can add a <a class="existingWikiWord" href="/nlab/show/category+of+sets">category of sets</a> to the dependent type theory and work entirely in the category of sets for <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a></p> </li> <li> <p>One can add a <a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a> satisfying certain <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a> and <a class="existingWikiWord" href="/nlab/show/axiom+schemata">axiom schemata</a>, such as <a class="existingWikiWord" href="/nlab/show/universe+extensionality">universe extensionality</a>, closure under identity types, closure under dependent sum types, closure under dependent product types, <a class="existingWikiWord" href="/nlab/show/propositional+resizing">propositional resizing</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">replacement</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">infinity</a>, and <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">choice</a>, to the dependent type theory and work entirely in the universe for <a class="existingWikiWord" href="/nlab/show/univalent+type+theory">univalent type theory</a> or <a class="existingWikiWord" href="/nlab/show/univalent+foundations">univalent foundations</a>. Adding internal universe types as <a class="existingWikiWord" href="/nlab/show/small">small</a> <a class="existingWikiWord" href="/nlab/show/object+classifiers">object classifiers</a> as well as all <a class="existingWikiWord" href="/nlab/show/higher+inductive+types">higher inductive</a> and <a class="existingWikiWord" href="/nlab/show/coinductive+types">coinductive types</a> to the universe results in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>.</p> </li> <li> <p>One can add a <a class="existingWikiWord" href="/nlab/show/Russell+type+of+all+propositions">Russell type of all propositions</a> and a <a class="existingWikiWord" href="/nlab/show/natural+numbers+type">natural numbers type</a> and work in the dependent type theory itself for <a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a>.</p> </li> </ul> <h2 id="basic_notions">Basic notions</h2> <h3 id="objects_and_collections"> Objects and collections</h3> <p>In most foundations of mathematics, there are basic notions of objects and collections of objects.</p> <p>Note that in certain foundations, the objects, collections, and membership are derived notions from some other notion. Collections are referred to a number of names, such as <a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/class">class</a>, <a class="existingWikiWord" href="/nlab/show/type">type</a>, et cetera. Objects could be referred to as <a class="existingWikiWord" href="/nlab/show/element">element</a> or <a class="existingWikiWord" href="/nlab/show/term">term</a>.</p> <p>For example, in <a class="existingWikiWord" href="/nlab/show/pure+set">pure set</a> theories like <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> and <a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a>, elements and sets are the same notion, and thus elements could be considered to be a derived notion from set, or sets could be considered to be a derived notion from element. In <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> with <a class="existingWikiWord" href="/nlab/show/urelements">urelements</a>, such as <a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a>, elements are the basic notion and sets are derived from elements. In <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>, while sets are basic, elements are derived from a basic notion of <a class="existingWikiWord" href="/nlab/show/function">function</a>, and in <a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a>, both sets and elements are derived notions from a basic notion of <a class="existingWikiWord" href="/nlab/show/function">function</a>. In <a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a> and <a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a>, sets and elements are both basic distinct notions.</p> <p>Something similar occurs with <a class="existingWikiWord" href="/nlab/show/class+theories">class theories</a>, such as <a class="existingWikiWord" href="/nlab/show/Morse-Kelley+class+theory">Morse-Kelley class theory</a> and the framework of <a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a>, where classes play the role of sets.</p> <p>In type theory, there are also a distinction to be made. In most type theories, both terms and types are basic foundational notions. However, in <a class="existingWikiWord" href="/nlab/show/book+HoTT">book HoTT</a>, terms are the basic notion, and <a class="existingWikiWord" href="/nlab/show/types">types</a> are derived from terms.</p> <p>In <a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a>, the <a class="existingWikiWord" href="/nlab/show/domain+of+discourse">domain of discourse</a> and higher-order <a class="existingWikiWord" href="/nlab/show/predicates">predicates</a> play the role of collections, while the objects in the <a class="existingWikiWord" href="/nlab/show/domain+of+discourse">domain of discourse</a> play the role of the elements.</p> <h3 id="membership_and_typing">Membership and typing</h3> <p>In most foundations, there is a basic notion of membership, of an “object being in a collection”.</p> <p>Foundations could be contrasted between those foundations where membership is a <a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a>, and those foundations where membership is a <span class="newWikiWord">typing judgment<a href="/nlab/new/typing+judgment">?</a></span>. This distinction is largely the same distinction as the distinction between <a class="existingWikiWord" href="/nlab/show/unsorted+set+theories">unsorted set theories</a> and <a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theories">simply sorted set theories</a> on one hand, and <a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theories">dependently sorted set theories</a> and <a class="existingWikiWord" href="/nlab/show/dependent+type+theories">dependent type theories</a> on the other hand.</p> <p>For theories with a membership relation, one could further distinguish between <a class="existingWikiWord" href="/nlab/show/homogeneous+membership+relations">homogeneous membership relations</a> (for relations on the same sort) and <a class="existingWikiWord" href="/nlab/show/heterogeneous+membership+relations">heterogeneous membership relations</a> (for relations between two different sorts), as well as membership relations which are primitive to the theory, and membership relations which are derived from some other existing structure in the theory.</p> <p>For theories with a typing judgment, one simply judges the object, element, or term <span class="mathematics">a</span> to be in the collection, set, or type <span class="mathematics">A</span>, () or <span class="mathematics">a:A</span>. This is in contrast to membership relations, where () is a proposition with some truth value, and thus one could say whether the proposition that the object, element, or term <span class="mathematics">a</span> is in collection, set, or type <span class="mathematics">A</span> is true or not.</p> <p>Formally, there are also a difference in the contexts. When () or <span class="mathematics">a:A</span> is a judgment, then it lies in the type layer, but when () is a true proposition, then it lies in the proposition layer <span class="mathematics">Φ</span> while the typing judgment <span class="mathematics">a:</span>Set lies in the type layer.</p> <h3 id="equality_and_equivalence">Equality and equivalence</h3> <p>In most foundations such as <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> and <a class="existingWikiWord" href="/nlab/show/logic+over+type+theory">logic over type theory</a>, one distinguishes various different notions of <em><a class="existingWikiWord" href="/nlab/show/equality">equality</a></em> or <em><a class="existingWikiWord" href="/nlab/show/equivalence">equivalence</a></em> of the terms of the language.</p> <p>There are broadly three different notions of equality which could be distinguished: <strong><a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a></strong>, <strong><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></strong>, and <strong><a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a></strong>, each of which applies for both objects (elements, terms) and collections (sets, classes, types). Judgmental equality is defined as a basic judgment in the foundations. Propositional equality is defined as a proposition in any <a class="existingWikiWord" href="/nlab/show/typed+predicate+logic">typed predicate logic</a>. Typal equality is defined as a type in type theory, and is also called the <a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a> or <a class="existingWikiWord" href="/nlab/show/path+type">path type</a> for elements, and the <a class="existingWikiWord" href="/nlab/show/type+of+equivalences">type of equivalences</a> for types.</p> <p>The equality of elements used in most <a class="existingWikiWord" href="/nlab/show/set+theories">set theories</a> and <a class="existingWikiWord" href="/nlab/show/class+theories">class theories</a> are <a class="existingWikiWord" href="/nlab/show/propositional+equalities">propositional equalities</a>. The equality of elements used in <a class="existingWikiWord" href="/nlab/show/dependent+type+theories">dependent type theories</a> are <a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a>. If the dependent type theory is not an <a class="existingWikiWord" href="/nlab/show/objective+type+theory">objective type theory</a>, most likely it also either has one of <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a> or <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a> to use for <a class="existingWikiWord" href="/nlab/show/definitions">definitions</a>.</p> <p>The equality of collections differs from theory to theory. There are <a class="existingWikiWord" href="/nlab/show/set+theories">set theories</a> and <a class="existingWikiWord" href="/nlab/show/class+theories">class theories</a> where <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a> is used as the notion of <a class="existingWikiWord" href="/nlab/show/equality">equality</a> between sets and classes, while for other set theories and class theories, the notion of equality between sets and classes is rather <a class="existingWikiWord" href="/nlab/show/bijection">bijection</a> of sets and classes, rather than equality of sets and classes. Something similar happens in dependent type theory, depending on whether one uses a separate type judgment, or <a class="existingWikiWord" href="/nlab/show/Russell+universes">Russell universes</a> without a separate type judgment: for Russell universes, the <a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a> is used for the equality of types in the universe, since types are terms of Russell universes. On the other hand, the dependent type theories with a separate type judgment, there is no identity type between two types, and one has to use the <a class="existingWikiWord" href="/nlab/show/type+of+equivalences">type of equivalences</a> instead.</p> <p>A mathematical foundation is said to respect the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a> if there is no strict <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a> between sets. Thus, any <a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a> like <a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a> violates the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a>.</p> <h3 id="size_issues_universes_and_classes">Size issues, universes, and classes</h3> <p>In most foundations of mathematics, there is no way to talk about the collection of all collections; this is known as <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a> in <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a>. However, there is a way around it, by the usage of <a class="existingWikiWord" href="/nlab/show/universes">universes</a>. Essentially, instead of trying to talk about the collection of all sets, one instead talks about the collection <span class="mathematics">U</span>, whose elements are called <strong><span class="mathematics">U</span>-<a class="existingWikiWord" href="/nlab/show/small+sets">small sets</a></strong> or <strong><span class="mathematics">U</span>-small types</strong>, and whose <a class="existingWikiWord" href="/nlab/show/subsets">subsets</a> or <a class="existingWikiWord" href="/nlab/show/subtypes">subtypes</a> are called <strong><span class="mathematics">U</span>-<a class="existingWikiWord" href="/nlab/show/classes">classes</a></strong>. The objects not in <span class="mathematics">U</span> are called <strong><span class="mathematics">U</span>-<a class="existingWikiWord" href="/nlab/show/large+sets">large sets</a></strong> or <strong><span class="mathematics">U</span>-large types</strong>, and the <a class="existingWikiWord" href="/nlab/show/subsets">subsets</a> or <a class="existingWikiWord" href="/nlab/show/subtypes">subtypes</a> which are not <a class="existingWikiWord" href="/nlab/show/singleton+subsets">singleton subsets</a> or subtypes are called <strong><span class="mathematics">U</span>-<a class="existingWikiWord" href="/nlab/show/proper+classes">proper classes</a></strong>. Each foundations of mathematics has their own approach to <a class="existingWikiWord" href="/nlab/show/universes">universes</a>:</p> <ul> <li> <p>In <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, one usually either uses <a class="existingWikiWord" href="/nlab/show/Grothendieck+universes">Grothendieck universes</a>, or some internal model of <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> or <a class="existingWikiWord" href="/nlab/show/class+theory">class theory</a>, whether <a class="existingWikiWord" href="/nlab/show/well-pointed+category">well-pointed</a> <a class="existingWikiWord" href="/nlab/show/Heyting+categories">Heyting categories</a>, <a class="existingWikiWord" href="/nlab/show/well-pointed+category">well-pointed</a> <a class="existingWikiWord" href="/nlab/show/division+allegories">division allegories</a>, <a class="existingWikiWord" href="/nlab/show/sets">sets</a> with <a class="existingWikiWord" href="/nlab/show/extensional+relation">extensional</a> <a class="existingWikiWord" href="/nlab/show/well-founded+relation">well-founded</a> <a class="existingWikiWord" href="/nlab/show/transitive+relation">transitive</a> relations, <a class="existingWikiWord" href="/nlab/show/categories+with+class+structure">categories with class structure</a>, et cetera.</p> </li> <li> <p>In <a class="existingWikiWord" href="/nlab/show/class+theory">class theory</a>, the notion of universe is already in the theory via the <a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a>, which is by definition a <a class="existingWikiWord" href="/nlab/show/class">class</a> <a class="existingWikiWord" href="/nlab/show/universe">universe</a>. The basic primitive in class theory are <a class="existingWikiWord" href="/nlab/show/classes">classes</a>, and the <span class="mathematics">U</span>-small classes are called <a class="existingWikiWord" href="/nlab/show/sets">sets</a>.</p> </li> <li> <p>In <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, one uses <a class="existingWikiWord" href="/nlab/show/univalent+universe">univalent</a> <a class="existingWikiWord" href="/nlab/show/Russell+universes">Russell universes</a> or <a class="existingWikiWord" href="/nlab/show/Tarski+universes">Tarski universes</a>, which are basically internal models of <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>.</p> </li> </ul> <h2 id="Concrete">Effect of foundations on concrete problems</h2> <p>It may seem on first sight that foundational questions in mathematics are remote from “real mathematics”. This is not quite so. For a list of “real world” problems that do depend on foundations see</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/effects+of+foundations+on+%22real%22+mathematics">effects of foundations on "real" mathematics</a></li> </ul> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/New+Foundations">New Foundations</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/univalent+foundations+for+mathematics">univalent foundations for mathematics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/synthetic+mathematics">synthetic mathematics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/category+theory+and+foundations">category theory and foundations</a></p> </li> </ul> <p><h2 id='section_Philosophical_musings'>Philosophical musings</h2></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Gravity+and+grace">Gravity and grace</a>, Simone Weil.</li> </ul> <h2 id="references">References</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Bertrand+Russell">Bertrand Russell</a>, <em><a class="existingWikiWord" href="/nlab/show/Principia+Mathematica">Principia Mathematica</a></em>, 1910</p> </li> <li id="Lawvere"> <p><a class="existingWikiWord" href="/nlab/show/William+Lawvere">William Lawvere</a>, <em>Foundations and applications: axiomatization and education</em>, Bulletin of Symbolic Logic 9 (2003), 213-224 (<a href="http://www.math.ucla.edu/~asl/bsl/0902/0902-006.ps">ps</a>, <a href="http://projecteuclid.org/euclid.bsl/1052669290">Euclid</a>)</p> </li> <li id="Harrington"> <p>L. A. Harrington (ed.), <em>Harvey Friedman’s Research on the Foundations of Mathematics</em>, Studies in Logic and the Foundations of Mathematics (2012)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Stefania+Centrone">Stefania Centrone</a>, <a class="existingWikiWord" href="/nlab/show/Deborah+Kant">Deborah Kant</a>, <a class="existingWikiWord" href="/nlab/show/Deniz+Sarikaya">Deniz Sarikaya</a> (editors), <em><a class="existingWikiWord" href="/nlab/show/Reflections+on+the+Foundations+of+Mathematics">Reflections on the Foundations of Mathematics</a></em>, Synthese Library <strong>407</strong> Springer (2019) [<a href="https://doi.org/10.1007/978-3-030-15655-8">doi:10.1007/978-3-030-15655-8</a>]</p> </li> </ul> <p><a class="existingWikiWord" href="/nlab/show/practical+foundations">Practical foundations</a> in terms of <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> language are laid out in</p> <ul id="Taylor"> <li><a class="existingWikiWord" href="/nlab/show/Paul+Taylor">Paul Taylor</a>, <em><a class="existingWikiWord" href="/nlab/show/Practical+Foundations+of+Mathematics">Practical Foundations of Mathematics</a></em>, Cambridge University Press (<a href="http://www.paultaylor.eu/~pt/prafm/index.html">web</a>)</li> </ul> <p>Under <a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a> this corresponds to a practical foundation in <a class="existingWikiWord" href="/nlab/show/program">programming</a>, laid out in</p> <ul id="Harper"> <li><a class="existingWikiWord" href="/nlab/show/Robert+Harper">Robert Harper</a>, <em><a class="existingWikiWord" href="/nlab/show/Practical+Foundations+for+Programming+Languages">Practical Foundations for Programming Languages</a></em> (<a href="https://www.cs.cmu.edu/~rwh/pfpl/">web</a>)</li> </ul> <p>A classification of <a class="existingWikiWord" href="/nlab/show/material+set+theories">material set theories</a> and <a class="existingWikiWord" href="/nlab/show/structural+set+theories">structural set theories</a> is in</p> <ul id="Shulman2018"> <li><a class="existingWikiWord" href="/nlab/show/Michael+Shulman">Michael Shulman</a> (2018). Comparing material and structural set theories. <a href="https://arxiv.org/abs/1808.05204">arXiv:1808.05204</a>.</li> </ul> <p>A foundation for <a class="existingWikiWord" href="/nlab/show/algebraic+topology">algebraic topology</a> in this practical spirit is laid out in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Samuel+Eilenberg">Samuel Eilenberg</a>, <a class="existingWikiWord" href="/nlab/show/Norman+Steenrod">Norman Steenrod</a>, <em><a class="existingWikiWord" href="/nlab/show/Foundations+of+Algebraic+Topology">Foundations of Algebraic Topology</a></em></li> </ul> <p>A big picture intro to the comparison between set theory, type theory and topos/category theory as approaches to foundations is in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Steve+Awodey">Steve Awodey</a>, <em>From Sets to Types to Categories to Sets</em> <a href="http://www.andrew.cmu.edu/user/awodey/preprints/stcsFinal.pdf">pdf</a></li> </ul> <p>A comparative discussion of complexities of different foundations is in</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Freek+Wiedijk">Freek Wiedijk</a>, <em>Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics</em> (<a href="http://www.cs.ru.nl/~freek/zfc-etc/zfc-etc.pdf">pdf</a>)</p> <p><strong>Abstract</strong> This paper presents <a class="existingWikiWord" href="/nlab/show/Automath">Automath</a> encodings (which also are valid in LF/P) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to find out which foundation is the simplest.</p> <p>The systems analyzed in this way are two kinds of <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> (ZFC and NF), two systems based on Church’s <a class="existingWikiWord" href="/nlab/show/higher+order+logic">higher order logic</a> (<a class="existingWikiWord" href="/nlab/show/Isabelle">Isabelle</a>/Pure and <a class="existingWikiWord" href="/nlab/show/HOL">HOL</a>), three kinds of <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> (the <a class="existingWikiWord" href="/nlab/show/calculus+of+constructions">calculus of constructions</a>, Luo’s extended calculus of constructions, and Martin-Löf predicative type theory) and one <a class="existingWikiWord" href="/nlab/show/ETCS">foundation based on category theory</a>. The conclusions of this paper are that the simplest system is type theory (the calculus of constructions) but that type theories that know about serious mathematics are not simple at all. Set theory is one of the simpler systems too. Higher order logic is the simplest if one looks at the number of concepts (twenty-five) needed to explain the system. On the other side of the scale, category theory is relatively complex, as is Martin-Löf’s type theory.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Colin+McLarty">Colin McLarty</a>, <em>Set theory for Grothendieck’s number theory</em>, <a href="http://www.cwru.edu/artsci/phil/Groth%20found.pdf">pdf</a></p> </li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on January 7, 2024 at 14:47:27. See the <a href="/nlab/history/foundation+of+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/foundation+of+mathematics" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/4172/#Item_29">Discuss</a><span class="backintime"><a href="/nlab/revision/foundation+of+mathematics/114" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/foundation+of+mathematics" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/foundation+of+mathematics" accesskey="S" class="navlink" id="history" rel="nofollow">History (114 revisions)</a> <a href="/nlab/show/foundation+of+mathematics/cite" style="color: black">Cite</a> <a href="/nlab/print/foundation+of+mathematics" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/foundation+of+mathematics" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>