How do we actually use urelements, in practice? Example request. In the usual approach to ordinals and cardinals (namely, von Neumann's approach), every cardinal is also an ordinal, and every ordinal is also a set. So if $\kappa$ is a cardinal, then the expression $2^\kappa$ has at least three meanings; so its meaning has to be specified in the surrounding text, or inferred from the context.
Now arguably, this isn't an issue of any real substance. That's a perfectly legitimate position; I don't happen to share it. For that reason, I'd like to experiment with the idea that set, ordinal and cardinal are mutually exclusive concepts. That way, if $\kappa$ is a cardinal, then expressions like $2^\kappa$ are unambiguous - e.g. in this case, its definitely cardinal exponentiation we're doing.
To give another example, there's good reason to distinguish between Conway's implementation of the surreal numbers, and the surreal numbers themselves. Otherwise, statements like $x=y$ are ambiguous - do we mean they're equal as numbers, or that they're equal as sets?
So we now have two reasons to distinguish between entities and the sets that represent them. The first was the ambiguity of expressions like $2^\kappa$. The second is the ambiguity of statements like $x=y$.
Lets focus our attention on the surreal numbers as an example. Suppose for a moment that we're sold on the above arguments. In this hypothetical universe, we want to distinguish between Conway's implementation of the surreal numbers, and the surreal numbers themselves.
Okay, one way of doing this would be to conservatively extend our language with new sorts. So we start off with a one sorted language whose elements are called 'sets.' Then we define a proper class $C$ whose elements are precisely the sets that Conway calls 'surreal numbers,' as well as an equivalence relation $\sim$ on $C$ that specifies which elements of $C$ are identical as numbers.
Now here comes the unconventional part. Instead of stopping there, we go one step further by extending our language with a new sort $S$ whose elements are called 'surreal numbers', and a canonical function $C \rightarrow S$ such that if $f$ is the aforementioned function, then $x \sim y \Leftrightarrow f(x)=f(y)$ for all $x,y \in C$.
It seems great in theory, but there's a problem: we can't collect surreal numbers into sets. After all, $\in$ is a relationship between two sets, so if $\alpha$ is a surreal number, then '$\alpha \in X$' isn't even a well-formed expression! Clearly, this isn't convenient.
Question. Can the approach using sorts be salvaged? If so, how?
I hope its salvageable, but lets assume for the moment that it isn't, or that no one knows how. Then we need another approach.
Enter the atom (or urelement, if you prefer). We begin the same: define $C$ and $\sim$. But, instead of adding a new sort $S$, we just collect a bunch of atoms together into a class, call it $S$ for 'surreal numbers.' Since atoms can belong to sets, concepts like $\alpha \in X$ make sense, even if $\alpha$ is surreal. Yay! We've solved the problem. That's the theory, but I've never actually seen this done in practice. What does it actually look like? Thus, I have a request.
Request. Can someone write up an example of how this would be done, in practice? I get the general gist of the idea, but I'm unsure about the details.
 A: Well, I completely disagree with this approach, but let me give my opinion on how it should be done.
The problem with atoms is that they are completely indiscernible from one another. If $a,b$ are atoms and $\varphi(a)$ is true then $\varphi(b)$ is true as well. At least in the language where all we have to express is $\in$ which is a relation pertaining sets and their elements.
This is why you ought to be adding two things. The class of atoms and an ordering on the atoms. Then you can add an axiom stating that the atoms and their ordering is a well-order class isomorphic to the usual class of ordinals. Then you can declare that from now on we shall refer to these atoms when we talk about ordinals.
Similarly we add a third sort for cardinals, and we can include the order or addition/multiplication into the language.
But the point is that there are no theorems which will be stated differently. Just whenever we refer to ordinals it will be clear that these ordinals have a different type than the rest of the sets. Of course we have to tweak a lot of definitions, for example a sequence of length $\alpha$ is no longer a function from the ordinal $\alpha$, but rather a function whose domain is $\{x\in{\sf Ord^*}\mid x<\alpha\}$. And so on and so forth. But beyond these sort of tweaks and changes there shouldn't be any change whatsoever. The only difference is that now when you say "Let $\alpha,\beta$ be two ordinals and $\gamma=\alpha+\beta$" we know that this cannot be addition as cardinals or anything because ordinals make a completely different type of object.
This is a particularly good time to bring up (again) the point that in set theory we really write meta-proofs rather than proofs. That is, we actually say "suppose that $\varphi(x,y,z)$ is the formula stating that $z$ is the ordered pair $\langle x,y\rangle$, then bla bla bla".
We don't really care about the formula. It's quite easy to take Kuratowski's definition for ordered pairs, but there are others. We just care about the fact that such definition exists and it's simple enough. Rarely we do care that the encoding is simple enough, but even then there are degrees of freedom.
Similarly we don't really care about the actual way of devising ordinals or cardinals, and all our proofs can be easily re-fitted to any definitions of these mathematical notions. But sometimes it makes things simpler that way, so it's more convenient to just use it like that. Of course when we have the von Neumann ordinals then often we can make nice shortcuts (such as the aforementioned about sequences), but it's not very difficult seeing that this is not a real mathematical issue. In fact, I doubt that you would find it confusing too.
