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> pure set 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> pure set </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/636/#Item_10" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Pure sets</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="pure_sets">Pure sets</h1> <div class='maruku_toc'> <ul> <li><a href='#motivation'>Motivation</a></li> <li><a href='#idea'>Idea</a></li> <li><a href='#formalisation_in_material_set_theory'>Formalisation in material set theory</a></li> <li><a href='#formalization_in_structural_set_theory'>Formalization in structural set theory</a></li> <ul> <li><a href='#membership_graphs'>Membership graphs</a></li> <li><a href='#examples_of_apgs'>Examples of APGs</a></li> <li><a href='#ambiguities'>Ambiguities</a></li> <li><a href='#membership_trees'>Membership trees</a></li> <li><a href='#extensional_graphs'>Extensional graphs</a></li> <li><a href='#equivalence'>Equivalence</a></li> </ul> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="motivation">Motivation</h2> <p>In <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a>, there is an intuitive conception of what a <a class="existingWikiWord" href="/nlab/show/set">set</a> is, which may be stated informally as follows: a set is a collection of sets. Actually, it is possible to have <a class="existingWikiWord" href="/nlab/show/urelements">urelements</a> in a material set theory (such as <a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a>), although the most common axiom systems do not allow this; in any case we can say that a <em>pure</em> set is a collection of pure sets.</p> <p>The primary motivation for <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> is that this conception of a set is not needed in ordinary <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a>; it is sufficient to characterise the <a class="existingWikiWord" href="/nlab/show/category+of+sets">category of sets</a> (although a structural set theory can also be described in ways other than category-theoretic). However, material set theory is itself part of mathematics, and we may want to describe the material notion of a pure set in structural terms.</p> <p>There is also a very practical point to this exercise: the translation between material and structural set theories. Any model of a material set theory is already a model of a corresponding structural set theory, but we go through the yoga below to construct a model of a material set theory out of a model of a structural set theory. In particular, we must do this to prove that two set theories (one material and one structural) are equiconsistent.</p> <p>See also at <em><a class="existingWikiWord" href="/nlab/show/material-structural+adjunction">material-structural adjunction</a></em>.</p> <h2 id="idea">Idea</h2> <p>Taking a base notion of <a class="existingWikiWord" href="/nlab/show/set">set</a> as granted, we wish to define a <strong>pure set</strong> to be a set of pure sets. On the face of it, this is a circular definition, but like many such definitions, it can be made precise in (at least) two ways: <a class="existingWikiWord" href="/nlab/show/recursion">recursively</a> and <a class="existingWikiWord" href="/nlab/show/corecursion">corecursively</a>.</p> <ul> <li> <p>The ‘recursive’ meaning is that all pure sets must be <em>constructed</em>, starting from nothing, as sets of other previously constructed pure sets. This results in the <strong><a class="existingWikiWord" href="/nlab/show/well-founded+relation">well-founded</a> pure sets</strong>. Thus, at first, the only well-founded set possible is the <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi><mo>=</mo><mo stretchy="false">{</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\empty = \{ \}</annotation></semantics></math>, the set of no pure sets. Once you have that, you can form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⋆</mo><mo>=</mo><mo stretchy="false">{</mo><mi>∅</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\star = \{\empty\}</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mo>⋆</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{\star\}</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>∅</mi><mo>,</mo><mo>⋆</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{\empty,\star\}</annotation></semantics></math>, and so on. In this way we can obtain at least all <a class="existingWikiWord" href="/nlab/show/hereditarily+finite+sets">hereditarily finite sets</a>; if we use an <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a> as well, we can jump to the <a class="existingWikiWord" href="/nlab/show/countably+infinite+set">countably infinite set</a> of all hereditarily finite sets and continue from there.</p> </li> <li> <p>The ‘corecursive’ meaning is that any pure set can be <em>deconstructed</em> into a set of other pure sets, and every possible such deconstruction defines a unique pure set. In this way we obtain not just well-founded pure sets but also <strong>ill-founded pure sets</strong>. (The inclusion of well-founded sets among the ill-founded sets is an example of the <a class="existingWikiWord" href="/nlab/show/red+herring+principle">red herring principle</a>.) Possible examples of non-well-founded sets include a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>•</mo></mrow><annotation encoding="application/x-tex">\bullet</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>•</mo><mo>=</mo><mo stretchy="false">{</mo><mo>•</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\bullet = \{\bullet\}</annotation></semantics></math> (a suggestive model for the <a class="existingWikiWord" href="/nlab/show/point">point</a>), or 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> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>=</mo><mo stretchy="false">{</mo><mi>B</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">A = \{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><mo stretchy="false">{</mo><mi>∅</mi><mo>,</mo><mi>A</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">B = \{\empty, A\}</annotation></semantics></math>.</p> </li> </ul> <p>In addition, the meaning of this definition changes according to whether our <a class="existingWikiWord" href="/nlab/show/set+theory">set-theoretic</a> <a class="existingWikiWord" href="/nlab/show/foundations">foundation</a> is <a class="existingWikiWord" href="/nlab/show/material+set+theory">material</a> or <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural</a>.</p> <ul> <li> <p>If the foundation is ‘material’ or ‘membership-based,’ such as <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a>, then the elements of a set can, in fact, <em>be</em> other sets. Therefore, in this case we are defining (either recursively or corecursively) an <em>adjective</em> “pure” that can be applied to the noun “set”: a set is pure if at no point in its construction or deconstruction into elements do we encounter anything that is not a pure set.</p> <p>In the most common material set theories, such as <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a>, <em>all</em> sets are pure, since the only ‘things’ the theory deals with (hence the only things that can be elements of sets) are sets. However, there are easy modifications of these theories that allow ‘atoms’ or <a class="existingWikiWord" href="/nlab/show/urelement">urelement</a>s that are not sets, and in this case the pure sets will be those that ‘hereditarily’ contain no atoms. Many common material set theories (starting with von Neumann 1925, Zermelo 1930) also include an <a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a> asserting that all (pure) sets are well-founded; the dual <a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a> (due to Aczel) allows and ‘tames’ the ill-founded sets.</p> </li> <li> <p>If the foundation is ‘structural’ or ‘categorial’, such as <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> or <a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a>, then the elements of a set cannot <em>be</em> other sets. Thus, in this case we are defining a single noun “pure set,” with no <em>a priori</em> relation to the structural notion of “set” that occurs in the foundational theory. A <em>pure set</em>, according to this definition, is a set <em>equipped with structure</em> assigning to each of its elements another pure set (interpreted either recursively or corecursively).</p> <p>From this point of view, the definition of pure set provides a construction of a model of material set theory within a model of structural set theory: a global relation 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">\in</annotation></semantics></math> can be defined between pure sets which will satisfy the axioms of some material set theory. (Of course, the sets in a model of material set theory always model a structural set theory, so this is the ‘difficult’ direction of the equivalence between the two types of set theory.) Whether we use the recursive or corecursive definition determines whether the resulting material set theory will satisfy the axiom of foundation or the axiom of anti-foundation. Note that using these two choices, the composite operation “material <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> structural <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> material” reduces to the standard proofs of the relative consistency of the axioms of foundation and anti-foundation, since the passage from material to structural requires neither one.</p> </li> </ul> <h2 id="formalisation_in_material_set_theory">Formalisation in material set theory</h2> <p>In material set theory without urelements, every set is a pure set. If there are urelements, so that not all sets are pure, then it is easy to define the class of pure sets as follows:</p> <div class="un_defn"> <h6 id="definition">Definition</h6> <p>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> is <strong>pure</strong> if given any finite sequence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mi>n</mi></msub><mo>∈</mo><msub><mi>x</mi> <mrow><mi>n</mi><mo>−</mo><mn>1</mn></mrow></msub><mo>∈</mo><mi>…</mi><mo>∈</mo><msub><mi>x</mi> <mn>2</mn></msub><mo>∈</mo><msub><mi>x</mi> <mn>1</mn></msub><mo>∈</mo><msub><mi>x</mi> <mn>0</mn></msub><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">x_n \in x_{n-1} \in \dots \in x_2 \in x_1 \in x_0 = x</annotation></semantics></math>, all of the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">x_i</annotation></semantics></math> are sets.</p> </div> <p>Whether this produces the well-founded pure sets or the ill-founded ones depends on whether the sets in the ambient set theory are well-founded or ill-founded.</p> <p>If you are (unusually) working in an ill-founded material set theory and want only the well-founded pure sets, then you simply need to define the other adjective:</p> <div class="un_defn"> <h6 id="definition_2">Definition</h6> <p>A class <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> of sets is <strong><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>-inductive</strong> if whenever all elements of some 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> are 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>, then <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> itself is 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>. 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> is <strong>well-founded</strong> if it belongs to every <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>-inductive class <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>.</p> </div> <p>(That <em>all</em> sets are well-founded is the <a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a>.) 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 well-founded, then there can be no infinite sequence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∈</mo><mi>…</mi><mo>∈</mo><msub><mi>x</mi> <mn>2</mn></msub><mo>∈</mo><msub><mi>x</mi> <mn>1</mn></msub><mo>∈</mo><msub><mi>x</mi> <mn>0</mn></msub><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">\in \dots \in x_2 \in x_1 \in x_0 = x</annotation></semantics></math>, since the sets with no such sequence form an <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>-inductive class; the converse (that a set is well-founded if it has no such infinite sequence) holds using <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>. Then a well-founded pure set is simply a set that is both well-founded and pure.</p> <p>If you are (as usual) working in a well-founded material set theory and want to work with ill-founded pure sets, then you cannot do so directly; instead, follow the structural development in the next section.</p> <h2 id="formalization_in_structural_set_theory">Formalization in structural set theory</h2> <p>In a structural set theory like <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> or <a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a>, we can model a pure set by a graph describing its hereditary membership relation.</p> <p>One way to state the basic theoretical idea is that the class of well-founded sets is the <a class="existingWikiWord" href="/nlab/show/initial+algebra">initial algebra</a> of the covariant <a class="existingWikiWord" href="/nlab/show/power+set">power set</a> functor, while the class of ill-founded sets is the <a class="existingWikiWord" href="/nlab/show/terminal+coalgebra">terminal coalgebra</a> of the same functor. Of course, neither of these algebras exists as a set, since this would violate <a class="existingWikiWord" href="/nlab/show/Cantor%27s+theorem">Cantor's theorem</a>, but we can still describe what their elements would be like. We can also define these algebras as <a class="existingWikiWord" href="/nlab/show/discrete+category">discrete</a> <a class="existingWikiWord" href="/nlab/show/large+category">large categories</a>, or as proper classes in a structural set-class theory such as <a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a>.</p> <p>The discussion which follows is phrased informally, like most mathematics. However, it is purely structural and can be interpreted in any structural set theory. For instance, the definition below of a “graph” as a set with a binary relation should be formalized as a set <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> together with an injection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo>↪</mo><mi>G</mi><mo>×</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">R \hookrightarrow G \times G</annotation></semantics></math>.</p> <h3 id="membership_graphs">Membership graphs</h3> <p>To describe a pure set, we must give all the elements of that set, each of which is a pure set and thus must have its own elements, which are also pure sets, and so on. A convenient way to “picture” a pure set is with a <em>graph</em>.</p> <div class="un_defn"> <h6 id="definition_3">Definition</h6> <p>For the purposes of this page, a <strong>graph</strong> will mean a set <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> of <strong>nodes</strong> equipped with a binary <a class="existingWikiWord" href="/nlab/show/relation">relation</a> <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> on the nodes. A node <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> is called a <strong>child</strong> of a node <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>j</mi></mrow><annotation encoding="application/x-tex">j</annotation></semantics></math> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>→</mo><mi>j</mi></mrow><annotation encoding="application/x-tex">i \to j</annotation></semantics></math>.</p> </div> <p>The idea of a graph-picture of pure sets is that the <em>nodes</em> represent <em>pure sets</em>, and we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>→</mo><mi>j</mi></mrow><annotation encoding="application/x-tex">i\to j</annotation></semantics></math> precisely when <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>∈</mo><mi>j</mi></mrow><annotation encoding="application/x-tex">i\in j</annotation></semantics></math>. Clearly the membership relations between any collection of pure sets should be representable by a graph. To what extent the converse holds, i.e. which graphs can be interpreted as membership-relations between pure sets, depends on whether the pure sets in question are well-founded or ill-founded. For purposes of drawing well-founded pure sets, only well-founded graphs should be used, whereas arbitrary graphs can be used to draw ill-founded sets. (In fact, one form of the <a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a> is that any graph is the picture of some pure set.)</p> <div class="un_defn"> <h6 id="definition_4">Definition</h6> <p>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> of nodes in a graph is <strong><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>-inductive</strong> if whenever all children of some node <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> are in <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>, then <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> itself is in <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>. A graph is <strong><a class="existingWikiWord" href="/nlab/show/well-founded+relation">well-founded</a></strong> if the only <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>-inductive set of nodes is the set of all nodes.</p> </div> <p>Assuming the principle of <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>, well-foundedness is equivalent to saying that the tree has no infinite paths.</p> <p>If we want to use a graph to describe a <em>specific</em> pure set, then we should single out one particular node as representing <em>that</em> set. Moreover, it makes sense to demand that the graph contain no “superfluous” data other than what is necessary to describe the hereditary membership structure of the particular set in question.</p> <div class="un_defn"> <h6 id="definition_5">Definition</h6> <p>A graph is <strong>pointed</strong> if it is equipped with a specified node <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> called the <strong>root</strong>. A pointed graph is <strong>accessible</strong> if for every node <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>, there exists a path <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><msub><mi>x</mi> <mn>0</mn></msub><mo>→</mo><msub><mi>x</mi> <mn>1</mn></msub><mo>→</mo><mi>…</mi><mo>→</mo><msub><mi>x</mi> <mi>n</mi></msub><mo>=</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">x = x_0 \to x_1 \to \dots \to x_n =\top</annotation></semantics></math> to the root; this is equivalent to saying that <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 a <a class="existingWikiWord" href="/nlab/show/top+element">top element</a> for the reflexive-<a class="existingWikiWord" href="/nlab/show/transitive+closure">transitive closure</a> 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">\to</annotation></semantics></math>. An accessible pointed graph is abbreviated <strong>APG</strong>.</p> </div> <p>An APG gives all the data necessary to characterize a pure 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 the pure set in question is well-founded iff the APG is well-founded. We can think of the root as representing <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> itself, the root's children as the elements 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>, the next level as those elements' elements, and so on.</p> <p>If we want to think of these elements as pure sets themselves, then we can “externalize” them into separate APGs. Specifically, for any node <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> in a graph <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>, the subgraph consisting of all those nodes which admit some path to <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> is an APG, which describes the pure set represented by <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>; we write it as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">G/z</annotation></semantics></math> and call it the <strong>full subgraph</strong> of <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> rooted at <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>. If <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> is an APG and <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> is a child of the root, we say that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">G/z</annotation></semantics></math> is an <strong>immediate subgraph</strong> of <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>. The immediate subgraphs of <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> represent the pure sets that are the “elements” of the pure set represented by <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>. Thus, the APG <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> pictures the hierarchy of elements 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>, where each immediate subgraph <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">G/z</annotation></semantics></math> corresponds to its root <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>, and <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> is interpreted as membership.</p> <h3 id="examples_of_apgs">Examples of APGs</h3> <p>Note that the nodes in most of the pictures below have labels, but these are for illustration only; they are <em>not</em> part of the structure defining the tree.</p> <p>First, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi><mo>=</mo><mo stretchy="false">{</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\empty = \{ \}</annotation></semantics></math> consists of nothing but a root:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>∅</mi></mrow><annotation encoding="application/x-tex"> \empty </annotation></semantics></math></div> <p>The set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⋆</mo><mo>=</mo><mo stretchy="false">{</mo><mi>∅</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\star = \{\empty\}</annotation></semantics></math> has the empty set attached to the root (which we draw at the top):</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mo>⋆</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mi>∅</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { \star \\ \uparrow \\ \empty } </annotation></semantics></math></div> <p>Notice 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">\empty</annotation></semantics></math> is an immediate subgraph, so we can write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi><mo>∈</mo><mo>⋆</mo></mrow><annotation encoding="application/x-tex">\empty \in \star</annotation></semantics></math>.</p> <p>Then the two most obvious ways of representing the ordinal <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math> as a pure set, namely <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mn>2</mn> <mi>Z</mi></msub><mo>=</mo><mo stretchy="false">{</mo><mo>⋆</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">2_Z = \{\star\}</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mn>2</mn> <mi>N</mi></msub><mo>=</mo><mo stretchy="false">{</mo><mi>∅</mi><mo>,</mo><mo>⋆</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">2_N = \{\empty, \star\}</annotation></semantics></math>, can be drawn as follows:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><msub><mn>2</mn> <mi>Z</mi></msub></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mo>⋆</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mi>∅</mi></mtd></mtr></mtable></mrow><mspace width="1em"></mspace><mspace width="1em"></mspace><mspace width="1em"></mspace><mspace width="1em"></mspace><mrow><mtable><mtr><mtd></mtd> <mtd></mtd> <mtd><msub><mn>2</mn> <mi>N</mi></msub></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd> <mtd><mo>↖</mo></mtd></mtr> <mtr><mtd><mi>∅</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>⋆</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>∅</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { 2_Z \\ \uparrow \\ \star \\ \uparrow \\ \empty } \quad \quad \quad \quad \array { & & 2_N \\ & \nearrow & & \nwarrow \\ \empty & & & & \star \\ & & & & \uparrow \\ & & & & \empty } </annotation></semantics></math></div> <p>Looking at immediate subtrees, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⋆</mo><mo>∈</mo><msub><mn>2</mn> <mi>Z</mi></msub></mrow><annotation encoding="application/x-tex">\star \in 2_Z</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi><mo>∈</mo><msub><mn>2</mn> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">\empty \in 2_N</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⋆</mo><mo>∈</mo><msub><mn>2</mn> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">\star \in 2_N</annotation></semantics></math>, but <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi><mo>∉</mo><msub><mn>2</mn> <mi>Z</mi></msub></mrow><annotation encoding="application/x-tex">\empty \notin 2_Z</annotation></semantics></math>.</p> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mn>2</mn> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">2_N</annotation></semantics></math> can also be represented as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mo>⋆</mo><mo>,</mo><mi>∅</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{\star, \empty\}</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd></mtd> <mtd></mtd> <mtd><msub><mn>2</mn> <mi>N</mi></msub></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd> <mtd><mo>↖</mo></mtd></mtr> <mtr><mtd><mo>⋆</mo></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>∅</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mi>∅</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { & & 2_N \\ & \nearrow & & \nwarrow \\ \star & & & & \empty \\ \uparrow \\ \empty } </annotation></semantics></math></div> <p>Of course, as a graph this is isomorphic to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>∅</mi><mo>,</mo><mo>⋆</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{\empty, \star\}</annotation></semantics></math>, and hence should represent the same pure set.</p> <p>These sets are all well-founded. A non-well-founded set can be represented either by an infinite picture, or by a picture with loops. Here is an infinite picture of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>•</mo><mo>=</mo><mo stretchy="false">{</mo><mo>•</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\bullet = \{\bullet\}</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mo>•</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mo>•</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mo>•</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mi>⋮</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { \bullet \\ \uparrow \\ \bullet \\ \uparrow \\ \bullet \\ \uparrow \\ \vdots } </annotation></semantics></math></div> <p>and here is a finite picture:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd></mtd> <mtd><mo>•</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">/</mo></mtd> <mtd></mtd> <mtd><mo>↖</mo></mtd></mtr> <mtr><mtd><mo>\</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">/</mo></mtd></mtr> <mtr><mtd></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { & \bullet \\ / & & \nwarrow \\ \backslash & & / \\ } </annotation></semantics></math></div> <p>In both cases, the unique immediate subgraphs verify that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>•</mo><mo>∈</mo><mo>•</mo></mrow><annotation encoding="application/x-tex">\bullet \in \bullet</annotation></semantics></math>.</p> <h3 id="ambiguities">Ambiguities</h3> <p>APGs are sufficient to describe all pure sets, but multiple APGs, even non-isomorphic ones, can represent the “same” pure set. Firstly, we have so far not eliminated the possibility of duplicate branches. For instance, the pure set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mn>2</mn> <mi>Z</mi></msub></mrow><annotation encoding="application/x-tex">2_Z</annotation></semantics></math> can also be represented as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mo>⋆</mo><mo>,</mo><mo>⋆</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{\star, \star\}</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd></mtd> <mtd></mtd> <mtd><msub><mn>2</mn> <mi>Z</mi></msub></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd> <mtd><mo>↖</mo></mtd></mtr> <mtr><mtd><mo>⋆</mo></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>⋆</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mi>∅</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>∅</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { & & 2_Z \\ & \nearrow & & \nwarrow \\ \star & & & & \star \\ \uparrow & & & & \uparrow \\ \empty & & & & \empty } </annotation></semantics></math></div> <p>It is easy to eliminate APGs with such “obviously redundant” branches.</p> <div class="un_defn"> <h6 id="definition_6">Definition</h6> <p>An APG <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> is <strong>rigid</strong> if whenever <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 two children of the same node <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> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>x</mi><mo>≅</mo><mi>G</mi><mo stretchy="false">/</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">G/x \cong G/y</annotation></semantics></math>, then in fact <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>.</p> </div> <p>Assuming <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>, rigidity is equivalent to saying that any graph <a class="existingWikiWord" href="/nlab/show/automorphism">automorphism</a> is the identity function. Note also that if two rigid APGs are isomorphic, they must be uniquely isomorphic. Thus, for rigid APGs, being isomorphic is a <em>property</em>, rather than <em>structure</em>.</p> <p>Even among rigid APGs, however, there are are ambiguities. For example, the pure set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mn>2</mn> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">2_N</annotation></semantics></math> can also be drawn by the APG</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><msub><mn>2</mn> <mi>N</mi></msub></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd> <mtd><mo>↖</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">|</mo></mtd> <mtd></mtd> <mtd><mo>⋆</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">|</mo></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd></mtr> <mtr><mtd><mi>∅</mi></mtd> <mtd></mtd> <mtd></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { 2_N \\ \uparrow & \nwarrow \\ | & & \star \\ | & \nearrow & \\ \empty & & } </annotation></semantics></math></div> <p>The issue here is that the “same” pure set can occur in more than one place in the membership hierarchy of a pure set, and we have to choose whether or not to identify them in the graph. There are three solutions to this problem:</p> <ol> <li>Demand that duplicate occurrences of a pure set always be represented separately.</li> <li>Demand that duplicate occurrences always be identified, wherever they occur.</li> <li>Define a notion of “equivalence” between APGs which is looser than isomorphism.</li> </ol> <p>These are of course related; the first two can be seen as specifying a particular isomorphism class within each of the equivalence classes defined by the third. In particular, they all result in equivalent notions of pure set, when they all apply. (However, in <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative</a> set theories, it seems that only the first method is applicable.) We will consider them all in turn.</p> <h3 id="membership_trees">Membership trees</h3> <p>A natural way to ensure that the same node is never “shared” between two occurrences is to require that our APGs be <em>trees</em>.</p> <div class="un_defn"> <h6 id="definition_7">Definition</h6> <p>An pointed graph is a <strong>tree</strong> if every node admits a <em>unique</em> path to the root. Equivalently, <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> is a tree if its root <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 a <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> of the <a class="existingWikiWord" href="/nlab/show/quiver">quiver</a> generated by the 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>.</p> </div> <p>A tree may or may not be well-founded. Note, though, that in a tree, the <a class="existingWikiWord" href="/nlab/show/opposite+relation">opposite relation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>←</mo></mrow><annotation encoding="application/x-tex">\leftarrow</annotation></semantics></math> is automatically well-founded: each node has a unique <a class="existingWikiWord" href="/nlab/show/natural+number">natural number</a> <em>height</em>, namely the length of its unique path to the root, so well-foundedness of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math> implies well-foundedness 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">\leftarrow</annotation></semantics></math>.</p> <p>It now makes sense to define a <em>pure set</em> to be a <em>rigid accessible pointed tree</em>. The idea is that two such trees represent the same pure set iff they are isomorphic. We define “membership” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>∈</mo><mi>H</mi></mrow><annotation encoding="application/x-tex">G\in H</annotation></semantics></math> between such trees to mean that <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> is isomorphic to some immediate subtree of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> (that is, a tree <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi><mo stretchy="false">/</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">H/z</annotation></semantics></math> where <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> is a child of the root of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>).</p> <p>For example, the tree representation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mn>2</mn> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">2_N</annotation></semantics></math> is the one we gave first:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd></mtd> <mtd></mtd> <mtd><msub><mn>2</mn> <mi>N</mi></msub></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd> <mtd><mo>↖</mo></mtd></mtr> <mtr><mtd><mi>∅</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>⋆</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>∅</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array { & & 2_N \\ & \nearrow & & \nwarrow \\ \empty & & & & \star \\ & & & & \uparrow \\ & & & & \empty } </annotation></semantics></math></div> <p>and the tree representation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>•</mo><mo>=</mo><mo stretchy="false">{</mo><mo>•</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\bullet = \{\bullet\}</annotation></semantics></math> is the infinite path:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mo>•</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mo>•</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mo>•</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mi>⋮</mi><mo>.</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { \bullet \\ \uparrow \\ \bullet \\ \uparrow \\ \bullet \\ \uparrow \\ \vdots .} </annotation></semantics></math></div> <p>Of course, a well-founded <a class="existingWikiWord" href="/nlab/show/infinite+set">infinite set</a> also has an infinite picture, but there are no infinite paths. Here is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>ω</mi> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">\omega_N</annotation></semantics></math>, the set of von Neumann <a class="existingWikiWord" href="/nlab/show/natural+numbers">natural numbers</a>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><msub><mi>ω</mi> <mi>N</mi></msub></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd> <mtd><mo>↖</mo></mtd> <mtd><mi>⋯</mi></mtd></mtr> <mtr><mtd><mi>∅</mi></mtd> <mtd><mo>⋆</mo></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><msub><mn>2</mn> <mi>N</mi></msub></mtd> <mtd><mi>⋯</mi></mtd></mtr> <mtr><mtd></mtd> <mtd><mo stretchy="false">↑</mo></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd><mo stretchy="false">↑</mo></mtd> <mtd><mi>⋯</mi></mtd></mtr> <mtr><mtd></mtd> <mtd><mi>∅</mi></mtd> <mtd></mtd> <mtd><mi>∅</mi></mtd> <mtd></mtd> <mtd><mo>⋆</mo></mtd> <mtd><mi>⋯</mi></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo stretchy="false">↑</mo></mtd> <mtd><mi>⋯</mi></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>∅</mi></mtd> <mtd><mi>⋯</mi></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>⋮</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { & & & \omega_N \\ & \nearrow & \nearrow & & \nwarrow & \cdots \\ \empty & \star & & & & 2_N & \cdots \\ & \uparrow & & & \nearrow & \uparrow & \cdots \\ & \empty & & \empty & & \star & \cdots \\ & & & & & \uparrow & \cdots \\ & & & & & \empty & \cdots \\ & & & & & & \vdots } </annotation></semantics></math></div> <p>So we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi><mo>∈</mo><msub><mi>ω</mi> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">\empty \in \omega_N</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⋆</mo><mo>∈</mo><msub><mi>ω</mi> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">\star \in \omega_N</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mn>2</mn> <mi>N</mi></msub><mo>∈</mo><mi>ω</mi></mrow><annotation encoding="application/x-tex">2_N \in \omega</annotation></semantics></math>, etc.</p> <p>A tree models a <em><a class="existingWikiWord" href="/nlab/show/hereditarily+finite+set">hereditarily finite set</a></em> if every node has finitely many children; a tree models a well-founded hereditarily finite set if and only if it is finite and <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> is <a class="existingWikiWord" href="/nlab/show/decidable+subset">decidable</a>. The relationship between these two facts and the no-infinite-path formulation of well-foundedness is a form of <span class="newWikiWord">Kőnig's Lemma<a href="/nlab/new/Konig%27s+lemma">?</a></span>.</p> <p>Given these definitions, one can prove the various axioms of material set theory. Specifically, if <strong><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a></strong> holds for the structural sets (of nodes, etc) used in this definition, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mstyle mathvariant="bold"><mi>BZC</mi></mstyle> <mo>−</mo></msup></mrow><annotation encoding="application/x-tex">\mathbf{BZC}^-</annotation></semantics></math> (which is <strong><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></strong> with only <a class="existingWikiWord" href="/nlab/show/bounded+separation">bounded separation</a> and no axioms of <a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">replacement</a> or <a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">foundation</a>) holds for rigid trees, while <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>BZC</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{BZC}</annotation></semantics></math> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mstyle mathvariant="bold"><mi>BZC</mi></mstyle> <mo>−</mo></msup></mrow><annotation encoding="application/x-tex">\mathbf{BZC}^-</annotation></semantics></math> together with foundation) holds for well-founded rigid trees. Similar results hold for <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive</a> weakenings of ETCS and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mstyle mathvariant="bold"><mi>BZC</mi></mstyle> <mo>−</mo></msup></mrow><annotation encoding="application/x-tex">\mathbf{BZC}^-</annotation></semantics></math>, since these definitions involve only function-sets and not power-sets. Likewise, we can strengthen both sides with axioms of replacement, collection, or separation, or by adding <a class="existingWikiWord" href="/nlab/show/Grothendieck+universes">Grothendieck universes</a>.</p> <p>The argument for the <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a> is perhaps the most interesting; it goes as follows. If each immediate subtree <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">G/x</annotation></semantics></math> of <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> is isomorphic to an immediate subtree <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi><mo stretchy="false">/</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">H/y</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> and conversely, then <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> and <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> are mutually uniquely determined by rigidity, so we have a bijection between the children of the roots of <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> and of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>. Since the isomorphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>x</mi><mo>≅</mo><mi>H</mi><mo stretchy="false">/</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">G/x \cong H/y</annotation></semantics></math> are also unique, again by rigidity, and each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">G/x</annotation></semantics></math> is disjoint from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>x</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">G/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>x</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">x\neq x'</annotation></semantics></math>, by the tree property, we can piece together these isomorphisms to define an isomorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>≅</mo><mi>H</mi></mrow><annotation encoding="application/x-tex">G\cong H</annotation></semantics></math>. (In particular, the uniqueness of all these isomorphisms means that the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> is not needed.)</p> <p>(Note, though, that this is only the “weak” version of extensionality. This is sufficient for well-founded sets, but we may need to strengthen rigidity somehow to obtain stronger notions of <a class="existingWikiWord" href="/nlab/show/extensional+relation">extensionality</a>, which are generally more appropriate for ill-founded sets. More precisely, the well-founded rigid trees model the usual axioms of extensionality and foundation, while arbitrary rigid trees model not Aczel’s axiom of anti-foundation AFA, but its “Scott” variant, SAFA.)</p> <h3 id="extensional_graphs">Extensional graphs</h3> <p>The “tree” representation can be thought of as an <em>unwrapped</em> picture; we now consider a <em>wrapped</em> picture in which there is no duplication at all. The natural way to ensure this is to require our graphs to be <a class="existingWikiWord" href="/nlab/show/extensional+relation">extensional</a>. For well-founded graphs, this is easy: a well-founded graph is <em>extensional</em> if for any nodes <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> such that 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>, we have <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\to x</annotation></semantics></math> iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>→</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">z\to y</annotation></semantics></math>, then necessarily <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>. For non-well-founded graphs, we need the notion of “strong extensionality” defined as follows.</p> <div class="un_defn"> <h6 id="definition_8">Definition</h6> <p>If <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> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> are graphs, a <strong><a class="existingWikiWord" href="/nlab/show/bisimulation">bisimulation</a></strong> from <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> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> is 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">\sim</annotation></semantics></math> from <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> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</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>G</mi></mrow><annotation encoding="application/x-tex">x\in G</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>H</mi></mrow><annotation encoding="application/x-tex">y\in H</annotation></semantics></math> with <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\sim y</annotation></semantics></math>, then:</p> <ul> <li>For any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>→</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">a\to x</annotation></semantics></math>, there is some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>H</mi></mrow><annotation encoding="application/x-tex">b\in H</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>→</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">b\to y</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></mrow><annotation encoding="application/x-tex">a\sim b</annotation></semantics></math>, and</li> <li>For any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>→</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">b\to y</annotation></semantics></math>, there is some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">a\in G</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>→</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">a\to x</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></mrow><annotation encoding="application/x-tex">a\sim b</annotation></semantics></math>.</li> </ul> <p>A graph <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> is <strong>extensional</strong> if the largest bisimulation from <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> to <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> is the identity.</p> </div> <p>The idea is that a bisimulation identifies pairs of nodes which “represent the same pure set.” One can show that a well-founded graph is extensional in this sense iff it is extensional in the weaker sense given above. Note also that any extensional APG is necessarily rigid, since any isomorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>x</mi><mo>≅</mo><mi>G</mi><mo stretchy="false">/</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">G/x \cong G/y</annotation></semantics></math> induces a bisimulation.</p> <p>Thus, it also makes sense to define a <em>pure set</em> to be an <em>extensional APG</em>. Two such APGs represent the same set iff they are isomorphic, and we define membership in the same way: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>∈</mo><mi>H</mi></mrow><annotation encoding="application/x-tex">G\in H</annotation></semantics></math> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>≅</mo><mi>H</mi><mo stretchy="false">/</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">G\cong H/x</annotation></semantics></math> for some child <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 the root of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>. Of course, one can again prove the axioms of material set theory from this definition. If we restrict to well-founded extensional APGs, we get the axiom of foundation, while if we allow all extensional APGs, we get Aczel’s axiom af anti-foundation (along with its strong version of the axiom of extensionality). Note that this definition is not predicative, since the notion of extensionality involves <a class="existingWikiWord" href="/nlab/show/quantification">quantification</a> over bisimulations, which are relations, i.e. subsets. Thus, it requires at least <a class="existingWikiWord" href="/nlab/show/limited+separation">limited separation</a>.</p> <p>For example, the extensional representation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mn>2</mn> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">2_N</annotation></semantics></math> is this one:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><msub><mn>2</mn> <mi>N</mi></msub></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd> <mtd><mo>↖</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">|</mo></mtd> <mtd></mtd> <mtd><mo>⋆</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">|</mo></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd></mtr> <mtr><mtd><mi>∅</mi></mtd> <mtd></mtd> <mtd></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { 2_N \\ \uparrow & \nwarrow \\ | & & \star \\ | & \nearrow & \\ \empty & & } </annotation></semantics></math></div> <p>while the extensional representation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>•</mo><mo>=</mo><mo stretchy="false">{</mo><mo>•</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\bullet = \{\bullet \}</annotation></semantics></math> is the loop:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd></mtd> <mtd><mo>•</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">/</mo></mtd> <mtd></mtd> <mtd><mo>↖</mo></mtd></mtr> <mtr><mtd><mo>\</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">/</mo></mtd></mtr> <mtr><mtd></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { & \bullet \\ / & & \nwarrow \\ \backslash & & / \\ } </annotation></semantics></math></div> <p>Finally, here is the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>ω</mi> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">\omega_N</annotation></semantics></math> of von Neumann <a class="existingWikiWord" href="/nlab/show/natural+numbers">natural numbers</a>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd></mtd> <mtd></mtd> <mtd><msub><mi>ω</mi> <mi>N</mi></msub></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd><mo stretchy="false">↑</mo></mtd> <mtd><mo>↖</mo></mtd> <mtd><mi>⋯</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">|</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">|</mo></mtd> <mtd></mtd> <mtd><msub><mn>2</mn> <mi>N</mi></msub></mtd> <mtd><mi>⋯</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">|</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">|</mo></mtd> <mtd><mo>↗</mo></mtd> <mtd><mo stretchy="false">↑</mo></mtd> <mtd><mi>⋯</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">|</mo></mtd> <mtd></mtd> <mtd><mo>⋆</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">|</mo></mtd> <mtd><mi>⋯</mi></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>\</mo></mtd> <mtd><mo stretchy="false">↑</mo></mtd> <mtd><mo stretchy="false">/</mo></mtd> <mtd><mi>⋯</mi></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mi>∅</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array { & & \omega_N \\ & \nearrow & \uparrow & \nwarrow & \cdots \\ | & & | & & 2_N & \cdots \\ | & & | & \nearrow & \uparrow & \cdots \\ | & & \star & & | & \cdots \\ & \backslash & \uparrow & / & \cdots \\ & & \empty } </annotation></semantics></math></div> <p>Again we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi><mo>∈</mo><msub><mi>ω</mi> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">\empty \in \omega_N</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⋆</mo><mo>∈</mo><msub><mi>ω</mi> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">\star \in \omega_N</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mn>2</mn> <mi>N</mi></msub><mo>∈</mo><mi>ω</mi></mrow><annotation encoding="application/x-tex">2_N \in \omega</annotation></semantics></math>, etc.</p> <p>Now an extensional accessible graph models a <a class="existingWikiWord" href="/nlab/show/hereditarily+finite+set">hereditarily finite set</a> iff the graph itself is finite and <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> is decidable.</p> <h3 id="equivalence">Equivalence</h3> <p>Finally, we consider the third solution to the ambiguity problem, and its relation to the first two: defining a looser notion of equivalence between APGs. Recall the notion of bisimulation. We say that two APGs <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> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> are <strong>equivalent</strong> if there is a bisimulation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∼</mo></mrow><annotation encoding="application/x-tex">\sim</annotation></semantics></math> from <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> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo><mo>∼</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">\top\sim\top</annotation></semantics></math>. Note that if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∼</mo></mrow><annotation encoding="application/x-tex">\sim</annotation></semantics></math> is a bisimulation from <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> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</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>y</mi></mrow><annotation encoding="application/x-tex">x\sim y</annotation></semantics></math>, then the APGs <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">G/x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi><mo stretchy="false">/</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">H/y</annotation></semantics></math> are equivalent; this justifies the interpretation of a bisimulation.</p> <p>We can now define a <em>pure set</em> to be an APG, with <em>equality</em> represented by <em>equivalence</em> in the above sense. Likewise, we define “membership” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>∈</mo><mi>H</mi></mrow><annotation encoding="application/x-tex">G\in H</annotation></semantics></math> to mean that <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> is <em>equivalent</em> to some immediate subgraph of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>. One can again prove the various axioms of material set theory with these definitions (either using well-founded APGs or arbitrary ones). As with extensional APGs, in this case we obtain the <em>strong</em> notion of <a class="existingWikiWord" href="/nlab/show/extensional+relation">extensionality</a> (which is equivalent to the weak one for well-founded sets). This definition is also not predicative.</p> <p>The relationship of this approach to the previous ones is as follows.</p> <ol> <li> <p>Every APG is equivalent to an extensional one. Namely, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≈</mo></mrow><annotation encoding="application/x-tex">\approx</annotation></semantics></math> be the maximal bisimulation on <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> (the union of all bisimulations); it is an equivalence relation, and its quotient <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></mrow><annotation encoding="application/x-tex">G/\approx</annotation></semantics></math> inherits the structure of an extensional APG which is equivalent to <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>. This is the <em>extensional quotient</em>; see <a class="existingWikiWord" href="/nlab/show/extensional+relation">extensional relation</a>.</p> </li> <li> <p>Two extensional APGs are equivalent iff they are isomorphic. For if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∼</mo></mrow><annotation encoding="application/x-tex">\sim</annotation></semantics></math> is a bisimulation from <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> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>, then defining <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\approx y</annotation></semantics></math> in <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> if there exists a node <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> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∼</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">x\sim z</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>z</mi></mrow><annotation encoding="application/x-tex">y\sim z</annotation></semantics></math> gives a bisimulation on <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>, which must be the identity, and similarly for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>; hence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∼</mo></mrow><annotation encoding="application/x-tex">\sim</annotation></semantics></math> must in fact be a bijection. Thus, the notion of “pure set” obtained from “extensional APGs and isomorphism” is the same as that obtained from “arbitrary APGs and equivalence.”</p> </li> <li> <p>Every APG is equivalent to one that is a tree, its “unwrapping”. The nodes of the tree can be taken to be the finite paths <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mi>n</mi></msub><mo>→</mo><mi>…</mi><mo>→</mo><msub><mi>x</mi> <mn>0</mn></msub><mo>=</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">x_n \to \dots \to x_0 = \top</annotation></semantics></math> ending at the root, with any “one-level extension” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mrow><mi>n</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>→</mo><msub><mi>x</mi> <mi>n</mi></msub><mo>→</mo><mi>…</mi><mo>→</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">x_{n+1} \to x_n \to \dots \to \top</annotation></semantics></math> being a child of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mi>n</mi></msub><mo>→</mo><mi>…</mi><mo>→</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">x_n \to \dots\to \top</annotation></semantics></math>. The bisimulation relates each path <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mi>n</mi></msub><mo>→</mo><mi>…</mi><mo>→</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">x_n \to \dots\to \top</annotation></semantics></math> to its initial node <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mi>n</mi></msub></mrow><annotation encoding="application/x-tex">x_n</annotation></semantics></math>.</p> </li> <li> <p>Moreover, every APG is equivalent to a <em>rigid</em> accessible pointed tree. The key here is to first take the extensional quotient, then perform the above “unwrapping” construction: the unwrapping of any extensional graph will always be rigid.</p> </li> <li> <p>Two well-founded rigid accessible pointed trees are equivalent iff they are isomorphic. For if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∼</mo></mrow><annotation encoding="application/x-tex">\sim</annotation></semantics></math> is a bisimulation from <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> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>, define a new 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">\simeq</annotation></semantics></math> from <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> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</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>y</mi></mrow><annotation encoding="application/x-tex">x\simeq y</annotation></semantics></math> iff there are paths from <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> to the corresponding roots which are pointwise related 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">\sim</annotation></semantics></math>, i.e. we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><msub><mi>x</mi> <mi>n</mi></msub><mo>→</mo><msub><mi>x</mi> <mrow><mi>n</mi><mo>−</mo><mn>1</mn></mrow></msub><mo>→</mo><mi>⋯</mi><mo>→</mo><msub><mi>x</mi> <mn>1</mn></msub><mo>→</mo><msub><mi>x</mi> <mn>0</mn></msub><mo>=</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">x = x_n \to x_{n-1} \to \cdots \to x_1 \to x_0 = \top</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><mi>y</mi> <mi>n</mi></msub><mo>→</mo><msub><mi>y</mi> <mrow><mi>n</mi><mo>−</mo><mn>1</mn></mrow></msub><mo>→</mo><mi>⋯</mi><mo>→</mo><msub><mi>y</mi> <mn>1</mn></msub><mo>→</mo><msub><mi>y</mi> <mn>0</mn></msub><mo>=</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">y = y_n \to y_{n-1} \to \cdots \to y_1 \to y_0 = \top</annotation></semantics></math>, with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mi>i</mi></msub><mo>∼</mo><msub><mi>y</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">x_i \sim y_i</annotation></semantics></math>. We can then prove by well-founded induction that whenever <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\simeq y</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≃</mo></mrow><annotation encoding="application/x-tex">\simeq</annotation></semantics></math> is a bijection between the children 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 of <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>. For assume that all the children 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> have this property. Then if we have <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></mrow><annotation encoding="application/x-tex">x' \to x</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><mo>→</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">x''\to x</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>′</mo><mo>∼</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x' \sim y</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><mo>∼</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x'' \sim y</annotation></semantics></math>, then by hypothesis <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∼</mo></mrow><annotation encoding="application/x-tex">\sim</annotation></semantics></math> is a bijection between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>x</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">G/x'</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi><mo stretchy="false">/</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">H/y</annotation></semantics></math>, and between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>x</mi><mo>″</mo></mrow><annotation encoding="application/x-tex">G/x''</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi><mo stretchy="false">/</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">H/y</annotation></semantics></math>, hence we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo stretchy="false">/</mo><mi>x</mi><mo>′</mo><mo>≅</mo><mi>G</mi><mo stretchy="false">/</mo><mi>x</mi><mo>″</mo></mrow><annotation encoding="application/x-tex">G/x' \cong G/x''</annotation></semantics></math>; thus by rigidity <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>. Therefore, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≃</mo></mrow><annotation encoding="application/x-tex">\simeq</annotation></semantics></math> is a bijection between the children 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 the children of <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>. The construction 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">\simeq</annotation></semantics></math> then ensures that for any child <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></mrow><annotation encoding="application/x-tex">x'\to x</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≃</mo></mrow><annotation encoding="application/x-tex">\simeq</annotation></semantics></math> relates each node in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo stretchy="false">/</mo><mi>x</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">X/x'</annotation></semantics></math> to a node in at most one <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi><mo stretchy="false">/</mo><mi>y</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">Y/y'</annotation></semantics></math>; hence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≃</mo></mrow><annotation encoding="application/x-tex">\simeq</annotation></semantics></math> is in fact a bijection from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo stretchy="false">/</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">X/x</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi><mo stretchy="false">/</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">Y/y</annotation></semantics></math>. Thus, by induction, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≃</mo></mrow><annotation encoding="application/x-tex">\simeq</annotation></semantics></math> is a bijection.</p> </li> </ol> <p>In order to extend this last result to non-well-founded trees, we would need to use a stronger notion of rigidity. (This makes sense since SAFA is incompatible with AFA. We could expect to be able to use “Scott-extensionality” in place of extensionality to obtain a theory equivalent to that of rigid trees.) For example, the following two ill-founded trees are equivalent but not isomorphic, yet both are rigid.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mo>•</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mo>•</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↑</mo></mtd></mtr> <mtr><mtd><mo>•</mo></mtd></mtr> <mtr><mtd><mi>⋮</mi></mtd></mtr></mtable></mrow><mspace width="1em"></mspace><mspace width="1em"></mspace><mspace width="1em"></mspace><mspace width="1em"></mspace><mrow><mtable><mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>•</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd> <mtd><mo>↖</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mo>•</mo></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>•</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd> <mtd><mo>↖</mo></mtd></mtr> <mtr><mtd><mi>⋰</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>•</mo></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>•</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>↗</mo></mtd> <mtd></mtd> <mtd><mo>↖</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mi>⋰</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>⋰</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>⋱</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ \bullet \\ \uparrow \\ \bullet \\ \uparrow \\ \bullet \\ \vdots } \quad\quad\quad\quad \array{ & & & & \bullet \\ & & & \nearrow & & \nwarrow\\ & & \bullet & & & & \bullet\\ & \nearrow & & & & \nearrow & & \nwarrow\\ \udots & & & & \bullet & & & & \bullet\\ & & & \nearrow & & & & \nearrow & & \nwarrow\\ & & \udots & & & & \udots & & & & \ddots } </annotation></semantics></math></div> <p>In conclusion, there are two extreme ways to represent a pure set by an isomorphism class of graphs, but any accessible pointed graph will represent a pure set one way or another. For well-founded sets, the two extreme ways are equivalent, but for ill-founded sets the choice between them can make a difference (and in fact, there are a number of other possible variants, corresponding to the spectrum of anti-foundation axioms discussed by Aczel).</p> <p>Note that the version on the left is the unwrapping of the loop; we would like a stronger version of rigidity that would rule out the version on the right. As it is, the best that we have come up with is simply: isomorphic to the unwrapping of some extensional APG. Technically this works, but it is not very satifsying.</p> <h2 id="references">References</h2> <ul> <li>Peter Aczel (1988). Non-well-founded sets. CSLI 14; Stanford University. <a href="http://irafs.org/courses/materials/aczel_set_theory.pdf">PDF</a>.</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on December 12, 2022 at 13:12:10. See the <a href="/nlab/history/pure+set" 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/pure+set" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/636/#Item_10">Discuss</a><span class="backintime"><a href="/nlab/revision/pure+set/50" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/pure+set" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/pure+set" accesskey="S" class="navlink" id="history" rel="nofollow">History (50 revisions)</a> <a href="/nlab/show/pure+set/cite" style="color: black">Cite</a> <a href="/nlab/print/pure+set" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/pure+set" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>