Ur-elemental surprises For most of my (mathematical) life, I believed that there was really no essential difference between set theory without urelements and set theory with urelements. However, while that may be true in certain coarse senses, there are occasions where things genuinely change if urelements are used.
The three big examples I'm aware of are the following:

*

*Independence results over $\mathsf{ZFA}$ are much easier to establish than over $\mathsf{ZF}$. (Of course via Jech–Sochor/Pincus many such independence results can be "ported over" to $\mathsf{ZF}$, but (i) not all can be, (ii) that takes serious work and came much later, and (iii) I think it's still fair to say that the original arguments have a distinct "flavor" of their own.)


*When we look at very weak set theories (around the level of $\mathsf{KP}$), there are technical niceties to having urelements around that makes them the "right" choice. Barwise's excellent book Admissible sets and structures includes some discussion of this point. To quote from chapter 1:

*

*"[O]ne is tempted to make a simplifying mistake. We have first thrown out urelements from $\mathsf{ZF}$ because $\mathsf{ZF}$ is so strong. When we then weaken $\mathsf{ZF}$ to $\mathsf{KP}$ we must remember to reexamine the justification for banning the urelements. Doing so, we discover that the justification has completely disappeared. [… T]he chief advantage [of allowing urelements] is that it allows us to form, for any structure $\mathfrak{M}=\langle M, R_1,\dotsc,R_k\rangle$, a particularly important admissible set $\mathbb{HYP}_\mathfrak{M}$ above $\mathfrak{M}$."



*Looking at alternative set theories, the theory $\mathsf{NF}{+}\mathsf{AC}$ is outright and complicatedly inconsistent and the consistency of $\mathsf{NF}$ is still open (Holmes' claimed proof having not yet been fully accepted to the best of my knowledge). However, the respective urelement-allowing variants $\mathsf{NFUC}$ and $\mathsf{NFU}$ are easily proved to be consistent relative to weak set theories.
I'm curious about what other examples might be out there:

What are some examples where it is especially convenient, especially inconvenient, or simply meaningfully different to work with urelements as opposed to working without urelements?

To be clear, I'm really only interested in purely mathematical — maybe "technical" is more appropriate? — considerations here. The question of whether set theory with or without urelements is more "natural" is an interesting one, but not the sort of thing that I'm asking about here. I'm also not asking about historical issues around the choice to disallow urelements (although again that's an interesting topic).
 A: In his dissertation work, Bokai Yao has investigated the nature of urelement set theory, particularly in the context of a proper class of urelements. See a preprint at:

*

*Bokai Yao, Forcing with urelements, arxiv:2212.13627, 2022.

There is a surprising subtlety to the precise formulations of the theory — if one is not careful, many principles expected to be equivalent turn out not to be.

*

*In particular, the replacement axiom does not imply collection over the other natural axioms, when there are urelements. (folklore)

*With only the replacement formulation, it is consistent to have a proper class of urelements, yet every set has only finitely many urelements. (folklore)

*Even with collection, it is consistent that there is a proper class of urelements, yet every set has only countably many urelements.

*the various forms of the axiom of global choice are no longer equivalent, when there are a proper class of urelements.

*The DC scheme is not provable in ZFCU, when there are urelements, even though one has the axiom of choice, the well order principle and more. Specifically, the $\omega$-DC scheme is not provable in the replacement-only theory, and the $\alpha$-DC scheme is not provable even when one adds the collection axiom.

Here is Yao's diagram showing some of the theories that he separates:

ZFCU${}_\text{R}$ is the urelement set theory with replacement, but not collection, and with AC. RP is the reflection principle; Tail asserts that every set of urelements has a tail cardinality (a largest cardinality of urelements disjoint from it); Plenitude asserts that for every cardinal $\kappa$ there is a set of $\kappa$ many urelements; Closure asserts that the cardinals realized as sets of urelements is closed under set suprema; Scatter (also called duplication) asserts that for every set of urelements, there is an equinumerous disjoint set of urelements.
In my view, the central lesson is that it is a quite subtle matter to find the right theory for set theory with urelements, and the problem is only compounded if one works over weak theories. Many expected principles go awry, and it is naive to expect simply to take a given theory and add urelements without considering these subtle issues.
Yao and I also have a joint paper in which we consider urelements in the context of various second-order set theories, such as Kelley-Morse set theory with urelements.

*

*Joel David Hamkins and Bokai Yao, Reflection in second-order set theory with abundant urelements bi-interprets a supercompact cardinal. 2022. To appear in the JSL. arxiv:2204.09766
Again there is a separation of theories, and the main result is concerned with the surprising strength of the second-order reflection principle when there is a proper class of urelements, particularly when this class has size larger than Ord. The main result is that the strength of reflection with the abundant atoms axiom implies the consistency of a supercompact cardinal.
The first part of our paper gives a series of bi-interpretability results, showing how various pure set theories are bi-interpretable with corresponding urelement theories. Such results provide a negative answer to your question, in the sense that in the context where the bi-interpretation result is applicable, there is nothing at stake in the choice between the pure set theories and the urelement theories — bi-interpretable theories have the same semantic content and can be seen as translations of one another.
Our final philosophical conclusion emphasizes that in order for urelement set theory to be truly useful, that is, not translatable as a pure set theory, one must have some weird sets of urelements.

Furthermore, the bi-interpretability of many natural formulations of urelement
set theory with corresponding pure set theories, as in theorems 1 and 16, is itself
an explanation of precisely how those particular urelement conceptions can be
dispensed with in the foundations of mathematics—any mathematical structure
to be found in the urelement set theories can be found via the bi-interpretation
also in the corresponding pure set theories. And theorems 20 and 30 show that this
remains true even when one adds abundant urelements and second-order reflection.
If urelement set theories are to play an indispensible role in the foundations
of mathematics, therefore, it must not be with those theories, but rather with
urelement set theories that are not bi-interpretable with a pure set theory and
perhaps not interpretable at all in any pure set theory. But in this case, it would
seem that the urelement set theories must involve much stranger sets of urelements,
neither well-orderable nor even equinumerous with any pure set. The mathematical
structures built on such domains will not be isomorphic with any structure to be
found amongst the pure sets. But what are these strange urelements that give rise
to these weird sets? One wants an explanation for why we should need or expect to
find such sets in the foundations of mathematics. What mathematical structures
will they represent?

