Set theories that do require the existence of urelements? - MathOverflow

Set theories that do require the existence of urelements?

2010-01-25T07:42:05Z

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?

Answer by Hans Stricker for Set theories that do require the existence of urelements?

2010-01-25T13:34:40Z

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.

Answer by Joel David Hamkins for Set theories that do require the existence of urelements?

2010-01-25T13:59:08Z

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

Answer by Russell O'Connor for Set theories that do require the existence of urelements?

2010-02-18T19:39:32Z

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

Answer by Ian Maxwell for Set theories that do require the existence of urelements?

2011-03-03T15:52:02Z

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