I'm thinking of creating a non-standard set theory with urelements that has a certain restriction on a specific kind of sets which ZF set theory does not have. Informally, I would like for all set elements to be "equally nested" e.g. $\{a, b\}$ and $\{\{a\}, \{b\}\}$ would both be valid sets in this set theory, but $\{a, \{b\}\}$ would not.
How would one formalize this?
On
One approach may be to introduce the binary relation symbol $\prec$ (meaning having nesting level less than or equal). Then you add axioms that nail the meaning of this:
$$\forall A\forall B:(A\prec B) \leftrightarrow (\forall \xi: \xi\notin A \land \xi\notin B) \lor (\exists\beta\in B\forall\alpha\in A:\alpha\prec\beta)$$
That is the nesting level of $A$ is no larger than that of $B$ if the most nested element of $A$ is has no larger nesting level than the least nested element of $B$.
Then we can formulate the equi-nested requirement:
$$\forall A \forall \xi,\eta\in A:\xi\prec \eta \land \eta\prec\xi$$
Also we need to adapt the axiom of extensionality to cope with ur-elements:
$$\forall A\forall B: (\forall \xi: \xi\in A\leftrightarrow \xi\in B) \leftrightarrow A=B \lor (\forall\xi: \xi\notin A\land\xi\notin B)$$
Apart from this we need to reformulate some of the normal axioms to prevent formation of non-equinested sets. We need to reformulate the axiom of pairing, schema of replacement to prohibit this. Also we need to do something about the axiom of infinity since the normal aproach is to construct the infinite set using differently nested sets.
One approach borrowing from Peanno's axioms would be to postulate a non-empty set of ur-elements with a injection to a proper subset of itself.
(*) I use here the construct that allow membership relation on ur-elements, that is an ur-element is an element $U$ such that $\forall x:x\notin U$
In what follows, I'll try to set up the beginnings of a set theory matching your intuitions.
First let's get the easy axioms down. Clearly we want extensionality - two sets are identical iff they have the same elements - except modified to allow urelements. There are multiple ways to do this, but I think the cleanest is to work in a two-sorted language, with one sort being for sets and the other for urelements; and have our language contain, besides the sort symbols, only the relation "$\in$." Then we have the axioms "If $x\in y$, then $y$ is a set," and "Two sets are the same iff they have the same elements;" let's call these two axioms together Extensionality.
The interesting bit, of course, is capturing the same-level restriction. I think the easiest way to formalize "every set is equi-nested" is the following:
Say that $x$ is a depth-$0$ element of $a$ if $x= a$. This is a bit of an abuse of terminology, but it's useful below.
Say that $x$ is a depth-$(n+1)$ element of $a$ if $x\in y$ for some depth-$n$ element of $a$.
It will be useful to write "$x\in_n y$" for "$x$ is a depth-$n$ element of $y$;" note that for each $n$, this is an abbreviation of a formula in the usual language of set theory with set and urelement sorts, so we're not adding to the language by using these symbols.
Then for each distinct $m, n\in\mathbb{N}$, we let $\psi_{m, n}$ be the sentence
(Note that by contrapositive, $\varphi_{m, n}\equiv\varphi_{n, m}$.) These are the Leveling axioms.
The conjunction of the sentences $\varphi_{m, n}$ prevents the kind of "level-breaking" behavior you want to avoid - without having to explicitly give sets types. For example, the sentence $\psi_{0, 1}$ prevents $a=\{a\}$ (and prevents $a\in a$ in general). And sets like $\{a, \{a, b\}\}$ are ruled out by $\psi_{1,2}$.
Alright, now we have a "first approximation" of the set theory we want: let $T_0$ consist of extensionality + all the leveling axioms.
Let's think a little about how the set theory we're building goes from here.
One natural thing we want at this point is the concept of "same level" - even though we've deliberately avoided giving sets explicit levels, we still want to be able to talk about the sets of the same level as a given one. There are two natural ways to do this.
We can look up one level: we write $a\sim_\uparrow b$ ("$a$ and $b$ have the same level from above") if there is some $x$ with $a, b\in x$.
We can look down one level: we write $a\sim_{\downarrow } b$ ("$a$ and $b$ have the same level from below") if for all $x\in a$ and $y\in b$ there is some $c$ with $x, y\in c$.
We can define other notions of "same level," by looking further above or below, but there doesn't seem to be a good reason to do so at the moment.
These each suggest a corresponding comprehension scheme: for each formula $\varphi(x; \overline{y})$, we have the axioms $$(*)_\varphi^\uparrow\quad\forall a, \overline{b}\exists c\forall d(d\in c\iff \varphi(d, \overline{b})\wedge a\sim_\uparrow d)],$$ and $$(*)_\varphi^\downarrow \quad\forall a, \overline{b}\exists c\forall d(d\in c\iff \varphi(d, \overline{b})\wedge a\sim_\downarrow d)].$$
Each scheme is to be interpreted the same way: as saying that we can form the set of all things of a given level satisfying any first-order property. The difference is in how they interpret "level." Specifically, the point of separation is urelements.
We have a choice to make: how do we want to treat urelements? Specifically, do we want all urelements to have the same "level," or do we want to allow urelements to have different "levels?" The point is that if $u, v$ are urelements, then we trivially have $u\sim_\downarrow v$ (since neither has any elements at all) but we may not have $u\sim_\uparrow v$.
Thinking about this, we are led to two natural theories:
If we want all urelements to be the same level, then it's natural in fact to demand that $\forall a, b(a\sim_\uparrow b\iff a\sim\downarrow b)$. Taking this, the theory $T_0$, and both (or equivalently, either) comprehension schemes gives us the theory $T_{flat}$.
If we want to allow urelements to be on different levels, then we clearly don't want to allow the $(*)^\downarrow$-scheme, since they would let us form the set of all urelements. So for this purpose, we want the theory $T_0$ and just the $(*)^\uparrow$-scheme; the resulting theory is $T_{bumpy}$.
From now on we'll write "$\sim$" for "$\sim_\uparrow$," the point being that in $T_{flat}$ they're equal and in $T_{bumpy}$ we're not directly interested in $\sim_\downarrow$.
Clearly $T_{flat}$ implies $T_{bumpy}$. I suspect, though, that $T_{bumpy}$ will ultimately be the "right" one to look at.
Now let's take stock and see what we have so far!
What can we prove? One easy theorem of $T_\uparrow$ (and hence of $T_\downarrow$ as well) is that there is no "top level": for each $a$ there is a $b$ with $a\in b$; in fact, the set $\{a\}$ itself exists. We apply Leveling to the formula "$x=a$": then $a$ is the only thing with the same level as $a$ which is equal to $a$, so this gives us $\{a\}$.
Another easy result in both theories is that $\sim$ is preserved by set formation: if $a,b$ are sets, where every element of $a$ is $\sim$ every element of $b$ (equivalently, we can replace "every" with "some"), then $a\sim b$, and $\{a, b\}$ exists. This lets us construct Kuratowski ordered pairs: if $a\sim b$ then the set $\{\{a\}, \{a, b\}\}$ exists.
That said, we can't prove much: the structure consisting only of $\{\}, \{\{\}\}, \{\{\{\}\}\}, ...$ is a model of both $T_\uparrow$ and $T_\downarrow$, so these are extremely weak axiom systems if we don't incorporate urelements. In fact, the only variety we'll be able to get in the "pure" (= urelement-free) part is by using illfounded sets! So this is a theory which works best in the additional presence of an antifoundation axiom appropriately formulated to play well with the leveling axioms. And as things stand, the situation doesn't change too much when we bring in urelements.
So the next thing to do is think about adding "stuff" to our theory. There are three general kinds of "stuff" that occur to me:
Although the well-founded pure part of any model of these theories is basically trivial, additional axioms could make things much more interesting on the illfounded pure (and impure) part! For instance, one natural option is a version of powerset: that given a set $a$, the set of nonempty subsets of $a$ is again a set (we need nonempty because the emptyset has "level zero").
We could give the urelements structure by expanding the language to include function and relation symbols on the urelements. So, e.g., we could have the set of urelements form a group. This idea of "building a set theory on top of a structure" is a common one in set theory with urelement, especially in higher computability theory where we often look at a particular family of sets built "on top of" a given structure.
The power of sets in ZFC comes from their versatility, and this versatility can be lost when we force strict type agreement as we've done here. So it's reasonable to drop the ZFC-intuition that "sets are enough," and add some new sorts! For instance, maybe we want to consider sequences of objects of possibly different "levels." In this case, we're viewing a sequence as a different kind of "thing" than a set. From a ZFC standpoint that feels weird, but here things are different - so maybe this is something we want to do!
So there are lots of directions we can go. But I'll stop here for now: even though we certainly don't have a satisfactory set theory yet, we have a decent start towards building in that direction.