## Set theories that do require the existence of urelements?

I am looking for an axiomatic set theory that not only admits the existence of urelements/atoms (via two-sortedness or an additional unary predicate) but requires it, e.g. by an axiom like "for each set there is an equipollent set of urelements" (= "there are arbitrarily many urelements"). Any references?

-

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 Faithful Representation in Set Theory with Atoms by Harvey Friedman.

The relevant axiom is #11: "There is no set consisting of all atoms."

A consequence of this axiom is, that there definitely are 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.

-
It's not your doing, but I parsed Axiom 11 incorrectly and got very confused. Better I think is: "There is no set which contains every atom." (I originally read the statement as "There is no set $S$ such that every element of $S$ is an atom", which made no sense at all.) – Pete L. Clark Jan 25 2010 at 13:42
Do you agree with my reading, then? – Hans Stricker Jan 25 2010 at 13:50
Side note: If categorists tend to see sets as "bags of dots" (and categories as "bags of dots with arrows between them") why not measure category theory against a set theory which explicitely captures "bags of dots". Simply because the category of sets is equivalent to the category of sets with atoms (as I suppose)? – Hans Stricker Jan 25 2010 at 14:01
If you assume AC, then every set (even one containing atoms) can be well-ordered and is thus isomorphic to a von Neumann ordinal, which is a pure set (hereditarily contains no atoms). But in the absence of AC things can be more interesting, e.g. consider a permutation model of ZFA. – Mike Shulman Jan 25 2010 at 15:47

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.

Andreas Blass has an article here, where he investigates the connection between some theorems in homological algebra and the Axiom of Choice. In his introduction, he states:

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;

In contrast, sometimes it is useful to have only a set of atoms, as witnessed by Eric Hall's article, which contains the following remark.

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).

-

Nominal logic is based on the Frænkel-Mostowski permutation model of set theory. In particular Nominal logic has a freshness axiom that states ${\forall}x. {\exists}a \in \mathbb{A}. a \# x$, where $\mathbb{A}$ is the set of atoms and # is a definable relation which is a bit too complicated to put here.

For reference, see the work by Andrew Pitts and Murdoch Gabbay. For example "A New Approach to Abstract Syntax Involving Binders".

-

I don't know if this is exactly what you're looking for, but it's a theorem of NFU that $|\mathcal{P}(V)| < |V|$---which has as a corollary not only that there are atoms, but that the set of atoms is equipollent with the universe.

(A somewhat more disquieting way of putting this is that there are more atoms than there are sets.)

-
 Something's wrong. NF extends NFU and proves there are no urelements, hence you are effectively claiming that NF is inconsistent, which is actually a major open problem. – Emil Jeřábek Mar 3 2011 at 16:00 Fair enough; I should more accurately say NFU+Choice. NF itself is inconsistent with choice, which is essentially why NFU was devised. You're right that NF is inconsistent iff NFU can prove the existence of atoms without invoking the axiom of choice. – Ian Maxwell Mar 4 2011 at 20:35