Set theories that do require the existence of urelements? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-18T23:55:05Z http://mathoverflow.net/feeds/question/12905 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/12905/set-theories-that-do-require-the-existence-of-urelements Set theories that do require the existence of urelements? Hans Stricker 2010-01-25T07:42:05Z 2011-03-03T15:52:02Z <p>I am looking for an axiomatic set theory that not only <em>admits</em> the existence of urelements/atoms (via two-sortedness or an additional unary predicate) but <em>requires</em> it, e.g. by an axiom like "for each set there is an equipollent set of urelements" (= "there are arbitrarily many urelements"). Any references?</p> http://mathoverflow.net/questions/12905/set-theories-that-do-require-the-existence-of-urelements/12933#12933 Answer by Hans Stricker for Set theories that do require the existence of urelements? Hans Stricker 2010-01-25T13:34:40Z 2010-01-25T13:34:40Z <p>In the final end I found such a theory, it's called ZFCUA (= Zermelo Frankel set theory with the axiom of choice and unlimited atoms), see <a href="http://cs.nyu.edu/pipermail/fom/2004-January/007845.html" rel="nofollow">Faithful Representation in Set Theory with Atoms</a> by Harvey Friedman.</p> <p>The relevant axiom is #11: "There is no set consisting of all atoms."</p> <p>A consequence of this axiom is, that there definitely <strong>are</strong> atoms (since the empty set is a set) and furthermore, that there are so many, that the collection of all of them is not a set but a proper class.</p> http://mathoverflow.net/questions/12905/set-theories-that-do-require-the-existence-of-urelements/12934#12934 Answer by Joel David Hamkins for Set theories that do require the existence of urelements? Joel David Hamkins 2010-01-25T13:59:08Z 2010-01-25T13:59:08Z <p>Your question is equivalent to asking whether the urelements, or atoms, can form a proper class. This axiom is consistent with ZFA, but usually ZFA is introduced so as to not insist on this (and indeed, not insist on any atoms at all). I believe that many (or most) of the other standard set-theories-with-urelements also allow this. </p> <p>Andreas Blass has an article <a href="http://www.jstor.org/pss/1998165" rel="nofollow">here</a>, where he investigates the connection between some theorems in homological algebra and the Axiom of Choice. In his introduction, he states: </p> <blockquote> <blockquote> <p>In Section 3, we construct a model of set theory with no nontrivial injective abelian groups. It is a permutation model in which the atoms (= urelements) form a proper class;</p> </blockquote> </blockquote> <p>In contrast, sometimes it is useful to have only a set of atoms, as witnessed by <a href="http://h.web.umkc.edu/halle/PapersForEveryone/PermSVC.pdf" rel="nofollow">Eric Hall's article</a>, which contains the following remark.</p> <blockquote> <blockquote> <p>Definitions and Conventions. The theory ZFA is a modification of ZF allowing atoms, also known as urelements. See Jech [4] for a precise definition. A model of ZFA may have a proper class of atoms; however, for this paper we redefine ZFA to include an axiom which says that the class of atoms is a set (always denoted by A).</p> </blockquote> </blockquote> http://mathoverflow.net/questions/12905/set-theories-that-do-require-the-existence-of-urelements/15747#15747 Answer by Russell O'Connor for Set theories that do require the existence of urelements? Russell O'Connor 2010-02-18T19:39:32Z 2010-02-18T19:39:32Z <p>Nominal logic is based on the Frænkel-Mostowski permutation model of set theory. In particular Nominal logic has a freshness axiom that states <code>${\forall}x. {\exists}a \in \mathbb{A}. a \# x$</code>, where $\mathbb{A}$ is the set of atoms and <code>#</code> is a definable relation which is a bit too complicated to put here.</p> <p>For reference, see the work by Andrew Pitts and Murdoch Gabbay. For example "<a href="http://portal.acm.org/citation.cfm?id=788938" rel="nofollow">A New Approach to Abstract Syntax Involving Binders</a>".</p> http://mathoverflow.net/questions/12905/set-theories-that-do-require-the-existence-of-urelements/57259#57259 Answer by Ian Maxwell for Set theories that do require the existence of urelements? Ian Maxwell 2011-03-03T15:52:02Z 2011-03-03T15:52:02Z <p>I don't know if this is exactly what you're looking for, but it's a theorem of NFU that $|\mathcal{P}(V)| &lt; |V|$---which has as a corollary not only that there are atoms, but that the set of atoms is equipollent with the universe.</p> <p>(A somewhat more disquieting way of putting this is that there are more atoms than there are sets.)</p>