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> SEAR 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> SEAR </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/13686/#Item_8" 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>SEAR</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="sear">SEAR</h1> <div class='maruku_toc'> <ul> <li><a href='#introduction'>Introduction</a></li> <li><a href='#description_of_sear'>Description of SEAR</a></li> <ul> <li><a href='#types'>Types</a></li> <li><a href='#basic_axioms'>Basic axioms</a></li> <li><a href='#consequences_of_the_basic_axioms'>Consequences of the basic axioms</a></li> <li><a href='#power_sets_and_colimits'>Power sets and colimits</a></li> <li><a href='#infinity'>Infinity</a></li> <li><a href='#collection'>Collection</a></li> <ul> <li><a href='#the_ghost_of_a_universal_set'>The ghost of a universal set</a></li> <li><a href='#applications_of_collection'>Applications of collection</a></li> </ul> </ul> <li><a href='#variants_and_comparisons'>Variants and Comparisons</a></li> <ul> <li><a href='#the_axiom_of_choice'>The Axiom of Choice</a></li> <li><a href='#constructive_sear'>Constructive SEAR</a></li> <li><a href='#bounded_sear_and_etcs'>Bounded SEAR and ETCS</a></li> <li><a href='#sear_and_zf'>SEAR and ZF</a></li> <ul> <li><a href='#from_zf_to_sear'>From ZF to SEAR</a></li> <li><a href='#from_sear_to_zf'>From SEAR to ZF</a></li> </ul> <li><a href='#type_theory_and_internalization'>Type theory and internalization</a></li> </ul> <li><a href='#making_alternate_primitive_choices'>Making alternate primitive choices</a></li> <ul> <li><a href='#threesorted_sear'>Three-sorted SEAR</a></li> <li><a href='#SEPS'>SEPS: Using pairs and subsets instead of relations</a></li> <li><a href='#sepf_using_pairs_and_functions_instead_of_relations'>SEPF: Using pairs and functions instead of relations</a></li> <li><a href='#eqfree'>Eliminating equality</a></li> </ul> <li><a href='#related_pages_and_spinoffs'>Related pages and spinoffs</a></li> </ul> </div> <h2 id="introduction">Introduction</h2> <p><strong>SEAR</strong>, short for <strong>Sets, Elements, And Relations</strong>, is a <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> with the following properties:</p> <ul> <li>It is equivalent in strength to the <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <a class="existingWikiWord" href="/nlab/show/ZF">ZF</a>. (It can be augmented by an <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> to produce <em>SEARC</em>, which is strongly equivalent to <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a>.)</li> <li>It contains a subtheory called <strong>bounded SEAR</strong> which (when augmented by choice) is strongly equivalent to <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>. Conversely, ETCS can be augmented by a replacement axiom to become equivalent to SEARC.</li> </ul> <p>Being a structural set theory, SEAR differs from ZF in the following ways (which are also ways in which it is similar to ETCS):</p> <ul> <li>There is a type distinction between <em>sets</em> and <em>elements</em>; a set is never an element of another set. Every element is an element <em>of some set</em>.</li> <li>The elements of a set have no “internal structure;” they are merely featureless points.</li> <li>The “elementhood” relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> only makes sense when <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> is known to be an element of some ambient set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is known to be a subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>.</li> </ul> <p>A good description of the difference between material and structural set theory can be found at <a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">Trimble on ETCS I</a>. However, ZFC and ETCS also differ along another axis than the material-structural. At <a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">Trimble on ETCS III</a> the following metaphor is proposed for this dimension:</p> <blockquote> <p>with ZFC it’s more as if you can just hop in the car and go; with ETCS you build the car engine from smaller parts with your bare hands, but in the process you become an expert mechanic, and are not so rigidly attached to a particular make and model.</p> </blockquote> <p>Using this metaphor, SEAR can be thought of as an ETCS-car which comes preassembled with a nice slick control panel. Or, using an alternate metaphor, ZFC is like Windows, ETCS is like UNIX, and SEAR is like OS X (or maybe Ubuntu). With SEAR you get a nice familiar interface with which it is easy to do standard things, there is less cruft than you get with ZFC, and behind the scenes you have all the power of ETCS (and more). (Of course, if you like Microsoft products, then this metaphor probably does not appeal to you.)</p> <p>Note that experts will probably always prefer to build their own car/OS; the goal of SEAR is to make structural set theory accessible to a wider audience. In particular, SEAR is intended to demonstrate the complete independence of <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> from <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>. Thus, apart from being (by default) stronger than ETCS, SEAR differs from it in the following ways:</p> <ul> <li>It includes the notion of an <em>element</em> of a set as a primitive concept, rather than defining it as a particular sort of function.</li> <li>It does <em>not</em> include the notion of a <a class="existingWikiWord" href="/nlab/show/function">function</a> as a primitive concept (instead it includes the notion of a <a class="existingWikiWord" href="/nlab/show/binary+relation">binary relation</a>, with functions defined via their <a class="existingWikiWord" href="/nlab/show/graph+of+a+function">graphs</a> in a familiar way).</li> <li>It does not include the notions of composition or identities (of either functions or relations) as primitive concepts. In particular, it does not require the user to know what a <a class="existingWikiWord" href="/nlab/show/category">category</a> is, even implicitly.</li> <li>As a corollary, its axioms do not require knowledge of categorical concepts such as <a class="existingWikiWord" href="/nlab/show/limits">limits</a> and <a class="existingWikiWord" href="/nlab/show/natural+numbers+objects">natural numbers objects</a> (although these concepts can be very naturally introduced while learning SEAR).</li> <li>The property of <a class="existingWikiWord" href="/nlab/show/axiom+of+separation">separation</a> (one of the most important facts in the everyday use of set theory) is a direct consequence of the axioms of SEAR. Compare how in ETCS, the property of bounded separation follows from the theorem that a <a class="existingWikiWord" href="/nlab/show/topos">topos</a> is a <a class="existingWikiWord" href="/nlab/show/Heyting+category">Heyting category</a>, which requires <a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">substantial work</a>.</li> </ul> <h2 id="description_of_sear">Description of SEAR</h2> <h3 id="types">Types</h3> <p>SEAR is a theory about three kinds of things: <strong>sets</strong>, <strong>elements</strong>, and <strong>relations</strong>. Every element, and every variable that ranges over elements, is always associated to something denoting a set (which might be a constant or a variable); we say it is an element <strong>of</strong> that set. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> is an element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> we write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>; note that this is not an <em>assertion</em> which may be true or false, but a <em>typing</em> declaration. In formal terms, this means that SEAR is a <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependently typed</a> theory, with a type of sets, a type of elements for each set term, and a type of relations for each pair of set terms.</p> <p>One consequence of this is that whenever we <a class="existingWikiWord" href="/nlab/show/quantification">quantify</a> over elements we must always quantify over elements <em>of some set</em>; thus we can say “for all elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>” but not “for all elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>.” Another consequence is that the assertion <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x=y</annotation></semantics></math> is only well-formed (a precondition to its being true <em>or</em> false) if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> are elements of the same set.</p> <p>In a similar manner, every relation is always associated to an ordered pair of sets, the first called its <strong><a class="existingWikiWord" href="/nlab/show/source">source</a></strong> and the second its <strong><a class="existingWikiWord" href="/nlab/show/target">target</a></strong> (thus the fundamental relations in SEAR are binary relations). If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math> is a relation from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> we write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright B</annotation></semantics></math>. As with elements, the assertion <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>=</mo><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\varphi=\psi</annotation></semantics></math> is only well-formed if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\psi</annotation></semantics></math> have the same source and the same target.</p> <p>Implicit in the existence of three types of things is that nothing is both a set and an element, etc., so in particular a statement such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x=A</annotation></semantics></math> is not well-formed if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> is an element and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> a set. Furthermore, SEAR does not include an equality relation between sets: even if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> are both sets we do not consider <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>=</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A=B</annotation></semantics></math> to be well-formed. (Thus SEAR respects the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a>.)</p> <p>The final piece of data that we have is a notion of when a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright B</annotation></semantics></math> <strong>holds</strong> of a pair of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math>. We write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)</annotation></semantics></math> when <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math> holds of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math>.</p> <h3 id="basic_axioms">Basic axioms</h3> <p>Now we can state the axioms of SEAR, beginning with the most basic ones.</p> <p><strong>Axiom 0 (Nontriviality):</strong> <em>There exists a set which contains an element.</em></p> <p><strong>Axiom 1 (Relational comprehension):</strong> <em>For any two sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, and any property <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> that can obtain of an element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and an element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, there exists a unique relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright B</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)</annotation></semantics></math> if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> obtains of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math>.</em></p> <p>Here “property” is interpreted formally as “first-order formula”, which makes the axiom (like later the axiom of collection) in fact an axiom scheme.</p> <p>Axiom 1 basically says that relations are what we expect them to be intuitively. It should remind the reader of the <a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a>. The two important differences are (1) the presence of two sets and two variables, rather than one, and (2) the fact that what is produced is not a <em>set</em>, but a <em>relation</em> (a different kind of thing). The to-be-introduced Axiom 2 will enable us to make relations into (sub)sets, but first we need some terminology.</p> <div class="num_defn" id="function"> <h6 id="definition">Definition</h6> <p>A relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright B</annotation></semantics></math> is called a <strong><a class="existingWikiWord" href="/nlab/show/function">function</a></strong> from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> if for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>, there exists exactly one <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)</annotation></semantics></math>.</p> </div> <p>We write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A\to B</annotation></semantics></math> for such a function, and for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> we write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(x)</annotation></semantics></math> for the resulting unique <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math>. Note that the uniqueness clause in Axiom 1 implies that functions are extensional: if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>,</mo><mi>g</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f,g:A\to B</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>g</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(x)=g(x)</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>=</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">f=g</annotation></semantics></math>.</p> <p><strong>Axiom 2 (Tabulations):</strong> <em>For any relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright B</annotation></semantics></math>, there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|\varphi|</annotation></semantics></math> and functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">p:{|\varphi|}\to A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo>:</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">q:{|\varphi|}\to B</annotation></semantics></math> such that: (1) for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)</annotation></semantics></math> if and only if there exists <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>∈</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">r\in {|\varphi|}</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo stretchy="false">(</mo><mi>r</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">p(r)=x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo stretchy="false">(</mo><mi>r</mi><mo stretchy="false">)</mo><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">q(r)=y</annotation></semantics></math>, and (2) for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>∈</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">r\in {|\varphi|}</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>∈</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">s\in{|\varphi|}</annotation></semantics></math>, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo stretchy="false">(</mo><mi>r</mi><mo stretchy="false">)</mo><mo>=</mo><mi>p</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p(r)=p(s)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo stretchy="false">(</mo><mi>r</mi><mo stretchy="false">)</mo><mo>=</mo><mi>q</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">q(r)=q(s)</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>=</mo><mi>s</mi></mrow><annotation encoding="application/x-tex">r=s</annotation></semantics></math>.</em></p> <p>A set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|\varphi|</annotation></semantics></math> equipped with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi></mrow><annotation encoding="application/x-tex">q</annotation></semantics></math> as in Axiom 2 is called a <strong>tabulation</strong> of the relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math>. We think of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|\varphi|</annotation></semantics></math> as “the set of pairs <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(x,y)</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)</annotation></semantics></math> holds,” with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi></mrow><annotation encoding="application/x-tex">q</annotation></semantics></math> projecting <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(x,y)</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math>, respectively. Note that by Axiom 1, any set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> equipped with functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mi>R</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">p:R\to A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo>:</mo><mi>R</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">q:R\to B</annotation></semantics></math> satisfying (2) determines a unique relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright B</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)</annotation></semantics></math> holds iff there is an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>∈</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">r\in R</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo stretchy="false">(</mo><mi>r</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">p(r)=x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo stretchy="false">(</mo><mi>r</mi><mo stretchy="false">)</mo><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">q(r)=y</annotation></semantics></math>; then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> is a tabulation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math>.</p> <h3 id="consequences_of_the_basic_axioms">Consequences of the basic axioms</h3> <p>Axioms 0, 1, and 2 alone are very powerful! Here are some things we can do with them.</p> <div class="num_theorem" id="emptyset"> <h6 id="theorem">Theorem</h6> <p>There exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi></mrow><annotation encoding="application/x-tex">\emptyset</annotation></semantics></math> which has no elements.</p> </div> <div class="proof"> <h6 id="proof">Proof</h6> <p>By Axiom 0, there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>. By Axiom 1, there exists a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright A</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)</annotation></semantics></math> holds <em>never</em>. Using Axiom 2, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi></mrow><annotation encoding="application/x-tex">\emptyset</annotation></semantics></math> be a tabulation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math>.</p> </div> <p>From now on we fix a particular set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi></mrow><annotation encoding="application/x-tex">\emptyset</annotation></semantics></math> having no elements. By Axiom 1, for any set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> there is exactly one relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi><mo>↬</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\emptyset\looparrowright A</annotation></semantics></math> and exactly one relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>↬</mo><mi>∅</mi></mrow><annotation encoding="application/x-tex">A\looparrowright\emptyset</annotation></semantics></math>.</p> <div class="num_theorem" id="terminalset"> <h6 id="theorem_2">Theorem</h6> <p>There exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> which has exactly one element.</p> </div> <div class="proof"> <h6 id="proof_2">Proof</h6> <p>By Axiom 0, there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> containing an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>. By Axiom 1, there exists a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright A</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(y,z)</annotation></semantics></math> holds iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">y=x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">z=x</annotation></semantics></math>. Using Axiom 2, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> be a tabulation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math>.</p> </div> <p>From now on we fix a particular set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> having exactly one element; we usually denote this element by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⋆</mo></mrow><annotation encoding="application/x-tex">\star</annotation></semantics></math>. By Axiom 1, for every set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> there exists a unique function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">f:A\to 1</annotation></semantics></math>, defined by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mo>⋆</mo></mrow><annotation encoding="application/x-tex">f(x)=\star</annotation></semantics></math> for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>. Likewise, to every function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>:</mo><mn>1</mn><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">g:1\to A</annotation></semantics></math> there corresponds a unique element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>, by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo stretchy="false">(</mo><mo>⋆</mo><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">g(\star)=x</annotation></semantics></math>.</p> <p>We define a <strong>subset</strong> of a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> to be a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo>:</mo><mn>1</mn><mo>↬</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">S:1\looparrowright A</annotation></semantics></math>. By Axiom 1, a subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is determined by precisely those <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo stretchy="false">(</mo><mo>⋆</mo><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">S(\star,x)</annotation></semantics></math>. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo stretchy="false">(</mo><mo>⋆</mo><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">S(\star,x)</annotation></semantics></math> we write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">x\in S</annotation></semantics></math>. Note that this is an <em>overloading</em> of the notation <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>; it can be distinguished from the previous usage because here <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is a relation, not a set. Note also that the previous usage <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> was a typing declaration (it says what kind of thing <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> is when we introduce it), whereas <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">x\in S</annotation></semantics></math> is a statement which can be either true or false.</p> <p>Now Axiom 2 implies that from any subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> we can construct a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|S|</annotation></semantics></math> with a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">i:{|S|}\to A</annotation></semantics></math> such that (1) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">x\in S</annotation></semantics></math> iff there is an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>′</mo><mo>∈</mo><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">x'\in {|S|}</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">i(x')=x</annotation></semantics></math>, and (2) for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>′</mo><mo>,</mo><mi>x</mi><mo>″</mo><mo>∈</mo><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">x',x''\in {|S|}</annotation></semantics></math>, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo><mo>=</mo><mi>i</mi><mo stretchy="false">(</mo><mi>x</mi><mo>″</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">i(x')=i(x'')</annotation></semantics></math> then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>′</mo><mo>=</mo><mi>x</mi><mo>″</mo></mrow><annotation encoding="application/x-tex">x'=x''</annotation></semantics></math>. A function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi></mrow><annotation encoding="application/x-tex">i</annotation></semantics></math> with property (2) is called <strong>injective</strong>; in this way we set up a correspondence between subsets and injective functions. (Likewise, a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A\to B</annotation></semantics></math> is <strong>surjective</strong> if for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math> there is an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">f(x)=y</annotation></semantics></math>.) Combined with Axiom 1, this implies the following <em>separation property</em>.</p> <div class="num_theorem" id="sep"> <h6 id="theorem_3">Theorem</h6> <p>For any property <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> of elements of a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> and an injective function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">i:B\to A</annotation></semantics></math> such that for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a\in A</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(a)</annotation></semantics></math> iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>=</mo><mi>i</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">a=i(b)</annotation></semantics></math> for some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">b\in B</annotation></semantics></math>.</p> </div> <p>Although the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|S|</annotation></semantics></math> is not determined uniquely by the subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>, it is determined up to <a class="existingWikiWord" href="/nlab/show/bijection">bijection</a>. We define an <strong>bijection</strong> to be a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\psi:A\looparrowright B</annotation></semantics></math> such that for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> there is a unique <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\psi(x,y)</annotation></semantics></math>, and for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math> there is a unique <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\psi(x,y)</annotation></semantics></math>. Clearly any bijection is a function, as is its opposite (defined by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>ψ</mi> <mi>o</mi></msup><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⇔</mo><mi>ψ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\psi^o(y,x) \Leftrightarrow \psi(x,y)</annotation></semantics></math>), and these two properties characterize bijections. It is also easy to see that a function is a bijection iff it is both injective and surjective.</p> <p>For example, it is easy to see that if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> both have no elements, there is a unique bijection between them; thus an empty set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi></mrow><annotation encoding="application/x-tex">\emptyset</annotation></semantics></math> is determined up to unique bijection. Likewise, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> both contain a unique element, then there is a unique bijection between them; thus a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> with one element is also determined up to unique bijection.</p> <div class="num_theorem" id="tabuniq"> <h6 id="theorem_4">Theorem</h6> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|\varphi|</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><mo>′</mo></mrow><annotation encoding="application/x-tex">{|\varphi|}'</annotation></semantics></math> are two tabulations of the same relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright B</annotation></semantics></math>, then there is a bijection between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|\varphi|</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><mo>′</mo></mrow><annotation encoding="application/x-tex">{|\varphi|}'</annotation></semantics></math>.</p> </div> <div class="proof"> <h6 id="proof_3">Proof</h6> <p>By Axiom 1, define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>:</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><mo>↬</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><mo>′</mo></mrow><annotation encoding="application/x-tex">B:{|\varphi|} \looparrowright {|\varphi|}'</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(x,y)</annotation></semantics></math> holds precisely when <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>p</mi><mo>′</mo><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p(x)=p'(y)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>q</mi><mo>′</mo><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">q(x)=q'(y)</annotation></semantics></math>. The properties of tabulations immediately imply that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> is a bijection.</p> </div> <div class="num_cor" id="sstabuniq"> <h6 id="corollary">Corollary</h6> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|S|</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow><mo>′</mo></mrow><annotation encoding="application/x-tex">{|S|}'</annotation></semantics></math> are two tabulations of the same subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo>⊆</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">S\subseteq A</annotation></semantics></math>, then there is a bijection between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|S|</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow><mo>′</mo></mrow><annotation encoding="application/x-tex">{|S|}'</annotation></semantics></math>.</p> </div> <p>The <strong>composite</strong> of two relations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright B</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mo>:</mo><mi>B</mi><mo>↬</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">\psi:B\looparrowright C</annotation></semantics></math> is defined to be the relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">\psi\varphi:A\looparrowright C</annotation></semantics></math> (also written <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mo>∘</mo><mi>φ</mi></mrow><annotation encoding="application/x-tex">\psi\circ\varphi</annotation></semantics></math>) such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\psi\varphi(x,z)</annotation></semantics></math> holds of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>∈</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">z\in C</annotation></semantics></math> iff there is a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\psi(y,z)</annotation></semantics></math>. The <strong>identity</strong> relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>id</mi> <mi>A</mi></msub><mo>:</mo><mi>A</mi><mo>↬</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">id_A:A\looparrowright A</annotation></semantics></math> is defined by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>⇔</mo><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">id_A(x,y) \Leftrightarrow x=y</annotation></semantics></math>.</p> <div class="num_theorem" id="category"> <h6 id="theorem_5">Theorem</h6> <p>Composition of relations is associative (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>χ</mi><mo stretchy="false">(</mo><mi>ψ</mi><mi>φ</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><mi>χ</mi><mi>ψ</mi><mo stretchy="false">)</mo><mi>φ</mi></mrow><annotation encoding="application/x-tex">\chi(\psi\varphi)=(\chi\psi)\varphi</annotation></semantics></math>), and identity relations are identities for composition (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo lspace="0em" rspace="thinmathspace">id</mo> <mi>B</mi></msub><mo>∘</mo><mi>φ</mi><mo>=</mo><mi>φ</mi><mo>=</mo><mi>φ</mi><mo>∘</mo><msub><mo lspace="0em" rspace="thinmathspace">id</mo> <mi>A</mi></msub></mrow><annotation encoding="application/x-tex">\id_B\circ \varphi = \varphi = \varphi\circ\id_A</annotation></semantics></math>). The composite of functions is a function, and the identity relation is a function. The composite of bijections is a bijection, and a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright B</annotation></semantics></math> is a bijection iff there is a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mo>:</mo><mi>B</mi><mo>↬</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\psi:B\looparrowright A</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mi>φ</mi><mo>=</mo><msub><mi>id</mi> <mi>A</mi></msub></mrow><annotation encoding="application/x-tex">\psi\varphi = id_A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mi>ψ</mi><mo>=</mo><msub><mi>id</mi> <mi>B</mi></msub></mrow><annotation encoding="application/x-tex">\varphi\psi=id_B</annotation></semantics></math>.</p> </div> <div class="proof"> <h6 id="proof_4">Proof</h6> <p>Just as in naive set theory.</p> </div> <p>Informally speaking, we have two <a class="existingWikiWord" href="/nlab/show/categories">categories</a> whose objects are the sets: in <a class="existingWikiWord" href="/nlab/show/Rel">Rel</a> the morphisms are the relations, while in <a class="existingWikiWord" href="/nlab/show/Set">Set</a> the morphisms are the functions. Formally, all we can say is that these are “meta-categories,” in the sense that from any model of the first-order axioms of SEAR we can construct them as models of the first-order axioms of a category. (This is not that different from the status of large categories such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> in material set theories such as ZF. We could also speak about “proper classes” as is done in ZF using first-order formulas.) See also the section on Universes, below.</p> <p>In both of these (meta-)categories, the <a class="existingWikiWord" href="/nlab/show/isomorphisms">isomorphisms</a> are the bijections. We have also already observed that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi></mrow><annotation encoding="application/x-tex">\emptyset</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> are an <a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a> and a <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>, respectively, and that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi></mrow><annotation encoding="application/x-tex">\emptyset</annotation></semantics></math> is both initial and terminal in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Rel</mi></mrow><annotation encoding="application/x-tex">Rel</annotation></semantics></math>.</p> <p>For sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\top:A\looparrowright B</annotation></semantics></math> denote the relation such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\top(x,y)</annotation></semantics></math> holds always. A tabulation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo></mrow><annotation encoding="application/x-tex">\top</annotation></semantics></math> is denoted <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\times B</annotation></semantics></math>; it is a set equipped with functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mi>A</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">p:A\times B \to A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo>:</mo><mi>A</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">q:A\times B\to B</annotation></semantics></math> such that for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math>, there exists a unique <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>∈</mo><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">z\in A\times B</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">p(z)=x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">q(z)=y</annotation></semantics></math>. It is called the <strong><a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a></strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>.</p> <div class="num_theorem" id="product"> <h6 id="theorem_6">Theorem</h6> <p>For any sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\times B</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/product">product</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> in the category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>.</p> </div> <div class="proof"> <h6 id="proof_5">Proof</h6> <p>Just as in naive set theory.</p> </div> <p>In particular, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> has products.</p> <div class="num_theorem" id="lex"> <h6 id="theorem_7">Theorem</h6> <p>The category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> has finite limits.</p> </div> <div class="proof"> <h6 id="proof_6">Proof</h6> <p>It remains to construct the <a class="existingWikiWord" href="/nlab/show/equalizer">equalizer</a> of two functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>,</mo><mi>g</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f,g:A\to B</annotation></semantics></math>. Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> be the subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> so that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">x\in S</annotation></semantics></math> just when <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>g</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(x)=g(x)</annotation></semantics></math>; then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">{|S|}\to A</annotation></semantics></math> is easily shown to be an equalizer of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi></mrow><annotation encoding="application/x-tex">g</annotation></semantics></math>.</p> </div> <div class="num_theorem" id="imfact"> <h6 id="theorem_8">Theorem</h6> <p>For any function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A\to B</annotation></semantics></math> we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>=</mo><mi>m</mi><mi>e</mi></mrow><annotation encoding="application/x-tex">f = m e</annotation></semantics></math>, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>im</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>↪</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">m:im(f)\hookrightarrow B</annotation></semantics></math> is an injection and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo>:</mo><mi>A</mi><mo>↠</mo><mi>im</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">e:A\twoheadrightarrow im(f)</annotation></semantics></math> is a surjection. A set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>im</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">im(f)</annotation></semantics></math> equipped with such <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi></mrow><annotation encoding="application/x-tex">m</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi></mrow><annotation encoding="application/x-tex">e</annotation></semantics></math> is unique up to bijection and is called the <strong>image</strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>.</p> </div> <div class="proof"> <h6 id="proof_7">Proof</h6> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>im</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">im(f)</annotation></semantics></math> be <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|S|</annotation></semantics></math> where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is defined by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">y\in S</annotation></semantics></math> iff there exists an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">f(x)=y</annotation></semantics></math>. By definition, we have an injection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>im</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>↪</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">m:im(f)\hookrightarrow B</annotation></semantics></math>. And for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>, clearly <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">f(x)\in S</annotation></semantics></math>, so there is a unique <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>im</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">y\in im(f)</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">m(y)=f(x)</annotation></semantics></math>; we define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">e(x)=y</annotation></semantics></math>. It is easy to verify the rest.</p> </div> <p>Similarly, we can define the union and intersection of subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> in the usual way: we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi><mo>∪</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">x\in S\cup T</annotation></semantics></math> iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">x\in S</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">x\in T</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi><mo>∩</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">x\in S\cap T</annotation></semantics></math> iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">x\in S</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">x\in T</annotation></semantics></math>.</p> <div class="num_theorem" id="heyting"> <h6 id="theorem_9">Theorem</h6> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/well-pointed+category">well-pointed</a> <a class="existingWikiWord" href="/nlab/show/Heyting+category">Heyting category</a> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Rel</mi></mrow><annotation encoding="application/x-tex">Rel</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/division+allegory">division allegory</a>.</p> </div> <div class="proof"> <h6 id="proof_8">Proof</h6> <p>Left to the reader.</p> </div> <h3 id="power_sets_and_colimits">Power sets and colimits</h3> <p>In structural set theory, sets cannot contain other sets (or relations), so we cannot strictly speaking have “the set of subsets of a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>.” What we generally do instead is have a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">P A</annotation></semantics></math> each of whose elements is <em>associated to</em> a subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> in a bijective way. This association happens via a specified relation between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">P A</annotation></semantics></math>.</p> <p><strong>Axiom 3 (power sets):</strong> <em>For any set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">P A</annotation></semantics></math> and a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϵ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">\epsilon:A\looparrowright P A</annotation></semantics></math> such that for any subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a unique <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>∈</mo><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">s\in P A</annotation></semantics></math> with the property that for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">x\in S</annotation></semantics></math> iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϵ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>s</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\epsilon(x,s)</annotation></semantics></math>.</em></p> <p>As in both material set theory and ETCS, many useful consequences flow from this axiom. We first observe that the property of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">P A</annotation></semantics></math> stated for subsets actually implies an analogous property for all relations.</p> <div class="num_theorem" id="topos"> <h6 id="theorem_10">Theorem</h6> <p>For any relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo>:</mo><mi>B</mi><mo>↬</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">R:B\looparrowright A</annotation></semantics></math>, there exists a unique function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>R</mi></msub><mo>:</mo><mi>B</mi><mo>→</mo><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">f_R:B\to P A</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(y,x)</annotation></semantics></math> if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϵ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><msub><mi>f</mi> <mi>R</mi></msub><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\epsilon(x,f_R(y))</annotation></semantics></math>. It follows that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/topos">topos</a> (and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Rel</mi></mrow><annotation encoding="application/x-tex">Rel</annotation></semantics></math> is a power allegory).</p> </div> <div class="proof"> <h6 id="proof_9">Proof</h6> <p>We simply define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>R</mi></msub></mrow><annotation encoding="application/x-tex">f_R</annotation></semantics></math> elementwise; for each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> we define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>R</mi></msub><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_R(y)</annotation></semantics></math> to be the unique element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">P A</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϵ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><msub><mi>f</mi> <mi>R</mi></msub><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\epsilon(x,f_R(y))</annotation></semantics></math> holds iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(y,x)</annotation></semantics></math> holds. Extensionality of functions implies that it is unique.</p> </div> <p>As usual, power sets also imply the existence of function sets.</p> <div class="num_theorem" id="ccc"> <h6 id="theorem_11">Theorem</h6> <p>For any two sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>B</mi> <mi>A</mi></msup></mrow><annotation encoding="application/x-tex">B^A</annotation></semantics></math> and a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ev</mi><mo>:</mo><msup><mi>B</mi> <mi>A</mi></msup><mo>×</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">ev:B^A \times A\to B</annotation></semantics></math> such that for any function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A\to B</annotation></semantics></math> there exists a unique element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>s</mi> <mi>f</mi></msub><mo>∈</mo><msup><mi>B</mi> <mi>A</mi></msup></mrow><annotation encoding="application/x-tex">s_f\in B^A</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ev</mi><mo stretchy="false">(</mo><msub><mi>s</mi> <mi>f</mi></msub><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">ev(s_f,a)=f(a)</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a\in A</annotation></semantics></math>. It follows that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian closed category</a>.</p> </div> <div class="proof"> <h6 id="proof_10">Proof</h6> <p>We take <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>B</mi> <mi>A</mi></msup></mrow><annotation encoding="application/x-tex">B^A</annotation></semantics></math> to be a tabulation of the subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo>×</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(A\times B)</annotation></semantics></math> containing only the functions. More precisely, define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>⊆</mo><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo>×</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">F\subseteq P(A\times B)</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>∈</mo><mi>F</mi></mrow><annotation encoding="application/x-tex">s\in F</annotation></semantics></math> iff for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>, there exists a unique <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϵ</mi><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>,</mo><mi>s</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\epsilon((x,y),s)</annotation></semantics></math>, and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>B</mi> <mi>A</mi></msup><mo>=</mo><mrow><mo stretchy="false">|</mo><mi>F</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">B^A = {|F|}</annotation></semantics></math>.</p> </div> <p>The correspondences in Theorems <a class="maruku-ref" href="#topos"></a> and <a class="maruku-ref" href="#ccc"></a> are “meta-bijections,” but by a standard Yoneda lemma argument they can be converted into actual bijections as defined above in SEAR. This produces bijections such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>C</mi> <mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow></msup><mo>≅</mo><mo stretchy="false">(</mo><msup><mi>C</mi> <mi>A</mi></msup><msup><mo stretchy="false">)</mo> <mi>B</mi></msup></mrow><annotation encoding="application/x-tex">C^{A\times B} \cong (C^A)^B</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo>×</mo><mi>B</mi><mo stretchy="false">)</mo><mo>≅</mo><mo stretchy="false">(</mo><mi>P</mi><mi>A</mi><msup><mo stretchy="false">)</mo> <mi>B</mi></msup></mrow><annotation encoding="application/x-tex">P(A\times B) \cong (P A)^B</annotation></semantics></math>.</p> <p>We now construct <a class="existingWikiWord" href="/nlab/show/quotient+set">quotient set</a>s. Of course, by an <strong><a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></strong> on a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> we mean a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">R:A\looparrowright A</annotation></semantics></math> which is reflexive, transitive, and symmetric.</p> <div class="num_theorem" id="quotients"> <h6 id="theorem_12">Theorem</h6> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> is an equivalence relation on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, then there is a surjective function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo>:</mo><mi>A</mi><mo>↠</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">q:A\twoheadrightarrow B</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(x,y)</annotation></semantics></math> holds iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>q</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">q(x)=q(y)</annotation></semantics></math>.</p> </div> <div class="proof"> <h6 id="proof_11">Proof</h6> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> induces a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>R</mi></msub><mo>:</mo><mi>A</mi><mo>→</mo><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">f_R:A\to P A</annotation></semantics></math> as above; let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> be <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>im</mi><mo stretchy="false">(</mo><msub><mi>f</mi> <mi>R</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">im(f_R)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi></mrow><annotation encoding="application/x-tex">q</annotation></semantics></math> the surjective part of the image factorization. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(x,y)</annotation></semantics></math> holds, then by symmetry and transitivity, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mo>⇔</mo><mi>R</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(x,z)\Leftrightarrow R(y,z)</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi></mrow><annotation encoding="application/x-tex">z</annotation></semantics></math>; hence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>R</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><msub><mi>f</mi> <mi>R</mi></msub><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_R(x)=f_R(y)</annotation></semantics></math> and so <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>q</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">q(x)=q(y)</annotation></semantics></math>. Conversely, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>q</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">q(x)=q(y)</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>R</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><msub><mi>f</mi> <mi>R</mi></msub><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_R(x)=f_R(y)</annotation></semantics></math>; but <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><msub><mi>f</mi> <mi>R</mi></msub><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">y\in f_R(y)</annotation></semantics></math> by reflexivity, hence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><msub><mi>f</mi> <mi>R</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">y\in f_R(x)</annotation></semantics></math> and thus <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(x,y)</annotation></semantics></math> holds.</p> </div> <p>Such a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, which is easily seen to be unique up to bijection, is called a <strong>quotient</strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> and often written <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo stretchy="false">/</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">A/R</annotation></semantics></math>.</p> <p>Likewise, given sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⊔</mo><mi>B</mi><mo>=</mo><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">A\sqcup B={|S|}</annotation></semantics></math>, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is the subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>A</mi><mo>×</mo><mi>P</mi><mi>B</mi></mrow><annotation encoding="application/x-tex">P A \times P B</annotation></semantics></math> consisting of the pairs <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo stretchy="false">{</mo><mi>x</mi><mo stretchy="false">}</mo><mo>,</mo><mo stretchy="false">{</mo><mo stretchy="false">}</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\{x\},\{\})</annotation></semantics></math> for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo stretchy="false">{</mo><mo stretchy="false">}</mo><mo>,</mo><mo stretchy="false">{</mo><mi>y</mi><mo stretchy="false">}</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\{\},\{y\})</annotation></semantics></math> for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math>. (Of course, here we are identifying elements of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>A</mi><mo>×</mo><mi>P</mi><mi>B</mi></mrow><annotation encoding="application/x-tex">P A \times P B</annotation></semantics></math> with ordered pairs of subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> via the projections of the product and the defining relations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>ϵ</mi> <mi>A</mi></msub></mrow><annotation encoding="application/x-tex">\epsilon_A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>ϵ</mi> <mi>B</mi></msub></mrow><annotation encoding="application/x-tex">\epsilon_B</annotation></semantics></math>.) We have evident injections <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>→</mo><mi>A</mi><mo>⊔</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\to A\sqcup B</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>→</mo><mi>A</mi><mo>⊔</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">B\to A\sqcup B</annotation></semantics></math> which are jointly surjective and have disjoint image; we call <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⊔</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\sqcup B</annotation></semantics></math> the <strong>disjoint union</strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>.</p> <p>In particular, it follows that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/pretopos">pretopos</a> (as is any topos).</p> <h3 id="infinity">Infinity</h3> <p><strong>Axiom 4 (Infinity):</strong> <em>There exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi></mrow><annotation encoding="application/x-tex">N</annotation></semantics></math>, containing an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>o</mi></mrow><annotation encoding="application/x-tex">o</annotation></semantics></math>, and a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>:</mo><mi>N</mi><mo>→</mo><mi>N</mi></mrow><annotation encoding="application/x-tex">s:N\to N</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≠</mo><mi>o</mi></mrow><annotation encoding="application/x-tex">s(n)\neq o</annotation></semantics></math> for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>∈</mo><mi>N</mi></mrow><annotation encoding="application/x-tex">n\in N</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s(n) = s(m)</annotation></semantics></math> only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>=</mo><mi>m</mi></mrow><annotation encoding="application/x-tex">n = m</annotation></semantics></math> for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>,</mo><mi>m</mi><mo>∈</mo><mi>N</mi></mrow><annotation encoding="application/x-tex">n, m\in N</annotation></semantics></math>.</em></p> <p>It is easy to deduce any of the usual consequences of the axiom of infinity. The set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi></mrow><annotation encoding="application/x-tex">N</annotation></semantics></math> is not asserted to be minimal, but it is easy to cut it down to be so using separation. In particular, this axiom implies that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> has a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a>. We can then proceed to construct the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℚ</mi></mrow><annotation encoding="application/x-tex">\mathbb{Q}</annotation></semantics></math> of rational numbers and the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> of real numbers in any of the usual ways.</p> <p>Note also that Axiom 4 implies Axiom 0.</p> <p>We can however <a class="existingWikiWord" href="/nlab/show/natural+numbers+in+SEAR">define sets</a> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math> elements for each natural number <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math> directly axioms 0, 1, 2 and 3.</p> <h3 id="collection">Collection</h3> <p>The final axiom of SEAR is somewhat trickier to motivate. It corresponds to the <a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a> (or more precisely collection; see <a href="http://en.wikipedia.org/wiki/Axiom_schema_of_replacement">Wikipedia</a> until we get around to writing our own article) in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>ZFC</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{ZFC}</annotation></semantics></math>, and the reasons that we need it are the same as the reasons that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>ZFC</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{ZFC}</annotation></semantics></math> needs it.</p> <h4 id="the_ghost_of_a_universal_set">The ghost of a universal set</h4> <p>One way to motivate the collection axiom is as follows. Suppose for the sake of argument that there existed a <em>universal set</em>, meaning a set containing all other sets. Now in structural set theory this is meaningless, since no set can contain other sets, but there is an easy fix: we consider instead <em>indexed families</em> of sets. There are multiple ways to make this precise, but here is a very simple one: an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>-indexed <a class="existingWikiWord" href="/nlab/show/family+of+sets">family of sets</a> is simply a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">M:A\looparrowright X</annotation></semantics></math>. The set indexed by each element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a\in A</annotation></semantics></math> is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mi>a</mi></msub><mo>=</mo><mo stretchy="false">{</mo><mi>x</mi><mo>∈</mo><mi>X</mi><mo stretchy="false">|</mo><mi>M</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">M_a = \{x\in X | M(a,x)\}</annotation></semantics></math>. (Often one requires the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mi>a</mi></msub></mrow><annotation encoding="application/x-tex">M_a</annotation></semantics></math> to be a disjoint decomposition of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, so that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>M</mi> <mi>o</mi></msup></mrow><annotation encoding="application/x-tex">M^o</annotation></semantics></math> is a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">X\to A</annotation></semantics></math>, but this is unnecessary. In fact, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">M:A\looparrowright X</annotation></semantics></math> is a general family, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mo stretchy="false">|</mo><mi>M</mi><mo stretchy="false">|</mo></mrow><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">{|M|} \to A</annotation></semantics></math> is a function that represents a family in this stronger sense which is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math>.)</p> <p>With this definition, a <em>universal family of sets</em> would be a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> with a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math>-indexed family of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi><mo>:</mo><mi>U</mi><mo>↬</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">E:U\looparrowright Y</annotation></semantics></math> such that for any set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a unique <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>u</mi><mo>∈</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">u\in U</annotation></semantics></math> and a bijection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>≅</mo><msub><mi>E</mi> <mi>u</mi></msub></mrow><annotation encoding="application/x-tex">A\cong E_u</annotation></semantics></math>. The existence of such a universal set is inconsistent, but the collection axiom can be thought of as the “ghost” of what <em>would be implied</em> by Axioms 1 and 2 if a universal set <em>did</em> exist. Let’s now unravel that.</p> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> were a universal set, then any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>-indexed family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">M:A\looparrowright X</annotation></semantics></math> would induce a unique function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">f:A\to U</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>E</mi> <mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></msub><mo>≅</mo><msub><mi>M</mi> <mi>x</mi></msub></mrow><annotation encoding="application/x-tex">E_{f(x)} \cong M_x</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>. Conversely, any function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">f:A\to U</annotation></semantics></math> would induce an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>-indexed family of sets with this property: just take the composite relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi><mo>∘</mo><mi>f</mi></mrow><annotation encoding="application/x-tex">E \circ f</annotation></semantics></math>. (This family would not be unique, but it would be unique up to a suitable notion of <a class="existingWikiWord" href="/nlab/show/equivalence">equivalence</a> between indexed families.) Thus it is reasonable to consider the “ghost” of a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">f:A\to U</annotation></semantics></math> to be simply an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>-indexed family of sets.</p> <p>The ghost of a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>↬</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">A\looparrowright U</annotation></semantics></math> is even easier. By Axiom 1, to give such a relation would be equivalent to describing a property <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> that can obtain of an element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and a set. Thus, the ghost of a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>↬</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">A\looparrowright U</annotation></semantics></math> is simply such a property.</p> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> existed, Axiom 2 would imply that any relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>↬</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">A\looparrowright U</annotation></semantics></math> had a tabulation consisting of a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> and functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">p:B\to A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">q:B\to U</annotation></semantics></math>. We now kill <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> and inspect the ghostly remnants of this tabulation.</p> <p><strong>Axiom 5 (Collection):</strong> <em>For any set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and any property <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> which can obtain of an element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and a set, there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">p:B\to A</annotation></semantics></math>, and a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>-indexed family of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi><mo>:</mo><mi>B</mi><mo>↬</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">M:B\looparrowright Y</annotation></semantics></math> such that (1) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>p</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo>,</mo><msub><mi>M</mi> <mi>b</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(p(b),M_b)</annotation></semantics></math> holds for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">b\in B</annotation></semantics></math>, and (2) for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a\in A</annotation></semantics></math>, if there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(a,X)</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>im</mi><mo stretchy="false">(</mo><mi>p</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">a\in im(p)</annotation></semantics></math>.</em></p> <p>What this axiom asserts is actually a bit weaker than the precise ghost of a tabulation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>; that would require instead of (2) that for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a\in A</annotation></semantics></math> and any set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(a,X)</annotation></semantics></math>, there exists a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">b\in B</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo>=</mo><mi>a</mi></mrow><annotation encoding="application/x-tex">p(b)=a</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mi>b</mi></msub><mo>≅</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">M_b\cong X</annotation></semantics></math>. However, this stronger statement is still inconsistent, because if we took <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>=</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">A=1</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>=</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">P=\top</annotation></semantics></math> it would resurrect <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> in the form of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>! The form given above is weak enough to keep the dead in their graves, yet strong enough to be useful. (The former statement follows from the discussion below about inter-interpretability of SEAR and ZF, at least as long as the reader believes that ZF is consistent. The latter remains to be gone more into.)</p> <p><em>Exercise: why respect for the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a> necessary for Axiom 5 to be reasonable as stated?</em></p> <h4 id="applications_of_collection">Applications of collection</h4> <p>One thing that Axiom 5 is good for is the recursive construction of sets. For example, using Axioms 1–4 we can construct the sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi></mrow><annotation encoding="application/x-tex">N</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>N</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(N)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>P</mi><mo stretchy="false">(</mo><mi>N</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(P(N))</annotation></semantics></math>, and so on, but we cannot construct anything larger than all the sets in this sequence. Axiom 5 allows us to do that.</p> <p>(more detail to be added here…)</p> <h2 id="variants_and_comparisons">Variants and Comparisons</h2> <h3 id="the_axiom_of_choice">The Axiom of Choice</h3> <p>We obtain a theory called <strong>SEARC</strong> (SEAR with Choice) by adding the following axiom:</p> <p><strong>Axiom 6 (Choice):</strong> <em>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright B</annotation></semantics></math> is a relation such that for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a\in A</annotation></semantics></math>, there exists a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">b\in B</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(a,b)</annotation></semantics></math>, then there exists a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A\to B</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(a,f(a))</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a\in A</annotation></semantics></math>.</em></p> <p>This is easily seen to be equivalent to asserting that all surjections are <a class="existingWikiWord" href="/nlab/show/split+epimorphism">split</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>, which is a more common categorical form of the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>.</p> <h3 id="constructive_sear">Constructive SEAR</h3> <p>Axioms 1–5 of SEAR make perfect sense whether the ambient logic is <a class="existingWikiWord" href="/nlab/show/classical+logic">classical</a> or <a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">constructive</a>. By Diaconescu’s argument, Choice implies the logic is classical. We may call SEAR interpreted in intuitionistic logic <strong>ISEAR</strong>.</p> <p>To obtain a <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative</a> theory, Axiom 3 can be replaced by an appropriate weaker axiom, such as the existence of <a class="existingWikiWord" href="/nlab/show/disjoint+unions">disjoint unions</a> and <a class="existingWikiWord" href="/nlab/show/quotient+sets">quotient sets</a>. We may call this variation of SEAR <strong>PSEAR</strong>.</p> <p>If desired, we can also add <a class="existingWikiWord" href="/nlab/show/function+sets">function sets</a> or even a structural version of the axiom of <a class="existingWikiWord" href="/nlab/show/subset+collection">subset collection</a>; as usual, function sets, subset collection, and power sets are all equivalent using classical logic. We may call this variation of SEAR <strong>CSEAR</strong>.</p> <p>Compare <a class="existingWikiWord" href="/nlab/show/Erik+Palmgren">Erik Palmgren</a>'s <a href="http://www.math.uu.se/~palmgren/cetcs.pdf">constructive ETCS</a>.</p> <h3 id="bounded_sear_and_etcs">Bounded SEAR and ETCS</h3> <p>By <strong>bounded SEAR</strong> we mean the subtheory consisting of axioms 2–4 of SEAR plus</p> <p><strong>Axiom 1B (Bounded relational comprehension):</strong> <em>The same as Axiom 1, but the property <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> must be bounded (it can only involve quantifiers over elements, not sets or relations).</em></p> <p>All the theorems cited above remain true with Axiom 1 replaced by Axiom 1B, so bounded SEAR still implies that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is a well-pointed topos with a NNO. Therefore, <em>bounded SEARC</em> implies <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>. Conversely, it is not hard to show that given any <a class="existingWikiWord" href="/nlab/show/well-pointed+topos">well-pointed topos</a>, if we interpret “set” as “object of the topos”, “element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>” as “<a class="existingWikiWord" href="/nlab/show/global+element">global element</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">1\to A</annotation></semantics></math>”, and “relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\looparrowright B</annotation></semantics></math>” as “<a class="existingWikiWord" href="/nlab/show/subobject">subobject</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\times B</annotation></semantics></math>,” then Axioms 0, 1B, 2, and 3 are satisfied. It follows that ETCS also implies bounded SEARC, so the two are equivalent.</p> <p>ETCS can also be augmented with additional axioms to make it equivalent to full SEARC, but that is beyond our scope at the moment.</p> <h3 id="sear_and_zf">SEAR and ZF</h3> <h4 id="from_zf_to_sear">From ZF to SEAR</h4> <p>It is fairly straightforward to construct a model of SEAR from a model of <a class="existingWikiWord" href="/nlab/show/ZFC">ZF</a>. Given a model of ZF, we define the SEAR-sets to be the ZF-sets, and the SEAR-elements of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> to be the ZF-elements of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>. If we prefer, we can take the SEAR-elements of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> to be pairs <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(x,A)</annotation></semantics></math> where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><msub><mo>∈</mo> <mi>ZF</mi></msub><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in_{ZF} A</annotation></semantics></math>, so that the elements of distinct sets will be disjoint—but this is not necessary, since in SEAR the question of whether two distinct sets have elements in common is not even well-posed. Finally, we of course take the SEAR-relations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\looparrowright B</annotation></semantics></math> to be the ZF-subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\times B</annotation></semantics></math>, and we let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)</annotation></semantics></math> hold in SEAR iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><msub><mo>∈</mo> <mi>ZF</mi></msub><mi>φ</mi></mrow><annotation encoding="application/x-tex">(x,y)\in_{ZF} \varphi</annotation></semantics></math>. It is then easy to prove Axioms 0, 1, 2, 3, and 4 from the axioms of ZF, and likewise Axiom 6 follows easily from the axiom of choice in ZFC. (In fact, Z and ZC, where the replacement axiom is omitted, suffice for these conclusions.) The only axiom which requires some thought is Collection, and it is here that we use replacement.</p> <div class="num_theorem" id="zf-coll"> <h6 id="theorem_13">Theorem</h6> <p>The sets, elements, and relations in a model of ZF satisfy the Collection axiom of SEAR.</p> </div> <div class="proof"> <h6 id="proof_12">Proof</h6> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> be a set and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> a property as in Axiom 5. As given, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> is a first-order statement in the language of SEAR, but we can easily translate it into a statement in the language of ZF; from now on we work in ZF. Define</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>′</mo><mo>=</mo><mo stretchy="false">{</mo><mi>a</mi><mo>∈</mo><mi>A</mi><mo stretchy="false">|</mo><mo>∃</mo><mi>X</mi><mo>.</mo><mi>P</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo><mo stretchy="false">}</mo><mo>.</mo></mrow><annotation encoding="application/x-tex">A' = \{a\in A | \exists X. P(a,X)\}.</annotation></semantics></math></div> <p>By the <a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a>, for each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">a\in A'</annotation></semantics></math> there exists an <a class="existingWikiWord" href="/nlab/show/ordinal">ordinal</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>λ</mi></mrow><annotation encoding="application/x-tex">\lambda</annotation></semantics></math> and an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>∈</mo><msub><mi>V</mi> <mi>λ</mi></msub></mrow><annotation encoding="application/x-tex">X\in V_{\lambda}</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(a,X)</annotation></semantics></math>; let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>λ</mi> <mi>a</mi></msub></mrow><annotation encoding="application/x-tex">\lambda_a</annotation></semantics></math> be the <em>smallest</em> such <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>λ</mi></mrow><annotation encoding="application/x-tex">\lambda</annotation></semantics></math>. Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>↦</mo><msub><mi>V</mi> <mrow><msub><mi>λ</mi> <mi>a</mi></msub></mrow></msub></mrow><annotation encoding="application/x-tex">a\mapsto V_{\lambda_a}</annotation></semantics></math> is a class function, so by the axiom of replacement, the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><msub><mi>V</mi> <mrow><msub><mi>λ</mi> <mi>a</mi></msub></mrow></msub><mo stretchy="false">|</mo><mi>a</mi><mo>∈</mo><mi>A</mi><mo>′</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{V_{\lambda_a} | a\in A'\}</annotation></semantics></math> exists. Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi></mrow><annotation encoding="application/x-tex">Y</annotation></semantics></math> be the union of this set. Define</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>=</mo><mo stretchy="false">{</mo><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo><mo>∈</mo><mi>A</mi><mo>×</mo><mi>Y</mi><mo stretchy="false">|</mo><mi>P</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo><mo stretchy="false">}</mo><mo>,</mo></mrow><annotation encoding="application/x-tex">B = \{ (a,X)\in A\times Y | P(a,X)\},</annotation></semantics></math></div> <p>let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">p:B\to A</annotation></semantics></math> be the projection onto the first factor, and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi><mo>:</mo><mi>B</mi><mo>↬</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">M:B\looparrowright Y</annotation></semantics></math> be defined by</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>M</mi><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⇔</mo><mi>x</mi><mo>∈</mo><mi>X</mi><mo>.</mo></mrow><annotation encoding="application/x-tex">M((a,X),x) \Leftrightarrow x\in X.</annotation></semantics></math></div> <p>Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mrow><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow></msub><mo>=</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">M_{(a,X)} = X</annotation></semantics></math>, since each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>V</mi> <mi>λ</mi></msub></mrow><annotation encoding="application/x-tex">V_\lambda</annotation></semantics></math> is a transitive set, so <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo><mo>,</mo><msub><mi>M</mi> <mrow><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P((a,X), M_{(a,X)})</annotation></semantics></math> holds for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">(a,X)\in B</annotation></semantics></math>. Finally, by construction, if there exists <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(a,X)</annotation></semantics></math> then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>im</mi><mo stretchy="false">(</mo><mi>p</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">a\in im(p)</annotation></semantics></math>; thus the SEAR axiom of collection is satisfied.</p> </div> <p>Note the use of the axiom of foundation in addition to the axiom of replacement. This can be avoided if we use instead the ZF version of the <a href="http://en.wikipedia.org/wiki/Axiom_of_collection#Axiom_schema_of_collection">axiom of collection</a>, which is equivalent to the axiom of replacement over the other ZF axioms (including foundation), by an argument like that above.</p> <h4 id="from_sear_to_zf">From SEAR to ZF</h4> <p>Conversely, from any model of SEAR one can <em>construct</em> a model of ZF. The basic idea of this process is described at <a class="existingWikiWord" href="/nlab/show/pure+set">pure set</a>. Given a model of SEAR, we define a <strong>ZF-set</strong> to be an equivalence class of well-founded extensional accessible graphs, as described at <a class="existingWikiWord" href="/nlab/show/pure+set">pure set</a>. We define the global 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> on ZF-sets to be the “immediate subgraph” relation.</p> <p>The proofs of most of the axioms of ZF are straightforward, and may eventually be found at <a class="existingWikiWord" href="/nlab/show/pure+set">pure set</a>. Here we treat the proof of the replacement/collection axiom of ZF from the Collection axiom of SEAR, since that is specific to SEAR.</p> <div class="num_theorem" id="coll-zf"> <h6 id="theorem_14">Theorem</h6> <p>The ZF-sets constructed from a model of SEAR satisfy the ZF <a href="http://en.wikipedia.org/wiki/Axiom_of_collection#Axiom_schema_of_collection">axiom of collection</a> (which is equivalent to the axiom of replacement over the other axioms of ZF).</p> </div> <div class="proof"> <h6 id="proof_13">Proof</h6> <p>We will prove the version of the ZF axiom of collection which states that for any first-order formula <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> in the language of ZF, and any ZF-set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a ZF-set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> such that for any ZF-element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><msub><mo>∈</mo> <mi>ZF</mi></msub><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in_{ZF} A</annotation></semantics></math>, if there exists a ZF-set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(x,y)</annotation></semantics></math>, then there exists such a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> which is a ZF-element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>. Note that any first-order formula in the language of ZF about ZF-sets can easily be translated into a first-order formula in the language of SEAR.</p> <p>Fix such a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>; thus <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a SEAR-set equipped with a binary 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">\to</annotation></semantics></math> of a certain type. Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">A'</annotation></semantics></math> be the subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> consisting of the children of the root of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>. For a SEAR-set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>′</mo><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P'(a,X)</annotation></semantics></math> mean that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> admits the structure of a ZF-set such that the ZF-statement <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>down</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(down(a),X)</annotation></semantics></math> holds. By the SEAR axiom of collection, there is a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>A</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">p:B\to A'</annotation></semantics></math>, and a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>-indexed family of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi><mo>:</mo><mi>B</mi><mo>↬</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">M:B\looparrowright Y</annotation></semantics></math> such that (1) each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mi>b</mi></msub></mrow><annotation encoding="application/x-tex">M_b</annotation></semantics></math> admits the structure of a ZF-set with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>down</mi><mo stretchy="false">(</mo><mi>p</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>,</mo><msub><mi>M</mi> <mi>b</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(down(p(b)),M_b)</annotation></semantics></math>, and (2) if there is a ZF-set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>down</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(down(a),X)</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>im</mi><mo stretchy="false">(</mo><mi>p</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">a\in im(p)</annotation></semantics></math>.</p> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> be the subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>×</mo><mi>P</mi><mo stretchy="false">(</mo><mi>Y</mi><mo>×</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>×</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">B\times P(Y\times Y)\times Y</annotation></semantics></math> consisting of pairs <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>r</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(b,r,y)</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><msub><mi>M</mi> <mi>b</mi></msub></mrow><annotation encoding="application/x-tex">y\in M_b</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math> represents a binary relation on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mi>b</mi></msub></mrow><annotation encoding="application/x-tex">M_b</annotation></semantics></math> making it into a ZF-set such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>down</mi><mo stretchy="false">(</mo><mi>p</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>,</mo><msub><mi>M</mi> <mi>b</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(down(p(b)),M_b)</annotation></semantics></math>. Now <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> can be equipped with the relation that is the disjoint union of all the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math>s, i.e. we set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>r</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>→</mo><mo stretchy="false">(</mo><mi>b</mi><mo>′</mo><mo>,</mo><mi>r</mi><mo>′</mo><mo>,</mo><mi>y</mi><mo>′</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(b,r,y)\to (b',r',y')</annotation></semantics></math> iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>=</mo><mi>b</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">b=b'</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>=</mo><mi>r</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">r=r'</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><msub><mo>→</mo> <mi>r</mi></msub><mi>y</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">y\to_r y'</annotation></semantics></math>. Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>′</mo><mo>=</mo><mi>C</mi><mo>⊔</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">C'=C\sqcup 1</annotation></semantics></math> extend this relation with the additional point being a root, i.e. <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>r</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>→</mo><mo>⋆</mo></mrow><annotation encoding="application/x-tex">(b,r,y)\to \star</annotation></semantics></math> iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> is the root of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math>. Now <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">C'</annotation></semantics></math> is a well-founded accessible graph, but it may not be extensional; we take <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> to be the ZF-set represented by the extensional quotient of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">C'</annotation></semantics></math>.<br />Then for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><msub><mo>∈</mo> <mi>ZF</mi></msub><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in_{ZF}A</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≅</mo><mi>down</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x\cong down(a)</annotation></semantics></math> for some child <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi></mrow><annotation encoding="application/x-tex">a</annotation></semantics></math> of the root of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, i.e. <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">a\in A'</annotation></semantics></math>. Thus, if there is a ZF-set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(x,y)</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>im</mi><mo stretchy="false">(</mo><mi>p</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">a\in im(p)</annotation></semantics></math> and so there is such a ZF-set represented by one of the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math>‘s occurring in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>. By construction, this ZF-set is then equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>down</mi><mo stretchy="false">(</mo><mi>d</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">down(d)</annotation></semantics></math> for some child of the root of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>, hence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>down</mi><mo stretchy="false">(</mo><mi>d</mi><mo stretchy="false">)</mo><msub><mo>∈</mo> <mi>ZF</mi></msub><mi>D</mi></mrow><annotation encoding="application/x-tex">down(d) \in_{ZF} D</annotation></semantics></math>. Thus <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> satisfies the requirement of the ZF axiom of collection.</p> </div> <p>Thus, SEAR and SEARC are at least equiconsistent with ZF and ZFC, respectively. In fact, SEARC and ZFC are equivalent, in the sense that passage back and forth in either direction yields an equivalent model. However, passage from SEAR to ZF and back again can lose information, if there are sets in the model of SEAR which do not admit any well-founded extensional relation (this doesn’t happen in the presence of choice, since then every set can be well-ordered).</p> <h3 id="type_theory_and_internalization">Type theory and internalization</h3> <p>Every topos has an <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>, which is a <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>. However, the line between type theory and structural set theory is fine and sometimes hard to see; the main difference is that structural set theory can involve quantifiers over sets (= types), while type theory only allows (“bounded”) quantifiers over elements of types. However, formally, if one has a type judgment <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">A \; \mathrm{type}</annotation></semantics></math> and a type of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">Set \; \mathrm{type}</annotation></semantics></math> rather than a set judgment <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">set</mi></mrow><annotation encoding="application/x-tex">A \; \mathrm{set}</annotation></semantics></math>, one could use quantifers bounded over elements of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> instead of unbounded quantifiers. The type of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> in structural set theory behaves as a <a class="existingWikiWord" href="/nlab/show/Russell+universe">Russell universe</a> in <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, where given a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>∈</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">A \in Set</annotation></semantics></math> one could derive a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">A \; \mathrm{type}</annotation></semantics></math>. Through this correspondence, <em>Intuitionistic Bounded SEAR</em> can be treated as a type theory and interpreted internally in any topos with a NNO. Of course, if the topos is <a class="existingWikiWord" href="/nlab/show/boolean+topos">boolean</a>, then the logic can be classical.</p> <p>One can also write down stronger axioms on a topos such that if they are satisfied, then full Intuitionistic SEAR can be interpreted “internally” in that topos, extending the usual internal logic.</p> <h2 id="making_alternate_primitive_choices">Making alternate primitive choices</h2> <h3 id="threesorted_sear">Three-sorted SEAR</h3> <p>An alternate formulation of the theory uses three <a class="existingWikiWord" href="/nlab/show/sorts">sorts</a>, one for <a class="existingWikiWord" href="/nlab/show/sets">sets</a>, <a class="existingWikiWord" href="/nlab/show/elements">elements</a>, and <a class="existingWikiWord" href="/nlab/show/relations">relations</a>, making SEAR into a <a class="existingWikiWord" href="/nlab/show/three-sorted+set+theory">three-sorted set theory</a>. The membership <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a \in A</annotation></semantics></math> becomes a <a class="existingWikiWord" href="/nlab/show/relation">relation</a> between the sort of elements and the sort of <a class="existingWikiWord" href="/nlab/show/sets">sets</a>, while the relational domain and codomain notation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A \looparrowright B</annotation></semantics></math> also becomes a ternary relation between the sort of relations, and two copies of the sort of sets. There is a quinary relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">holds</mi><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo>,</mo><mi>φ</mi><mo>,</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{holds}(A, B, \varphi, a, b)</annotation></semantics></math> between all three sorts, which says that given sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, the relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math> holds for element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi></mrow><annotation encoding="application/x-tex">a</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A \looparrowright B</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a \in A</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">b \in B</annotation></semantics></math>.</p> <h3 id="SEPS">SEPS: Using pairs and subsets instead of relations</h3> <p>An alternate formulation of the theory, suggested by Toby, has four primitive notions: sets, elements, subsets, and a pairing operation. Sets and elements are as before. A <em>subset</em> is, like an element, attached to a certain set; it is always a subset <em>of</em> some set. Thus we have a typing declaration <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo>⊆</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">S\subseteq A</annotation></semantics></math>. We also have a primitive notion of when an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> <em>belongs to</em> a subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo>⊆</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">S\subseteq A</annotation></semantics></math>; thus now we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">x\in S</annotation></semantics></math> as a possible assertion of the theory (analogous to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(x,y)</annotation></semantics></math> before). We allow a typed equality predicate for subsets. Finally, there is an operation which assigns to every pair of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\times B</annotation></semantics></math>, and to every pair of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math> an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∈</mo><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">(x,y)\in A\times B</annotation></semantics></math>.</p> <p><strong>Axiom 0</strong> is the same as before.</p> <p><strong>Axiom <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mfrac><mn>1</mn><mn>2</mn></mfrac></mrow><annotation encoding="application/x-tex">\frac{1}{2}</annotation></semantics></math> (Pairing):</strong> <em>For every pair of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> and every element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>∈</mo><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">z\in A\times B</annotation></semantics></math>, there exists a unique pair of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>=</mo><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">z=(x,y)</annotation></semantics></math>.</em></p> <p><strong>Axiom <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mfrac><mn>1</mn><mn>2</mn></mfrac></mrow><annotation encoding="application/x-tex">1\frac{1}{2}</annotation></semantics></math> (Subset comprehension):</strong> <em>For every property <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> that can obtain of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> of some set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a unique subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo>⊆</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">S\subseteq A</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">x\in S</annotation></semantics></math> precisely when <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> obtains of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math></em></p> <p>We now define a <strong>relation</strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\looparrowright B</annotation></semantics></math> to be a subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\times B</annotation></semantics></math>. With this definition, Axiom <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mfrac><mn>1</mn><mn>2</mn></mfrac></mrow><annotation encoding="application/x-tex">1\frac{1}{2}</annotation></semantics></math> clearly implies Axiom 1 (relational comprehension). We define <strong>functions</strong> and their properties as before. Axiom <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mfrac><mn>1</mn><mn>2</mn></mfrac></mrow><annotation encoding="application/x-tex">\frac{1}{2}</annotation></semantics></math> implies that there are projection functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">A\times B\to A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\times B\to B</annotation></semantics></math> which make <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\times B</annotation></semantics></math> into a product in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>.</p> <p><strong>Axiom <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn><mfrac><mn>1</mn><mn>2</mn></mfrac></mrow><annotation encoding="application/x-tex">2\frac{1}{2}</annotation></semantics></math> (Separation):</strong> <em>For every set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and every subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo>⊆</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">S\subseteq A</annotation></semantics></math>, there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|S|</annotation></semantics></math> and an injective function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">i:{|S|}\to A</annotation></semantics></math> such that for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">x\in S</annotation></semantics></math> if and only if there is a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>∈</mo><mrow><mo stretchy="false">|</mo><mi>S</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">z\in {|S|}</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">i(z)=x</annotation></semantics></math>.</em></p> <p>Applying separation to subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\times B</annotation></semantics></math> and composing <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi></mrow><annotation encoding="application/x-tex">i</annotation></semantics></math> with the product projections, we recover Axiom 2 (tabulations). We can now go on with the subsequent axioms stated in the same way as before.</p> <h3 id="sepf_using_pairs_and_functions_instead_of_relations">SEPF: Using pairs and functions instead of relations</h3> <p>One could use functions instead of relations. Sets and elements are as before. A function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A \to B</annotation></semantics></math> depends on two sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, similar to a relation. For every function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A \to B</annotation></semantics></math> and element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a \in A</annotation></semantics></math>, one could form the element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f(a) \in B</annotation></semantics></math> called the <strong>function evaluation</strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> at <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi></mrow><annotation encoding="application/x-tex">a</annotation></semantics></math>. Finally, there is an operation which assigns to every pair of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\times B</annotation></semantics></math>, and to every pair of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math> an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∈</mo><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">(x,y)\in A\times B</annotation></semantics></math>, as well as functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mi>A</mi></msub><mo>:</mo><mi>A</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\pi_A:A \times B \to A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mi>B</mi></msub><mo>:</mo><mi>A</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\pi_B:A \times B \to B</annotation></semantics></math>.</p> <p><strong>Axiom 0</strong> is the same as before.</p> <p><strong>Axiom <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mfrac><mn>1</mn><mn>4</mn></mfrac></mrow><annotation encoding="application/x-tex">\frac{1}{4}</annotation></semantics></math> (strong extensionality):</strong> <em>Given function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">i:A \to B</annotation></semantics></math>, the following statements are logically equivalent to each other:</em></p> <ul> <li><em>there exists a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>i</mi> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo>:</mo><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">i^{-1}:B \to A</annotation></semantics></math> such that for all elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x \in A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y \in B</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>i</mi> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo stretchy="false">(</mo><mi>i</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">i^{-1}(i(x)) = x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo stretchy="false">(</mo><msup><mi>i</mi> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">i(i^{-1}(y)) = y</annotation></semantics></math></em></li> <li><em>for every element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">x \in B</annotation></semantics></math> there exists a unique element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">y \in A</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">i(y) = x</annotation></semantics></math></em></li> </ul> <p>A function is a <strong>bijection</strong> if one of the two conditions above hold.</p> <p><strong>Axiom <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mfrac><mn>1</mn><mn>2</mn></mfrac></mrow><annotation encoding="application/x-tex">\frac{1}{2}</annotation></semantics></math> (Pairing):</strong> <em>For every pair of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> and for every element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x \in A</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y \in B</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>∈</mo><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">z\in A\times B</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">\pi_A((x, y)) = x</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">\pi_B((x, y)) = y</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>=</mo><mo stretchy="false">(</mo><msub><mi>π</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>,</mo><msub><mi>π</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">z=(\pi_A(z),\pi_B(z))</annotation></semantics></math>.</em></p> <p>An function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A \to B</annotation></semantics></math> is an <strong>injection</strong> if for all elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x \in A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">y \in A</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x = y</annotation></semantics></math> if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>f</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(x) = f(y)</annotation></semantics></math>, and is usually denoted <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>↪</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A \hookrightarrow B</annotation></semantics></math>. <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a <strong>subset</strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> if it comes with an injection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mi>A</mi><mo>↪</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">i:A \hookrightarrow B</annotation></semantics></math>. We now define a <strong>relation</strong> to be a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> with an injective function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mi>R</mi><mo>↪</mo><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">i:R \hookrightarrow A\times B</annotation></semantics></math>.</p> <p><strong>Axiom <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn><mfrac><mn>1</mn><mn>2</mn></mfrac></mrow><annotation encoding="application/x-tex">2\frac{1}{2}</annotation></semantics></math> (Separation):</strong> <em>For every property <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> that can obtain of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> of some set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> and unique injection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mi>S</mi><mo>↪</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">i:S \hookrightarrow A</annotation></semantics></math> such that there exists an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">y \in S</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">i(y) = x</annotation></semantics></math> precisely when <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> obtains of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math></em></p> <p>A relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mi>R</mi><mo>↪</mo><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">i:R \hookrightarrow A \times B</annotation></semantics></math> is a <strong>total functional relation</strong> if for all elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a \in A</annotation></semantics></math>, there exists a unique element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">b \in B</annotation></semantics></math> and a unique element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>∈</mo><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">z \in A \times B</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">i(z) = (a, b)</annotation></semantics></math>. Since there is a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mi>A</mi></msub><mo>∘</mo><mi>i</mi><mo>:</mo><mi>R</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\pi_A \circ i:R \to A</annotation></semantics></math>, by strong extensionality there is an inverse function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi>π</mi> <mi>A</mi></msub><mo>∘</mo><mi>i</mi><msup><mo stretchy="false">)</mo> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo>:</mo><mi>A</mi><mo>→</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">(\pi_A \circ i)^{-1}:A \to R</annotation></semantics></math>, and the function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mi>B</mi></msub><mo>∘</mo><mo stretchy="false">(</mo><msub><mi>π</mi> <mi>A</mi></msub><mo>∘</mo><mi>i</mi><msup><mo stretchy="false">)</mo> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\pi_B \circ (\pi_A \circ i)^{-1}:A \to B</annotation></semantics></math> is the function satisfying <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo stretchy="false">(</mo><mo stretchy="false">(</mo><msub><mi>π</mi> <mi>A</mi></msub><mo>∘</mo><mi>i</mi><msup><mo stretchy="false">)</mo> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><msub><mi>π</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mo stretchy="false">(</mo><msub><mi>π</mi> <mi>A</mi></msub><mo>∘</mo><mi>i</mi><msup><mo stretchy="false">)</mo> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">i((\pi_A \circ i)^{-1}(a)) = (a, \pi_B((\pi_A \circ i)^{-1}(a))</annotation></semantics></math>. Thus, the <a class="existingWikiWord" href="/nlab/show/principle+of+unique+choice">principle of unique choice</a> holds.</p> <p>Applying separation to relations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mi>R</mi><mo>↪</mo><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">i:R \hookrightarrow A \times B</annotation></semantics></math> and using the <a class="existingWikiWord" href="/nlab/show/principle+of+unique+choice">principle of unique choice</a>, we recover Axioms 1 (relational comprehension) and 2 (tabulations). We can now go on with the subsequent axioms stated in the same way as before.</p> <h3 id="eqfree">Eliminating equality</h3> <p>As stated SEAR includes a fundamental “equality” relation on elements of a given set. However, we can also make equality into <em>structure</em>. This is definitely not along the “more accessible to undergraduates” direction! But it may sometimes be technically helpful.</p> <p>Consider a theory of <em><a class="existingWikiWord" href="/nlab/show/pre-sets">pre-sets</a></em>, <em>elements</em>, and <em>pre-relations</em> as in SEAR, with “pre-sets” replacing sets, except that there is no given equality relation on <em>anything</em>. Axiom 0 requires no modification. In Axiom 1, we reinterpret the “uniqueness” clause as a <em>definition</em> of what it means for two parallel pre-relations to be equal, i.e. <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>=</mo><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\varphi=\psi</annotation></semantics></math> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>⇔</mo><mi>ψ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)\Leftrightarrow\psi(x,y)</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> in the source and target of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\psi</annotation></semantics></math>.</p> <p>Before stating the version of Axiom 2 we need some definitions. We define a <strong>set</strong> to be a preset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> equipped with an <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence pre-relation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>=</mo> <mi>A</mi></msub></mrow><annotation encoding="application/x-tex">=_A</annotation></semantics></math> which satisfies the <a class="existingWikiWord" href="/nlab/show/principle+of+substitution">principle of substitution</a> and the <a class="existingWikiWord" href="/nlab/show/identity+of+indiscernibles">identity of indiscernibles</a>. A <strong>relation</strong> between sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mrow><msub><mo>=</mo> <mi>A</mi></msub></mrow><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(A,{=_A})</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mrow><msub><mo>=</mo> <mi>B</mi></msub></mrow><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(B,{=_B})</annotation></semantics></math> is a pre-relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mi>A</mi><mo>↬</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\varphi:A\looparrowright B</annotation></semantics></math> which is <em>extensional</em> in the sense that if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>′</mo><msub><mo>=</mo> <mi>A</mi></msub><mi>x</mi></mrow><annotation encoding="application/x-tex">x'=_A x</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>′</mo><msub><mo>=</mo> <mi>B</mi></msub><mi>y</mi></mrow><annotation encoding="application/x-tex">y'=_B y</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo>,</mo><mi>y</mi><mo>′</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x',y')</annotation></semantics></math>. Finally, a <strong>function</strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mrow><msub><mo>=</mo> <mi>A</mi></msub></mrow><mo stretchy="false">)</mo><mo>→</mo><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mrow><msub><mo>=</mo> <mi>B</mi></msub></mrow><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f:(A,{=_A}) \to (B,{=_B})</annotation></semantics></math> is a relation which is (a) <em><a class="existingWikiWord" href="/nlab/show/entire+relation">entire</a>:</em> for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math>, there is a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(x,y)</annotation></semantics></math>, and (b) <em><a class="existingWikiWord" href="/nlab/show/functional+relation">functional</a>:</em> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(x,y)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo>,</mo><mi>y</mi><mo>′</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(x',y')</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>x</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">x=_A x'</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><msub><mo>=</mo> <mi>B</mi></msub><mi>y</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">y=_B y'</annotation></semantics></math>.</p> <p>Now Axiom 2 reads: for any sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mrow><msub><mo>=</mo> <mi>A</mi></msub></mrow><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(A,{=_A})</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mrow><msub><mo>=</mo> <mi>B</mi></msub></mrow><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(B,{=_B})</annotation></semantics></math> and any relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>:</mo><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mrow><msub><mo>=</mo> <mi>A</mi></msub></mrow><mo stretchy="false">)</mo><mo>↬</mo><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mrow><msub><mo>=</mo> <mi>B</mi></msub></mrow><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi:(A,{=_A})\looparrowright (B,{=_B})</annotation></semantics></math>, there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><mo>,</mo><mrow><msub><mo>=</mo> <mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow></msub></mrow><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">({|\varphi|},{=_{|\varphi|}})</annotation></semantics></math> and functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">p:{|\varphi|}\to A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo>:</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">q:{|\varphi|}\to B</annotation></semantics></math> such that: (1) for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x\in A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">y\in B</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x,y)</annotation></semantics></math> if and only if there exists <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>∈</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">r\in {|\varphi|}</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo stretchy="false">(</mo><mi>r</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p(r,x)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo stretchy="false">(</mo><mi>r</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">q(r,y)</annotation></semantics></math>, and (2) for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>∈</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">r\in {|\varphi|}</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>∈</mo><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">s\in{|\varphi|}</annotation></semantics></math>, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo stretchy="false">(</mo><mi>r</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>A</mi></msub><mi>p</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p(r)=_A p(s)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo stretchy="false">(</mo><mi>r</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>B</mi></msub><mi>q</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">q(r)=_B q(s)</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><msub><mo>=</mo> <mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow></msub><mi>s</mi></mrow><annotation encoding="application/x-tex">r=_{|\varphi|}s</annotation></semantics></math>. Note that it is sufficient to assert merely that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">|\varphi|</annotation></semantics></math> is a pre-set and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi></mrow><annotation encoding="application/x-tex">q</annotation></semantics></math> are entire relations satisfying (1), since (2) can then be used to define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>=</mo> <mrow><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">|</mo></mrow></msub></mrow><annotation encoding="application/x-tex">=_{|\varphi|}</annotation></semantics></math> in such a way as to make it a set and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi></mrow><annotation encoding="application/x-tex">q</annotation></semantics></math> functions.</p> <p>The construction of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi></mrow><annotation encoding="application/x-tex">\emptyset</annotation></semantics></math> is just as in ordinary SEAR. The construction of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> in ordinary SEAR used equality, but we now have a simple replacement for it: let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> be any pre-set containing an element, equipped with the equivalence relation such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x=y</annotation></semantics></math> always for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>,</mo><mi>y</mi><mo>∈</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">x,y\in 1</annotation></semantics></math>. Similarly, in this variant we can construct quotient sets without needing powersets; we simply enlarge the equivalence relation on the underlying pre-set of a set.</p> <p>Of course, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mrow><msub><mo>=</mo> <mi>A</mi></msub></mrow><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(A,{=_A})</annotation></semantics></math> is a set, a <strong>subset</strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mo>↬</mo><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mrow><msub><mo>=</mo> <mi>A</mi></msub></mrow><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">1\looparrowright (A,{=_A})</annotation></semantics></math>. Axiom 3 can now be translated as-is, or it can be simplified to assert merely the existence of a pre-set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">P A</annotation></semantics></math> such that any subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is represented by some element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">P A</annotation></semantics></math>, with the uniqueness clause turned into a definition of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>=</mo> <mrow><mi>P</mi><mi>A</mi></mrow></msub></mrow><annotation encoding="application/x-tex">=_{P A}</annotation></semantics></math>. The same idea applies to all the other axioms.</p> <p>If to this equality-free version of SEAR we add a primitive notion of (non-extensional) “operation” and a <a class="existingWikiWord" href="/nlab/show/choice+operator">choice operator</a>, we obtain <a class="existingWikiWord" href="/nlab/show/SEAR%2B%CE%B5">SEAR+ε</a>.</p> <h2 id="related_pages_and_spinoffs">Related pages and spinoffs</h2> <p>The following pages develop various aspects of set theory in SEAR or related theories.</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/natural+numbers+in+SEAR">natural numbers in SEAR</a>: defining individual natural numbers without the axiom of infinity.</li> <li><a class="existingWikiWord" href="/nlab/show/categories+in+SEAR">categories in SEAR</a>: defining small categories, in response to a query on the blog.</li> <li><a class="existingWikiWord" href="/nlab/show/universes+in+SEAR">universes in SEAR</a>: how to formulate an axiom of <a class="existingWikiWord" href="/nlab/show/Grothendieck+universes">Grothendieck universes</a>.</li> <li><a class="existingWikiWord" href="/nlab/show/SEAR+plus+epsilon">SEAR plus epsilon</a>: a variant theory containing a <a class="existingWikiWord" href="/nlab/show/choice+operator">choice operator</a>.</li> <li><a class="existingWikiWord" href="/nlab/show/ETCR">ETCR</a>: A categorical version of Bounded SEARC.</li> <li><a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a>: A version of <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> that, like SEAR, includes elements as a primitive.</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on February 12, 2025 at 22:40:23. See the <a href="/nlab/history/SEAR" 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/SEAR" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/13686/#Item_8">Discuss</a><span class="backintime"><a href="/nlab/revision/SEAR/68" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/SEAR" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/SEAR" accesskey="S" class="navlink" id="history" rel="nofollow">History (68 revisions)</a> <a href="/nlab/show/SEAR/cite" style="color: black">Cite</a> <a href="/nlab/print/SEAR" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/SEAR" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>