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> structural set theory 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> structural set theory </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/111/#Item_34" 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+tight+apartness">axiom of tight apartness</a></p> </li> </ul> </div> <h2 id="removing_axioms">Removing axioms</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> </ul> <div> <p> <a href="/nlab/edit/foundations+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#Examples'>Examples</a></li> <ul> <li><a href='#ETCS'>Elementary theory of the category of sets (ETCS)</a></li> <li><a href='#sets_elements_and_relations_sear'>Sets, Elements and Relations (SEAR)</a></li> <li><a href='#structural_zfc'>Structural ZFC</a></li> <li><a href='#local_set_theory'>Local set theory</a></li> <li><a href='#setoids'>Setoids</a></li> <li><a href='#InHomotopyTypeTheory'>Homotopy-sets in homotopy type theory</a></li> </ul> <li><a href='#related_pages'>Related Pages</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>A <strong>structural set theory</strong> is a <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> which describes <a class="existingWikiWord" href="/nlab/show/structuralism">structural</a> mathematics, and <em>only</em> <a class="existingWikiWord" href="/nlab/show/structuralism">structural</a> mathematics: Sets are conceived as <a class="existingWikiWord" href="/nlab/show/objects">objects</a> that have <a class="existingWikiWord" href="/nlab/show/elements">elements</a>, and are related to each other by <a class="existingWikiWord" href="/nlab/show/functions">functions</a> or <a class="existingWikiWord" href="/nlab/show/relations">relations</a>. In the most common structural set theories such as <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>, sets are characterized by the functions between them, i.e. by the <a class="existingWikiWord" href="/nlab/show/category">category</a> (“<a class="existingWikiWord" href="/nlab/show/Set">Set</a>”) which they form (<a href="#Lawvere65">Lawvere 65</a>). This is what essentially all the application of <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> in the practice of <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a> actually uses – a point amplified by the approach of the introductory textbook <a href="#LawvereRosebrugh03">Lawvere-Rosebrugh 03</a>.</p> <p>This is in contrast to traditional <em><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a></em> (cf <em><a class="existingWikiWord" href="/nlab/show/material+versus+structural">material versus structural</a></em>) such as <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> or <a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a>, where sets are characterized by the membership relation “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∈</mo></mrow><annotation encoding="application/x-tex">\in</annotation></semantics></math>” and <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a> of sets “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>=</mo></mrow><annotation encoding="application/x-tex">=</annotation></semantics></math>” alone, and where sets can be elements of other sets, hence where there are sequences of sets which are elements of the next set in the sequence. This latter feature, however, is almost never actually used or even considered in <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a>, away from the study of <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> itself.</p> <p>As conceived by the <a class="existingWikiWord" href="/nlab/show/structuralism">structuralist</a>, <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a> is the study of structures whose form is independent of the particular attributes of the things that make them up. For instance, in <a class="existingWikiWord" href="/nlab/show/ZF">ZF</a> <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, “the set of natural numbers” can be defined as the von Neumann naturals <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>ω</mi> <mi>N</mi></msub><mo>=</mo><mo stretchy="false">{</mo><mi>∅</mi><mo>,</mo><mo stretchy="false">{</mo><mi>∅</mi><mo stretchy="false">}</mo><mo>,</mo><mo stretchy="false">{</mo><mi>∅</mi><mo>,</mo><mo stretchy="false">{</mo><mi>∅</mi><mo stretchy="false">}</mo><mo stretchy="false">}</mo><mo>,</mo><mi>…</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\omega_N = \{ \emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}, \dots \}</annotation></semantics></math> or alternately as the Zermelo naturals <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>ω</mi> <mi>Z</mi></msub><mo>=</mo><mo stretchy="false">{</mo><mi>∅</mi><mo>,</mo><mo stretchy="false">{</mo><mi>∅</mi><mo stretchy="false">}</mo><mo>,</mo><mo stretchy="false">{</mo><mo stretchy="false">{</mo><mi>∅</mi><mo stretchy="false">}</mo><mo stretchy="false">}</mo><mo>,</mo><mi>…</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\omega_Z = \{ \emptyset, \{\emptyset\}, \{\{\emptyset\}\}, \dots \}</annotation></semantics></math>, but either definition has all the necessary properties (namely, the properties making it a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a> in <a class="existingWikiWord" href="/nlab/show/Set">the category of sets</a>, when equipped with an appropriate successor operation). See, for instance, <a href="#WhatNumbersCouldNotBe">Benacerraf’s paper</a>.</p> <p>The structuralist says, essentially, that the number “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn></mrow><annotation encoding="application/x-tex">3</annotation></semantics></math>” should denote “the third place in a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a>” rather than some particular set such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>∅</mi><mo>,</mo><mo stretchy="false">{</mo><mi>∅</mi><mo stretchy="false">}</mo><mo>,</mo><mo stretchy="false">{</mo><mi>∅</mi><mo>,</mo><mo stretchy="false">{</mo><mi>∅</mi><mo stretchy="false">}</mo><mo stretchy="false">}</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{\emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}\}</annotation></semantics></math> as it does in any definition of “the set of natural numbers” in ZF.</p> <p><em>Structural set theory</em> provides a <a class="existingWikiWord" href="/nlab/show/foundation+of+mathematics">foundation of mathematics</a> which is free of this “superfluous baggage” attendant on theories such as ZF, in which there is lots of information such as whether or not <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn><mo>∈</mo><mn>17</mn></mrow><annotation encoding="application/x-tex">3\in 17</annotation></semantics></math> (yes, says von Neumann; no, says Zermelo) which is never used in mathematics. In a structural set theory, the elements (such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn></mrow><annotation encoding="application/x-tex">3</annotation></semantics></math>) of a set (such as <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>) <em>have</em> no identity apart from their existence as elements of that set, and whatever structure is given to that set by the functions and relations placed upon it. That is, sets (together with other attendant concepts such as <a class="existingWikiWord" href="/nlab/show/elements">elements</a>, <a class="existingWikiWord" href="/nlab/show/functions">functions</a>, and <a class="existingWikiWord" href="/nlab/show/relations">relations</a>) are the “raw material” from which mathematical structures are built. By contrast, theories such as ZF may be called <a class="existingWikiWord" href="/nlab/show/material+set+theories">material set theories</a> or <em>membership-based set theories</em>.</p> <p>Thus, somewhat paradoxically, it turns out that one of the primary attributes of a structural set theory is that the <em>elements</em> of a set have <em>no</em> “internal” structure; they are only given structure by means of functions and relations. In particular, they are not themselves sets, and by default cannot be elements of any other set (not in the sense that it is false that they are, but in the sense that it is meaningless to ask whether they are), so that elements of different sets cannot be compared (unless and until extra structure is imposed). Structural set theory thus looks very much like <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>. We contrast it with <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theories</a> such as ZF, in which the elements of sets can have internal structure, and are often (perhaps always) themselves sets.</p> <p>Structural set theories can be distinguished by whether they include a formal notion of <a class="existingWikiWord" href="/nlab/show/family">family</a> of <a class="existingWikiWord" href="/nlab/show/sets">sets</a>. Those that do are known as <a class="existingWikiWord" href="/nlab/show/first-order+set+theory">first-order set theories</a>, while those that do not are known as <span class="newWikiWord">zeroth-order set theories<a href="/nlab/new/zeroth-order+set+theory">?</a></span>. <span class="newWikiWord">Higher-order set theories<a href="/nlab/new/higher-order+set+theory">?</a></span> have a notion of families of families in addition to families of sets. This parallels <a class="existingWikiWord" href="/nlab/show/logic">logic</a>, where the role of <a class="existingWikiWord" href="/nlab/show/proposition">propositions</a> is played by sets and the role of <a class="existingWikiWord" href="/nlab/show/predicate">predicates</a> is played by families. Many structural set theories are only zeroth-order set theories, but the hSets and functions from hSets to the type hSet in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> form a higher-order set theory.</p> <p>It is hard to say precisely what makes a set theory “structural”, but one attempt is the notion of a <a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a>.</p> <h2 id="Examples">Examples</h2> <h3 id="ETCS">Elementary theory of the category of sets (ETCS)</h3> <p>The original, and most commonly cited, categorially presented structural set theory is the <em><a class="existingWikiWord" href="/nlab/show/elementary+theory+of+the+category+of+sets">elementary theory of the category of sets</a></em>, or <em><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a></em> for short (<a href="#Lawvere65">Lawvere 65</a>).</p> <p>Therefore structural set theory is also called <strong>categorial set theory</strong>.</p> <p><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> axiomatizes the <a class="existingWikiWord" href="/nlab/show/category">category</a> <a class="existingWikiWord" href="/nlab/show/Set">Set</a> of <a class="existingWikiWord" href="/nlab/show/sets">sets</a> as a <a class="existingWikiWord" href="/nlab/show/well-pointed+topos">well-pointed topos</a> and thus lends itself to <a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a> in <a class="existingWikiWord" href="/nlab/show/topos+theory">topos theory</a>. As such this is similar to the <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a>-theory found in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> (<a href="#InHomotopyTypeTheory">below</a>), which forms a <a class="existingWikiWord" href="/nlab/show/%CE%A0W-pretopos">ΠW-pretopos</a>.</p> <p><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> is weaker than <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a>. To handle some esoteric parts of modern mathematics such as Borel determinacy, it must be supplemented with an <a class="existingWikiWord" href="/nlab/show/axiom+of+collection">axiom of collection</a>, although it suffices for most everyday uses.</p> <p><a href="#McLarty93">McLarty 93</a> argues that ETCS resolves the issues originally raised by <a href="#Benacerraf65">Benacerraf 65</a>.</p> <h3 id="sets_elements_and_relations_sear">Sets, Elements and Relations (SEAR)</h3> <p>Another structural set theory, which is stronger than ETCS (since it includes the axiom of collection by default) and also less closely tied to category theory, is <a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a>.</p> <h3 id="structural_zfc">Structural ZFC</h3> <p>One could reformulate <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> as a three-sorted or dependently sorted <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> consisting of <a class="existingWikiWord" href="/nlab/show/sets">sets</a>, <a class="existingWikiWord" href="/nlab/show/elements">elements</a>, <a class="existingWikiWord" href="/nlab/show/functions">functions</a>, and structural versions of the 10 standard <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> axioms. This set theory is called <a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a>.</p> <p>It should also be possible to create an <a class="existingWikiWord" href="/nlab/show/allegory">allegorical</a> version of ZFC, but nobody has done so yet.</p> <h3 id="local_set_theory">Local set theory</h3> <p>Local set theory avoids the use of any global universe but instead is formulated in a many-sorted language that has various forms of sorts including, for each sort a power-sort; see <a href="#Bell">Bell</a> and <a href="#Aczel">Aczel</a>.</p> <h3 id="setoids">Setoids</h3> <p>Set theory set up in <a class="existingWikiWord" href="/nlab/show/extensional+type+theory">extensional</a> <a class="existingWikiWord" href="/nlab/show/intuitionistic+type+theory">intuitionistic type theory</a> via <a class="existingWikiWord" href="/nlab/show/setoids">setoids</a> is structural.</p> <h3 id="InHomotopyTypeTheory">Homotopy-sets in homotopy type theory</h3> <p>The collection of <a class="existingWikiWord" href="/nlab/show/h-sets">h-sets</a> in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> constitute a <a class="existingWikiWord" href="/nlab/show/%CE%A0W-pretopos">ΠW-pretopos</a>, hence a structural set theory (<a href="#RijkeSpitter13">Rijke-Spitters 13</a>). If the type theory also has a <a class="existingWikiWord" href="/nlab/show/type+of+all+propositions">type of all propositions</a>, then the collections of <a class="existingWikiWord" href="/nlab/show/h-sets">h-sets</a> constitute an <a class="existingWikiWord" href="/nlab/show/elementary+topos">elementary topos</a>.</p> <h2 id="related_pages">Related Pages</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material+versus+structural+set+theory">material versus structural set theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material-structural+adjunction">material-structural adjunction</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/categorical+set+theory">categorical set theory</a>, <a class="existingWikiWord" href="/nlab/show/allegorical+set+theory">allegorical set theory</a></p> </li> </ul> <h2 id="references">References</h2> <p>A textbook that introduces the <a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a> informally via structural set theory is</p> <ul> <li id="LawvereRosebrugh03"><a class="existingWikiWord" href="/nlab/show/William+Lawvere">William Lawvere</a>, <a class="existingWikiWord" href="/nlab/show/Robert+Rosebrugh">Robert Rosebrugh</a>, <em><a class="existingWikiWord" href="/nlab/show/Sets+for+Mathematics">Sets for Mathematics</a></em>, Cambridge UP 2003.</li> </ul> <p>The formal account of <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> originates with</p> <ul> <li id="Lawvere65"><a class="existingWikiWord" href="/nlab/show/William+Lawvere">William Lawvere</a>, <em>An elementary theory of the category of sets</em>, Proceedings of the National Academy of Science of the U.S.A <strong>52</strong> pp.1506-1511 (1965). (<a href="http://www.ncbi.nlm.nih.gov/pmc/articles/PMC300477/pdf/pnas00186-0196.pdf">pdf</a>)</li> </ul> <p>Structural set theory found in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> is discussed in</p> <ul> <li id="RijkeSpitters13"><a class="existingWikiWord" href="/nlab/show/Egbert+Rijke">Egbert Rijke</a>, <a class="existingWikiWord" href="/nlab/show/Bas+Spitters">Bas Spitters</a>, <em>Sets in homotopy type theory</em>, Mathematical Structures in Computer Science, Volume 25, Issue 5 (From type theory and homotopy theory to Univalent Foundations of Mathematics) (<a href="http://arxiv.org/abs/1305.3835">arXiv:1305.3835</a>)</li> </ul> <p>which became one chapter in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Univalent+Foundations+Project">Univalent Foundations Project</a>, <em><a class="existingWikiWord" href="/nlab/show/Homotopy+Type+Theory+%E2%80%93+Univalent+Foundations+of+Mathematics">Homotopy Type Theory – Univalent Foundations of Mathematics</a></em></li> </ul> <p>Relation to <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> is discussed in</p> <ul> <li id="Shulman18"><a class="existingWikiWord" href="/nlab/show/Michael+Shulman">Michael Shulman</a>, <em>Comparing material and structural set theories</em> (<a href="https://arxiv.org/abs/1808.05204">arXiv:1808.05204</a>)</li> </ul> <p>See also</p> <ul> <li id="Benacerraf65"> <p>P. Benacerraf, <em>What numbers could not be</em>, The Philosophical Review Vol. 74, No. 1, Jan., 1965</p> </li> <li id="McLarty93"> <p><a class="existingWikiWord" href="/nlab/show/Colin+McLarty">Colin McLarty</a>, <em>Numbers can be just what they have to</em>, Noûs, Vol 27, No. 4, 1993.</p> </li> <li> <p>John Bell, <em>Notes on toposes and local set theories</em> <a href="http://publish.uwo.ca/~jbell/topnotes.pdf">PDF</a></p> </li> <li> <p>Peter Aczel, <em>Local Constructive Set Theory and Inductive Definitions</em>, <a href="http://www.cs.man.ac.uk/~petera/sommaruga-book-paper.pdf">PDF</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Mike+Shulman">Mike Shulman</a>, <em>Syntax, Semantics, and Structuralism II</em> <a href="https://golem.ph.utexas.edu/category/2009/12/syntax_semantics_and_structura_1.html">blog</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tom+Leinster">Tom Leinster</a>, <em>Rethinking set theory</em> <a href="https://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html">blog</a>, <a href="http://arxiv.org/abs/1212.6543">arXiv</a></p> </li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on July 5, 2024 at 13:07:52. See the <a href="/nlab/history/structural+set+theory" 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/structural+set+theory" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/111/#Item_34">Discuss</a><span class="backintime"><a href="/nlab/revision/structural+set+theory/37" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/structural+set+theory" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/structural+set+theory" accesskey="S" class="navlink" id="history" rel="nofollow">History (37 revisions)</a> <a href="/nlab/show/structural+set+theory/cite" style="color: black">Cite</a> <a href="/nlab/print/structural+set+theory" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/structural+set+theory" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>