Urelement

There are several different but essentially equivalent ways to treat urelements in a first-order theory. One way is to work in a first-order theory with two sorts, sets and urelements, with a ∈ b only defined when b is a set. In this case, if U is an urelement, it makes no sense to say X \in U, although U \in X is perfectly legitimate. Another way is to work in a one-sorted theory with a unary relation used to distinguish sets and urelements. As non-empty sets contain members while urelements do not, the unary relation is only needed to distinguish the empty set from urelements. Note that in this case, the axiom of extensionality must be formulated to apply only to objects that are not urelements. This situation is analogous to the treatments of theories of sets and classes. Indeed, urelements are in some sense dual to proper classes: urelements cannot have members whereas proper classes cannot be members. Put differently, urelements are minimal objects while proper classes are maximal objects by the membership relation (which, of course, is not an order relation, so this analogy is not to be taken literally). == Urelements in set theory ==

The Zermelo set theory of 1908 included urelements, and hence is a version now called ZFA or ZFCA (i.e. ZFA with axiom of choice). It was soon realized that in the context of this and closely related axiomatic set theories, the urelements were not needed because they can easily be modeled in a set theory without urelements. Thus, standard expositions of the canonical axiomatic set theories ZF and ZFC do not mention urelements (for an exception, see Suppes). Axiomatizations of set theory that do invoke urelements include Kripke–Platek set theory with urelements and the variant of Von Neumann–Bernays–Gödel set theory described by Mendelson. In type theory, an object of type 0 can be called an urelement; hence the name "atom". Zermelo insisted on keeping urelements in his set theory, and considered the empty set a special case of an urelement. Urelements also remain useful in model theory, particularly in Fraenkel–Mostowski models. Adding urelements to the system New Foundations (NF) to produce NFU has surprising consequences. In particular, Jensen proved the consistency of NFU relative to Peano arithmetic; meanwhile, the consistency of NF relative to anything remains an open problem, pending verification of Holmes's proof of its consistency relative to ZF. Moreover, NFU remains relatively consistent when augmented with an axiom of infinity and the axiom of choice. Meanwhile, the negation of the axiom of choice is an NF theorem. Holmes (1998) takes these facts as evidence that NFU is a more successful foundation for mathematics than NF. Holmes further argues that set theory is more natural with than without urelements, since we may take as urelements the objects of any theory or of the physical universe. In finitist set theory, urelements are mapped to the lowest-level components of the target phenomenon, such as atomic constituents of a physical object or members of an organisation. == Quine atoms ==

An alternative approach to urelements is to consider them, instead of as a type of object other than sets, as a particular type of set. Quine atoms (named after Willard Van Orman Quine) are sets that only contain themselves, that is, sets that satisfy the formula x = {x}. Quine atoms cannot exist in systems of set theory that include the axiom of regularity, but they can exist in a non-well-founded set theory. Quine introduced Quine atoms (called "individuals") in his Mathematical Logic as a way to formalize atoms without changing the axiom of extensionality. The system of Mathematical Logic is an extension of Quine's New Foundations (NF), and NF does allow non-well-founded sets like Quine atoms. In fact, assuming the consistency of NF (or NFU), there exist models with no Quine atom, one Quine atom, or many Quine atoms. However, Quine atoms are not an adequate treatment of atoms in NF, since " is a Quine atom" is not a stratified sentence. On one hand, this means that stratified comprehension cannot separate Quine atoms from other sets. On the other hand, Quine atoms allow some constructions that could not be justified with structureless atoms: for example, given a set of Quine atoms, it is easy to construct a map from each to its singleton {{math|{x}}} (which is just the identity map on ). Therefore a model of NF with Quine atoms is usually much different from a model of NFU, where the cardinality of the set of all atoms is usually larger than the set of all sets. The significance of this difference is evidenced by the fact that NFU is consistent with the axiom of choice while NF is not. Similar to the NF situation, ZF set theory with the axiom of regularity removed cannot prove that any non-well-founded sets exist (unless it is inconsistent, in which case it will prove any arbitrary statement), but it is compatible with the existence of Quine atoms. Aczel's anti-foundation axiom implies that there is a unique Quine atom. Other non-well-founded theories may admit many distinct Quine atoms; at the opposite end of the spectrum lies Boffa's axiom of superuniversality, which implies that the distinct Quine atoms form a proper class. although other authors, e.g. Jon Barwise and Lawrence Moss, use the latter term to denote the larger class of sets with the property x ∈ x. == References ==